About

We started in 2021. We specialize in formal verification for critical software. Our current public case studies are concentrated in blockchain and financial infrastructure, but our methods apply more broadly to embedded, systems, and other high-assurance software. Most of our code is eventually open-sourced and relies on the proof assistant Rocq.

Exhaustively testing a program is a difficult task, as the set of possible program inputs is generally infinite. With formal verification, we make a mathematical analysis of the code to ensure that it behaves as expected in all possible situations. As this mathematical analysis is complex, we use the proof system Rocq to make sure that our reasoning is correct. You can then replay these proofs on your computer to verify our claims. When the code changes, we can replay existing proofs to check if nothing broke. This contrasts with manual code reviews where the most rigorous work is often difficult to preserve across code upgrades.

Here are our main past and current projects:

• coq-tezos-of-ocaml for the formal verification of the code of the L1 of the Tezos blockchain,
• rocq-of-rust a tool to formally verify Rust programs,
• coq-of-python a tool to formally verify Python programs and specify the reference implementation of the EVM (the virtual machine for the Ethereum's smart contracts).

We work best on selected software components where stronger evidence is worth the cost: critical logic, high-risk libraries, infrastructure code, and verification-sensitive subsystems.

If you want to make your software more trustworthy and work with us, email us!