Formal Land

Smart contract audit

We provide audits for your Solidity smart contracts. We use formal verification to make sure we cover all edge cases.

Such audits offer the highest degree of certainty and can be relatively cheap on the long run. We recommend applying formal verification after a few dozen millions of dollars of assets under management.

Rust verification

We audit Rust code using our formal verification tool coq-of-rust. It covers almost all Rust code, including the standard library, for any kinds of properties to verify.

This will be useful if you have critical libraries or applications written in Rust, such as blockchains, operating systems, or cryptographic primitives.

Zero Knowledge audit

We have expertise in zero-knowledge systems and provide audits with formal verification for these systems. Here are some examples of our products:

• rocq-of-noir a formal verification for Noir programs
• Garden an open source library to verify circuits (Circom, ...)

Cost

We target a cost starting at $20 per line of verified code. The maintenance cost is the same, but counting the number of modified/added lines.

Our cost is $50 per line for zero-knowledge circuits.

Ethereum Foundation

We are formally verifying for the Ethereum Foundation the correctness of the revm implementation of the EVM virtual machine, according to a functional specification.

This is an ongoing project, involving the formal verification of thousands of unmodified lines of Rust code.

Tezos

The formal verification of parts of the implementation of the Tezos blockchain was our first project. It started at Nomadic Labs and Inria with the development of the verification tool for OCaml coq-of-ocaml.

It continued with the repository coq-tezos-of-ocaml and the verification of parts of the storage system and the smart contracts VM.

Aleph Zero

Thanks to the Aleph Zero Foundation we developed the two following formal verification tools:

• coq-of-rust for Rust programs
• coq-of-solidity for Solidity/Yul programs

These enable the formal verification of most of the blockchain code that is written today, either in smart contracts or L1/L2.

Sui type-checker

We formally verified a first part of the type-checker for the Move language used by the Sui blockchain. Look at some of our blog posts such as Verification of one instruction of the Move's type-checker for more information.

Rocq prover

We rely on the formal verification tool Rocq (previously named Coq) to prove the correctness of your software. Rocq is a powerful proof assistant that allows us to verify the absence of any kinds of bugs in your code.

Based on the theory of the Calculus of Constructions, Rocq was originated at the Inria research center in France and received contributions from several Universities across the world.

Automated translation

We developed several automated translation tools from various programming languages (Rust, Solidity, OCaml, Noir, Circom, ...) to the Rocq proof system.

These tools allow us to verify the correctness of your software at the source level, and to maintain the proof of correctness as the code evolves.

Open source

We believe in the strength of open source to lower the cost of formal verification and make it accessible to more people.

To look at our code visit our GitHub and our blog.

AI

Thanks to an Erasmus grant, we are working on AI solutions in the VSCode editor to help developers write Rocq proofs. See our blog post Designing a coding assistant for Rocq for more details.