🦚 About

We started in 2021. We specialize in formal verification, that is to say the exhaustive testing of programs, with a focus on the blockchain industry. We develop innovative solutions 🚀 to verify code that was unverifiable before. Most of our code is eventually open-sourced and relies on the proof assistant Coq 🐓.

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 Coq 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 contrast with manual code audits where you must redo all the verification work for 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,
• coq-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).

If you want to make your code safer and work with us, email us!