SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine(…)
summary
SureDistrib defines probabilistic IO automata in the Rocq proof assistant and proves composition lemmas that let an abstract underlay be replaced by an implementation. It gives a mechanized proof that a modified Honeybadger-style binary agreement with an ideal common coin achieves almost-sure termination (probability 1) by building bounded [0,1] “hope” functions, showing submartingale properties, applying the optional stopping theorem, and extracting a quantitative expected-termination bound; artifacts and proofs are published and reusable.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 0:58Consensus protocols challenges
- 2:46Asynchronous consensus hard
- 4:10SureDistrib framework
- 5:13Probabilistic IO automata
- 7:20Composition proof architecture
- 8:46Infinite traces in proofs
- 9:08Asynchronous agreement common coin
- 10:32Proving liveness hope functions
- 13:21Conclusion future extensions
- 14:05Q&A
- 14:26Layered composition
- 15:30Common coin feasibility
- 16:41Detecting termination violations
- 17:45Final remarks
related talks
24mVerifying Almost-Sure Termination for Randomized Distributed Algorithms
45mCorrectness proofs of distributed systems with Isabelle
21mEnabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based S...
25mProperty-agnostic base case extension for scalable verification of distributed systems
28mReasoning about Distributed Reconfigurable Systems
48mThe Verification of a Distributed System
30mVerifying Reliable Network Components in a Distributed Separation Logic with Dep...
18mAdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects