Towards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda: Extended Version

TL;DR

This paper presents a formal, machine-checked model and correctness proofs of HotStuff-based Byzantine Fault Tolerant consensus in Agda, focusing on safety and assumptions about honest peers, as a step towards verifying various implementations.

Contribution

It introduces an abstract, implementation-independent model of HotStuff/LibraBFT with formal proofs in Agda, enabling correctness verification across multiple implementations.

Findings

Formal model of HotStuff/LibraBFT in Agda

Proof of safety properties for the abstract protocol

Definition of assumptions about honest peer behavior

Abstract

LibraBFT is a Byzantine Fault Tolerant (BFT) consensus protocol based on HotStuff. We present an abstract model of the protocol underlying HotStuff / LibraBFT, and formal, machine-checked proofs of their core correctness (safety) property and an extended condition that enables non-participating parties to verify committed results. (Liveness properties would be proved for specific implementations, not for the abstract model presented in this paper.) A key contribution is precisely defining assumptions about the behavior of honest peers, in an abstract way, independent of any particular implementation. Therefore, our work is an important step towards proving correctness of an entire class of concrete implementations, without repeating the hard work of proving correctness of the underlying protocol. The abstract proofs are for a single configuration (epoch); extending these proofs across configuration changes is future work. Our models and proofs are expressed in Agda, and are available in open source.