Formal Verification of a Distributed Dynamic Reconfiguration Protocol
summary
Formal, machine-checked TLA+ proofs establish safety of MongoRaftReconfig: an inductive invariant of 20 conjuncts and a TLAPS proof of LeaderCompleteness and StateMachineSafety. Development spends ~1–2 months finding the invariant and ~3–4 months writing proofs; artifact totals ≈3200 lines of TLA+ (360 for the spec, ~140 for the invariant), 78 lemmas and 3 top-level theorems, and full proof checking takes about 40 minutes using TLAPS and TLC for counterexamples.
AI-written summary · about
chapters (5)
related talks
28mReasoning about Distributed Reconfigurable Systems
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
25mProperty-agnostic base case extension for scalable verification of distributed systems
41mDesigning software with complex configurations
19mMostly Automated Verification of Liveness Properties for Distributed Protocols w...
48mThe Verification of a Distributed System
17mLiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
19mBridging the Verifiability Gap: Why We Need More From Our Specs and How We Get It