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 Coq proof assistant. The paper is self-contained; it includes a complete discussion of the algorithm and its correctness argument in English.
翻译:Hashgraph 共识算法是用于分配共享分类账的非同步的 Byzantine 断层容忍度的算法,其主要显著特征是,在不交换任何额外信息的情况下实现协商一致;每个参与者的投票可以从公共信息中确定,因此投票无需转发。在本文中,我们讨论了我们使用 Coq 验证助理将Hashgraph 算法及其正确性证明正规化的经验。 该文件是自成一体的,包括用英文全面讨论算法及其正确性论点。