Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant(…)
summary
Shipwright is a Dafny framework that proves liveness of BFT systems by modular compositional refinement and novel completion measures. The project is ~12,000 lines of Dafny framework code and verifies a single PBFT view with about 24,000 lines of Dafny, extracts to Go, and the full verification runs in ~4 minutes on a 12‑core machine. It handles untrusted cryptographic signature manipulation, encodes fairness as per‑task obligations, produces an executable server (~250 lines of Go), and the verified view refinement succeeds.
AI-written summary · about
chapters (10)
- 0:00Byzantine fault tolerance intro
- 1:08Verifying BFT with Shipwright
- 2:54Multicast proposal protocol
- 6:03Liveness with fairness predicates
- 8:30Liveness proof completion
- 12:19Decomposing PBFT subprotocols
- 13:43Executable implementations
- 14:47Go code from specs
- 15:09Summary of framework
- 15:31Q&A on fairness
related talks
17mThe Bedrock of Byzantine Fault Tolerance: A Unified Platform for BFT Protocols...
17mLiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
36mFlexible Byzantine Fault Tolerance
15mAlea-BFT: Practical Asynchronous Byzantine Fault Tolerance
18mRandomized Testing of Byzantine Fault Tolerant Algorithms
17mIn Link We Trust: BFT at the Speed of CFT using Switches
30mStrengthening Reliable Decentralized Systems at Interchain