Verifying the Hashgraph Consensus Algorithm
Karl Crary
TL;DR
This paper discusses the experience formalizing the Hashgraph algorithm and its correctness proof using the Rocq proof assistant, and includes a complete discussion of the algorithm and its correctness argument in English.
Abstract
The Hashgraph consensus algorithm is an algorithm for asynchronous Byzantine fault tolerance intended for distributed shared ledgers. Its main distinguishing characteristic is it achieves consensus without exchanging any extra messages; each participant's votes can be determined from public information, so votes need not be transmitted. In this paper, we discuss our experience formalizing the Hashgraph algorithm and its correctness proof using the Rocq proof assistant. The paper is self-contained; it includes a complete discussion of the algorithm and its correctness argument in English.