Correctness proofs of distributed systems with Isabelle
summary
Introduces a concrete Isabelle/HOL model of a simple consensus protocol (one acceptor, many proposers), implements proposer and acceptor step functions and a small network/harness (~30 lines model), and states the concrete claim: agreement (any two decided values are equal). Proves agreement by defining two precise invariants, using sledgehammer and Metis for automated steps, then a proof by induction over event lists; the full mechanized proof is about 200 lines proof and is available online.
AI-written summary · about
chapters (15)
- 0:00Intro
- 2:43Is it worth it
- 4:36Example distributed system
- 5:32Agreement property
- 6:10Consensus algorithm
- 9:50Sequence of time steps
- 10:22Step function
- 11:30Isabelle syntax
- 13:38Isabelle code
- 19:06Logical implication
- 19:47Formalizing the property
- 25:08Invariants
- 27:41Quantifiers
- 31:18Proof
- 37:09Proof by Induction
related talks
25mProperty-agnostic base case extension for scalable verification of distributed systems
16mInductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline...
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
24mVerifying Almost-Sure Termination for Randomized Distributed Algorithms
18mSureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine(…)
28mReasoning about Distributed Reconfigurable Systems
18mAdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects
16mBasilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols