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
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 📚.
Contact us!
If you want to audit your codebase with formal verification (Solidity, Rust, Go, OCaml) or for any other questions, contact us!