Skip to main content

Formal Land

Vitalik Buterin: Security is now the
#1 priority for Ethereum, especially formal verification of zkVMs

What is your organization doing about it?

๐Ÿ‘‰ย Contact us to verify your zkVM!ย ๐Ÿ‘ˆ We provide advanced formal verification services for Rust and the blockchain.

Our formal verification projects

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ย ๐Ÿ“š.

Rust language

Rust language

We developed the formal verification tool for Rustย ๐Ÿฆ€ coq-of-rust for the cryptocurrency Aleph Zeroย ๐Ÿ”—. We can 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

EVM

We are verifying that the two following EVM implementations:

are equivalent for every possible inputs. This would be the first time that one, and actually two, EVM implementations are formally verified.ย ๐Ÿ
This work relies on our tools coq-of-rust and coq-of-python.

More to come! ๐Ÿš€

More to come! ๐Ÿš€

We are working on another formal verification project that will be announced soon. This will help dApps to greatly reduce their risks.ย ๐Ÿง‘โ€๐Ÿš€๐ŸŒœ

Contact us

Contact us to formally verify your projects or for general discussions.