Formal Verification of Hashgraph Protocol : Future of Digital Trust

A Mathematical Milestone for Hashgraph DLT : Coq Proof Assistant based Verification of Asynchronous BFT Consensus Correctness

In the recently concluded Hedera Hashgraph Developer Conference, chief scientist of Hedera, Dr. Leemon Baird has announced that hashgraph consensus algorithm has been validated as asynchronous Byzantine Fault Tolerant (aBFT) by a math proof checked by computer using the Coq system.

“This is just the beginning. Formalized methods like these, where a computer verifies a math proof of correctness, are the future of software, wherever security and trust are critical.” ( Dr. Leemon Baird )

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 the 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.

His statement has a lot of interesting implications beyond the verification of the verification and validation of the Asynchronous BFT propounded by Hashgraph. It is worth noting that post — Hashgraph, there were a few DLT platforms with DAG based data structure that claimed speed and scale of Hashgraph consensus. Hence Coq based verification of Hashgraph consensus establishes the authority and ingeniuity of Hedera approach.

As stated in various articles, an asynchronous protocol based solution of Byzantine General Problem promises immense possibilities for the future information and communication systems as eventually all Blockchain and Distributed ledgers need to interact with legacy and emerging systems beyond the security and control offered by the realms of replicated state machines in the peer to peer network architecture and the combination of cryptographic schemes. Many times, this has to be achieved even beyond the trust offered by certificate authorities and hardware security modules. An asynchronous BFT promises a secure real world integration possibility for distributed ledger technology in scale and scope. However, the invocation of a Coq based proof assistant for the protocol verification signifies another emerging trend.

A few days back I have come across an interesting research paper on verifiable data structures. This paper elucidates the construction of verifiable logs and data formats. These data structures could be used for the construction of verifiable data formats and data types with better trust.

Formalised methods and mathematical proofs are becoming the emerging benchmarks of information systems. The above statement from Dr. Leemon Baird implies the wider possibilities of what Satoshi Nakamoto has famously said in his seminal whitepaper on Bitcoin.

In Cryptography we Trust

When computer programs and proof assistants like Coq can verify the mathematical proofs related to consensus protocols, encryption algorithms, cryptographic schemes, randomness algorithms etc, it is the advent of a new world of digital trust.

You can construct a brave new world of digital trust, dynamic verification and deep validation of digital signatures, data structures, internet protocols, sensor gateways, wireless routers and so many other information systems and technologies.

The possibilites from this episode is bewilderingly astonishing. This could be the emergence of algorithmic and mathematical proof based trust models for wide spectrum of information systems.

When we consider the spectre of NP-hard computational problems, proof assistants like Coq along with the paradigms like non-interactive proofs offer the possibility of Digital Trust beyond possibilities.

Hence we could confidently proclaim …

‘In Proof based Protocols We Trust’

Note: The Author is a Hashgraph MVP and a Global Community Ambassador. However the views expressed in the article are his personal perspectives.