Finding Invariants of Distributed Systems: It's a Small (Enough) World After All
summary
Swiss automates construction of inductive invariants by exhaustively searching a bounded candidate space, using counterexample-guided synthesis and SMT checks to prune failed candidates. A two-phase pipeline—a wide breadth pass that finds many small lemmas and a finisher that looks for one large final lemma—handles universal and existential quantifiers and accepts user hints about which variables to quantify. The system finds and verifies invariants for Paxos, solves 18 of 27 protocols, and shrinks search spaces from ~100 trillion possible predicates (100 ms per check) down to ~155 or from 820M to ~2k.
AI-written summary · about
chapters (7)
- 0:00The verification challenge
- 2:16Introducing Swiss
- 3:48Defining invariants
- 5:38Algorithm internals
- 7:35Search optimizations
- 8:40Evaluation and results
- 10:29Conclusion
related talks
16mInductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline...
14mDistAI: Data-Driven Automated Invariant Learning for Distributed Protocols
16mBasilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols
34mThe Math Behind Distributed Systems
48mThe Verification of a Distributed System
14mA Refinement Methodology for Distributed Programs in Rust
25mProperty-agnostic base case extension for scalable verification of distributed systems
28mReasoning about Distributed Reconfigurable Systems