The hashgraph consensus algorithm has been validated as asynchronous Byzantine Fault Tolerant (ABFT) by a math proof checked by computer using the Coq system. This proves the claims stated in the hashgraph tech report that hashgraph is ABFT — mathematically the highest possible level of security for distributed systems.
Coq is a formal proof verification system. Coq provides a formal language to write mathematical definitions and executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. It is often used for certifying the properties of programs, programming languages, and mathematics. Unlike most math proofs that are merely checked by humans, a Coq proof is actually checked by a computer. This avoids some of the mistakes that humans can make when reading a proof.
Read more about the ABFT proof here: Coq Proof Completed By Carnegie Mellon Professor Confirms Hashgraph Consensus Algorithm Is Asynchronous Byzantine Fault Tolerant
Download the Coq proof here: https://www.hedera.com/hashgraph-coq.zip