Linked Presentation: Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol ProofsIronSpec: Increasing the Reliability of Formal Specifications