验证哈希图共识算法

AI总结：

本文验证了哈希图共识算法的正确性，通过形式化方法和证明工具实现了算法的正确性证明。

摘要：

哈希图共识算法是一种用于分布式共享账本的异步拜占庭容错算法。其主要特点是它在不交换任何额外消息的情况下达成共识；每个参与者的投票可以由公开信息确定，因此无需传输投票。本文讨论了我们使用Rocq证明助手对哈希图算法进行形式化及其正确性证明的经历。本文自成一体；它包含了算法及其正确性论证的完整讨论。

英文摘要：

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.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。