Skip to main content

Formal Land

Formal verification for blockchain

Our references: Tezos, Aleph Zero, Sui

We build tools and services to make sure 💯 your code contains no vulnerabilities 🐞 or bugs, thanks to mathematical proofs 📐.

This is state-of-the-art security🦸: no state agencies can break this protection.

Our current and past projects

Solidity verification

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

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

EVM implementation

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

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

L1 of Tezos

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 📚.

Contact us!

If you want to audit your codebase with formal verification (Solidity, Rust, Go, OCaml) or for any other questions, contact us!