Audits and Standards

As part of its goal to deliver transparency to the development community, Hedera has engaged third-party security auditors and assurance providers to perform independent audits of the engineering work by Hedera’s development team on the platform, including the network services, as well standardizing processes such as the implementation of stablecoins built on Hedera to provide specific security guarantees that reduce technical complexity and create a predictable development environment.

FP Complete: Hedera Services and Hashgraph Platform Audit

For this report, the FP Complete team has reviewed the Hashgraph platform and Hedera network services code. Both code bases were audited initially with further differential reviews upon new revisions of the code. The source materials consist of:

FP Complete: Hedera Token Service Code Audit

For this report, the FP Complete team has reviewed the Hedera Token Service, which is part of the Hedera code base. The source materials consist of:

Quantstamp: Stablecoin Framework

Hedera and its ecosystem partners began with a specification, based on the Interwork Alliance (IWA) Token Taxonomy Framework (TTF), and incorporated enterprise requirements that focus on compliance. The specification was then formally verified for correctness, as well as audited by Quantstamp. This level of rigor enables issuers using the specification, formal verification, and audit to insure the security of the stablecoin and avoid costly errors that lead to hacks or locking of funds.

Carnegie Melon: Hashgraph Coq Proof

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.