LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols
summary
LiDO-DAG gives an abstract concurrent-object model and a refinement proof showing DAG protocols simulate leader-based consensus, implemented in Coq and extracted to executable artifacts. It yields the first mechanized safety and liveness proofs for Narwhal, Bullshark, and Sailfish, uncovers an optimization that reduces Sailfish worst-case latency, and reports a small formalization effort with reusable artifacts and evaluated artifact badges (DOI and Zenodo available).
AI-written summary · about
chapters (10)
- 0:00Consensus protocols intro
- 3:34DAG protocol verification challenges
- 5:20Byzantine fault tolerance
- 7:04Leader vs DAG consensus
- 9:34LiDO-DAG model
- 12:28LiDO model components
- 14:37Adapting LiDO for DAG
- 16:26Proving safety and liveness
- 17:29Takeaways and conclusion
- 18:13Q&A on efficiency
related talks
17mLiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
22mOptimizing network topologies...
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
19mMostly Automated Verification of Liveness Properties for Distributed Protocols w...
24mFormal Verification of a Distributed Dynamic Reconfiguration Protocol
16mBasilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols
45mCorrectness proofs of distributed systems with Isabelle
55mUntangling the BlockDAG