Compositional Verification of Composite Byzantine Protocols
Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Lewis Gilbert, Ilya Sergey · 2024
Byzantine Fault-Tolerant (BFT) protocols are known to be difficult to design and to reason about. To address this challenge, on one hand, several approaches have been developed recently for computer-aided formal verification of the desired correctness properties, both safety and liveness, of standalone BFT protocols. On the other hand, the distributed computing community has made attempts to reduce the conceptual complexity of constructing new such protocols by showing how to assemble them from simpler "building blocks". No methodology to date combines these two approaches for foundational verification of arbitrary BFT protocols.