As part of its goal to deliver transparency to the development community, Seedvest has engaged third-party security auditors and assurance providers to perform independent audits of the engineering work by Seedvest development team on the platform, including the network services, as well as standardizing processes such as the implementation of stablecoins built on Seedvest to provide specific security guarantees that reduce technical complexity and create a predictable development environment.
For this report, the FP Complete team has reviewed the Seedvest platform and Seedvest network services code. Both code bases were audited initially with further differential reviews upon new revisions of the code. The source materials consist of:
The Seedvest 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 Seedvest documentation audit tech report that Seedvest platform 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.