Formal Land

Solidity verification

We provide a formal verification tool for Solidity called coq-of-solidity. You can now express and verify any property about a smart contract using the proof assistant Coq 🐓.

With coq-of-solidity, you can prove the absence of bugs in your code and go further than with code audits. This tool is open-source, and we can help you set it up on your project.

Rust verification

We developed an open-source formal verification tool for Rust 🦀 coq-of-rust with the cryptocurrency Aleph Zero 🔗. You can now very arbitrarily large Rust programs, thanks to the use of the interactive theorem prover Coq 🐓 and our support of the Rust's standard library.
We are now improving our reasoning principles for Rust, in order to make the verification process more efficient 🏎️.

EVM implementation

To add more trust to the L2s built on top of Ethereum, we are proving the equivalence of the two EVM implementations:

• revm in Rust 🦀
• execution-specs in Python 🐍

This work relies on our tools coq-of-rust and coq-of-python.

L1 of Tezos

We formally verified 🔍 the code of the layer 1 of the security-focused blockchain Tezos. This is a significant achievement as no other blockchains have done that, verifying models of the implementation at best.
We covered a codebase of more than 100,000 lines of OCaml 🐫 code, including the storage system and the smart contracts VM, thanks to our innovative tools and methods. See the blog of the project for more details 📚.