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

Harold Carr, Christopher Jenkins, Mark Moir +2

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-…