Coq

公共分布式分类账平台Hedera Hashgraph最近宣布hashgraph consensus算法已被验证为异步拜占庭容错（BFT）算法。这是通过使用Coq系统的计算机检查的数学证明完成的。这证明了哈希图报告中的声明。据称哈希图在数学上是分布式系统的最高安全级别。Coq是一种正式的验证，它提供了一种形式语言来编写可执行的数学定义和算法。它还可以用于编写定理和机器检查证明的半交互开发环境。Coq通常用于验证程序、编程语言和数学的属性。与数学证明不同的是，Coq证明是通过计算机进行检查的。这有助于避免人类在阅读证明时可能犯的错误。