🛡️ Audit Reports
Reports
Here are reports about formal verification works we have done, using the 🐓 Coq proof system:
- Sui: the type-checker for Move (ongoing, Rust)
- Smoo.th elliptic curve library (Solidity)
- Aleph Zero:
coq-of-rustandcoq-of-solidity(Rust/Solidity) - Tezos: parts of the L1 (OCaml)
Get Started
We propose code audits with formal verification for Solidity/Rust/Go projects (L1, L2, and smart contracts) as:
- a one-time audit to verify your code at a specific point in time, for $20 per line of code,
- a subscription to verify your code as it evolves,
- consulting to train you to use our tools or formal verification in general.
We offer start-of-the-art security with formal verification and interactive theorem proving to cover all possible code executions for any forms of user/security requirements.
Even state actors cannot break security properties as the protection is a mathematical proof checked by a computer 🦸.
Our verifications process follows code changes to verify only what changed. This means that you save money 💰 compared to traditional audits, where you have to review everything for each release.
Our tools are open source, documented, and available on our GitHub. We rely on the proof system Coq 🐓 which is one of the most widely taught proof systems across the world 🌏, so that you can maintain our work on your side.
The typical price for our audit subscription is $15,000 per month, for one engineer available full time for your project to specify and formally verify your code. You can stop the subscription at any time or have someone half-time for half the price.