Skip to main content

🦚 About

We started as a company in November 2021, and are now a team of five people. We work primarily on the formal verification of the crypto-currency Tezos. We made and use the translator coq-of-ocaml from the OCaml language to the proof system Coq. This allows us to verify properties about the kernel of Tezos, composed of around 100,000 lines of code. We publish our results on the website of the project coq-tezos-of-ocaml.

If you want to make your software safer or work with us, contact us.