Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems
summary
Sift presents a concrete method that proves refinement between implementations and specs while automating most work: it uses refinement-guided automation plus encapsulation to turn a multi-layer refinement check into a single-state safety problem for a monolithic prover (IC3PO), and falls back to a divide-and-conquer step that inserts intermediate layers when automation times out. The authors verify six systems (leader election, distributed lock, two‑phase commit without extra layers; shared hash table with event fixes; Raft and multiplexers with added layers), cut Raft effort from ~12 to 4 person‑weeks, and ship executable verified implementations on GitHub.
AI-written summary · about
chapters (13)
- 0:00Intro
- 0:28Distributed systems have bugs
- 1:05Formal Verification
- 3:15The Power of Refinement
- 5:01A Hard Choice
- 6:30Encapsulation
- 8:14Target system
- 11:09Preconditions to If-statements
- 11:59Preconditions to Invariants
- 15:43Workflow of Sift
- 16:20Evaluation
- 17:38Performance
- 18:53Conclusion
related talks
48mThe Verification of a Distributed System
14mA Refinement Methodology for Distributed Programs in Rust
38mThe Verification of a Distributed System
15mStatically Verified Refinements for Multiparty Protocols
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
13mSharding the State Machine: Automated Modular Reasoning for Complex Concurrent System
19mBridging the Verifiability Gap: Why We Need More From Our Specs and How We Get It
16mIgloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verifica