LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
summary
LiDO is a refinement-ready model that adds an explicit pacemaker state so liveness of partially synchronous Byzantine SMR reduces to a few safety invariants, proven in Coq. The authors mechanize safety (~4,000 LOC) and liveness (~1,700 LOC) proofs for both unpipelined and pipelined Jolteon, extract an executable implementation to OCaml, and claim the first mechanized liveness proof for a pipelined Byzantine protocol. Artifacts and proofs are available for reuse and evaluation.
AI-written summary · about
chapters (11)
- 0:00LiDO introduction
- 2:31Partial synchrony and consensus
- 4:40Liveness proof challenges
- 5:23LiDO model and safety
- 7:32LiDO contributions and J protocol
- 8:13ADL to LiDO evolution
- 10:25LiDO operation example
- 12:17LiDO liveness proof method
- 14:03Jia protocol with LiDO
- 15:10Pipelining optimization
- 15:31Conclusion and future work
related talks
19mLiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols
19mMostly Automated Verification of Liveness Properties for Distributed Protocols w...
28mLiveness to Safety for Distributed Systems
18mAdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects
25mProperty-agnostic base case extension for scalable verification of distributed systems
15mTLC: Temporal Logic of Distributed Components
18mShipwright: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant(…)
24mFormal Verification of a Distributed Dynamic Reconfiguration Protocol