Compositional Verification of Byzantine Consensus

Until now, computer-aided proofs of the liveness of byzantine consensus algorithms assumed synchrony to reason in lock steps or the error-prone manual intervention of experts in the proof checker but could not be automated through model checking. We propose a compositional approach to verify a consensus algorithm, for any number n of processes and any upper bound t < n/3 on the number of byzantine processes. To this end, we identify a fairness property that makes this—otherwise purely asynchronous—byzantine consensus algorithm amenable to model checking. We decompose the algorithm in two parts: an inner broadcast algorithm and an outer decision algorithm. We encode these algorithms using threshold automata, and we formalize their properties in temporal logic. This allows us to automatically check the inner broadcasting algorithm, assuming fairness. For the verification of the outer algorithm, we simplify the automaton of the inner algorithm by relying on its checked properties. We verify in less than 70 seconds, not only the safety of byzantine consensus but also its liveness.