# π¦ 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!