
Formal Land
Formal verification services for software
Ship Bug-Free Code with Mathematical Certainty!
Prove your software systems are correct โ no edge cases, no surprises.
Tired ofโฆ
- Debugging complex systems for months?
- Missing edge cases in safety-critical code?
- Wasting resources on post-deployment fixes?
Formal Land develops technologies to eliminate these risks.
Services
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.
Case studies
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.
Technologies
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.
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.