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.

翻译：Hashgraph共识算法是一种用于分布式共享账本的异步拜占庭容错算法。其主要区别性特征在于无需交换任何额外消息即可达成共识；每个参与者的投票均可从公开信息中确定，因此无需传输投票信息。本文讨论了使用Rocq证明助手对Hashgraph算法及其正确性证明进行形式化验证的经验。本文自成体系，包含对算法及其正确性论证的完整英文论述。