Skip to main content

🦚 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:

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