Byzantine fault tolerant (BFT) systems guarantee liveness, which means that they are able to continue operating even under adversarial attack. Unfortunately, the presence of a single bug in a BFT implementation can compromise the security of the system. Formal verification is a promising approach to proving the absence of such bugs, but it requires considerable proof effort and choosing the right theorem to prove is tricky.

We introduce Shipwright, a framework for proving liveness of BFT systems using refinement, a technique that allows us to replace complex systems with simple ones. We take a compositional approach to verification in order to manage proof costs and to vet theorems for usefulness. We tackle three new challenges: the decomposition of an implementation into smaller subprotocols, the secure manipulation of cryptographic signatures by untrusted code, and the efficient checking of fairness properties with automated reasoning techniques. We apply the framework to the PBFT consensus protocol and show that we can extract and verify an implementation of a single view.