Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant Systems

Explore a conference talk from the Dafny 2025 workshop that introduces Shipwright, a modular framework designed for verifying liveness properties in Byzantine Fault Tolerant (BFT) systems. Presented by researchers Derek Leung, Nickolai Zeldovich, and M. Frans Kaashoek from the Massachusetts Institute of Technology, this 18-minute presentation addresses the critical challenge of ensuring BFT systems can continue operating even under adversarial attacks. Learn how Shipwright employs refinement techniques to replace complex systems with simpler ones while taking a compositional approach to verification that manages proof costs and validates theorems for usefulness. The talk tackles three key challenges: decomposing implementations into smaller subprotocols, securely manipulating cryptographic signatures with untrusted code, and efficiently checking fairness properties using automated reasoning. See how the framework is applied to the PBFT consensus protocol, demonstrating the extraction and verification of a single view implementation.