HederaHashgraph在下一代公共分类账中具有多种治理。最近宣布，哈希图共识算法已被验证为异步拜占庭容错技术。这是通过使用Coq系统的计算机检查的数学证明来完成的。分布式系统安全性的证明这是哈希表报告中提出的声明的证明。有人认为Hashgraph在数学上是分布式系统的最高安全级别。 Leemon Baird博士准备举行一次有关正式方法的会议。这将在Hedera18上举行，这是第一届Hashgraph开发者大会。还有一个在线直播，供有兴趣的人使用。 Coq是正式的验证证明。它提供了一种用于编写可执行的数学定义和算法的形式语言。它也可以用来编写定理和环境的半交互式开发的机器检查证明。 Coq通常用于验证程序，编程语言和数学的属性。与人工检查的数学证明不同，Coq证明是通过计算机检查的。这有助于避免人们在阅读证明时可能犯的错误。通过使用Coq的协助证明来进行验证。它检查证明是否正确。剑桥梅隆大学计算机科学副教授Karl Crary完成了验证工作。里蒙博士说，这仅仅是个开始。他说，经过计算机验证的证明是未来，信任和安全非常重要。异步拜占庭容错技术30多年来，拜占庭容错技术（BFT）被用作任何分布式系统的安全标准。如果系统可以保证所有节点都达成共识并知道它们已经达成共识，则该系统称为BFT。这种共识始终是一致的。 BFT需要在允许大量错误和攻击的同时实现这一目标。这些拜占庭式错误包括共谋，说谎和选择性的不参与行为。对于节点，通常很难就这些错误达成一致。此外，这些节点可能会崩溃。最好的BFT类型是异步的。在aBFT系统中，诚实成员之间的消息可能会延迟或太长。此外，他们可能无法联系到收件人。实际上，不良参与者可以部分控制网络。这是达成分布式共识的黄金位置。在这样的假设下，安全的分布式分类帐技术需要达成共识。一些算法可能声称支持“部分”算法。异步BFT。这是消息不会延迟超过给定时间段的地方。他们总是在规定的截止日期之前完成任务。但是，现实情况是，许多攻击者可能会利用此假设。他们可能使网络瘫痪或破坏交易发生的方式。有了Coq证明，Hedera将成为第一个使用计算机来验证数学证明的分类帐，这实际上是异步BFT。即使在出现网络错误和恶意节点的情况下，它也可以确保一致性。