Bolt-On Strong Consistency: Specification, Implementation, and Verification
summary
Shows how consensus safety can be proved from local properties by implementing strong replication atop a causal weak store and verifying at the single-node “worm” level. Introduces the stable update precondition as a local inductive artifact, implements a verified framework Super-V that generates SMT (EPR-decidable) checks, and verifies a raft-like system called Ferry (preconditions ≈110 LOC). Ferry runs on causal broadcast, is implemented and verified, and outperforms a leading Raft implementation on a five-node cluster.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:26Worm’s eye verification
- 2:12Party planning protocol
- 3:37Consensus safety properties
- 6:05Stable update precondition
- 9:57Ferry consensus case study
- 11:48Bolt-on strong consistency
- 12:11Conclusion
- 12:34Q&A
related talks
22mHow to Enforce and Verify Invariants in Weakly Consistent Databases
25mSafe Replication through Bounded Concurrency Verification
15mRethinking Safe Consistency in Distributed Object-Oriented Programming
43mWhat We Talk About When We Talk About Distributed Systems
24mArbitration-Free Consistency Is Available (and Vice Versa)
14mDistributed Consensus in 15 Minutes!
15mMuch ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent D
17mMixed & Verified Consistency with Propel and ConOpY