Web3
Audit Reports
Here are audit reports about formal verification works we have done for blockchain projects:
- Ethereum Foundation: formal specification of Revm (2026)
- Ethereum Foundation: Keccak hash function verification (2025)
- Ethereum Foundation: Branch equality verification (2025)
- Ethereum Foundation: LLZK verification (2025)
- Sui: the type-checker for Move (Rust)
- Smoo.th elliptic curve library (Solidity)
- Aleph Zero:
rocq-of-rustandrocq-of-solidity(Rust/Solidity) - Tezos: parts of the L1 (OCaml)
Working with us
We propose formal verification engagements for projects where stronger assurance is needed, including Rust, Solidity, ZK circuits, and other codebases that can benefit from our proof-oriented tooling and workflows.
Engagements can take the form of:
- a one-time audit to verify your code at a specific point in time,
- a subscription to verify your code as it evolves,
- consulting to train you to use our tools or formal verification in general.
We use formal verification and interactive theorem proving to cover software behaviors that are difficult to validate exhaustively with tests alone.
The output is a machine-checked proof for specified properties of the software under review.
Our verification process can follow code changes to re-check only what changed. This means that verification work can remain useful across releases instead of being recreated from zero each time.
Our tools are open source, documented, and available on our GitHub. We rely on the proof system Rocq so that the verification work remains inspectable and maintainable on your side as well.
The typical price for our subscription is $20,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.