We have completed a formal specification of Revm, the main Rust implementation of the Ethereum Virtual Machine (EVM), covering 94% of the EVM instructions, considering the function of their definitions. Using our tool rocq-of-rust, we translated the Rust code into the Rocq theorem prover and wrote purely functional specifications proven equivalent to the original code. In total, we produced about 50,000 lines of Rocq, and also proved the absence of panics for all covered instructions. We publish our full report: Formal Specification of Revm.

In this post, we propose a general overview of what formal verification is by decomposing it into two main steps:

• Translation of the source code to a formal language;
• Verification of the formal specification in the formal language.

We will cover the main techniques used at each step, knowing that in most cases it is possible to combine the approaches.

In this blog post, we show how we state the functional correctness of the implementation of the STATIC_CALL instruction in Revm, an implementation of the Ethereum's virtual machine EVM in Rust. This involves running rocq-of-rust to translate the Rust code to the theorem prover Rocq, and then making a proof by refinements until obtaining a specification of the code written in purely functional style, optimized for formal verification. This also proves the code cannot panic, as our specifications are free of panics.

In this blog post, we present our work to formally verify the determinism of the Keccak precompile ZK circuits in Plonky3 using our 🍀 Garden framework.

Concretely, this means that:

• This complex circuit is safe for use with all the zkVMs based on Plonky3.
• The 🍀 Garden framework is very expressive and can verify arbitrary circuits, as optimized precompiles are one of the most complex ZK circuits.

The formal verification of the determinism of ZK circuits is important, as this is one of the main sources of critical bugs in zkVMs, and these bugs cannot be found by other means, like testing, while most of the unverified zkVMs have at least one such bug.

In our previous blog post 🥷 Formal verification of an OpenVM chip, we have seen how to verify the determinism of the branch_eq chip of OpenVM. Now, we will see how to verify its completeness, meaning that it always accepts a valid witness for any possible input.

Many zkVMs are implemented in Rust, using the Plonky3 library to describe their circuits. While Rust is efficient and expressive for describing complex circuits, it is a complex language when it comes to formal verification. We present here a way to pretty-print the list of constraints generated by a Plonky3 program. That way, we will be able to import the constraints in a formal verification system like Rocq to make sure they are safe and correct.

In this blog post, we present the formal verification of the determinism of the BranchEq circuit of the OpenVM zkVM. This zkVM provides an implementation of RISC-V with Plonky3, and appears to be very fast even on a CPU.

We do our verification work using the formal verification system Rocq, showing the determinism on a model of the code. To see the other properties that can be verified, you can refer to our previous blog post 🦄 What to verify in a zkVM. We will see later how to make sure that the Rocq model corresponds to the actual Rust implementation of the circuit.

We present in this blog post the main properties that need to be formally verified in the circuits of a zkVM to consider it as secure.

The formal verification of zero-knowledge applications is considered a priority by Vitalik Buterin, the founder of Ethereum, among others. The website ethproofs.org lists zkVMs ready to run Ethereum, with formal verification of the code being one of the criteria to appear as 🟩 green.

In this blog post, we present a short introduction to Rocq, a formal verification system, as a summary of the guide Rocq in a Hurry from Yves Bertot of the Rocq team.

Rocq is the formal system that we use exclusively, but other interactive theorem provers work the same way. From this introduction, you can get a sense of how the verification of mathematical statements or security properties of programs works.

In this blog post, we present a short example about how we define reasoning rules in Rocq to formally verify the safety of zero-knowledge circuits written in LLZK.