Linked Presentation: Anvil: Verifying Liveness of Cluster Management ControllersInductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs
