Proposal: Optimized Verified EVM Interpreters for ZK

Magicians Tooling
, , ,
1

Hello,

Here is a proposal to discuss how to make efficient EVM interpreters ready for the upcoming zkVMs, using verified compilation.

image
image1920Ă—1224 138 KB

Context

To migrate Ethereum to ZK systems, especially on the L1, security is critical. There seems to be a consensus on using all possible techniques to ensure security, including formal verification.

As of today, considerable effort has been made to formally verify the circuits and cryptographic primitives. A good page with recent projects is probably https://verified-zkevm.org/ , founded by the Ethereum Foundation.

To make the formal verification end-to-end, one also needs to formally verify the assembly code of EVM interpreters, since circuits are generally designed for RISC-V or similar ISAs and run interpreters like Revm or Ethrex, which should also be verified down to the assembly level.

What Exists

Today, it is possible to generate verified assembly code for an EVM using a compilation pipeline from an interpreter written in a formal language (Lean or Rocq) down to the assembly level, using the verified C compiler CompCert. Note that CompCert is built in Rocq but with rocq-lean-import it is possible to connect Lean and Rocq, at least on the computable terms. A modern pipeline wrapping CompCert is Peregrine.

Another project, which is still early, is to write an EVM interpreter directly in assembly (RISC-V) and formally verify that it correctly implements the EVM specification. This is the evm-asm project written in Lean.

Limitations

Some limitations or risks of the projects above are as follows, the main one being probably less efficiency:

  • Losing the existing EVM interpreters. As the main EVM interpreters today (Geth, Revm, Nethermind, …) are not written in a formal language, and the techniques above require it, we would lose these existing codebases. This includes all the work that has been put into these in terms of reliability and efficiency. Maybe this is “sink cost fallacy”, but it creates risk to disable these code bases.
  • Efficiency. Compilers and programming languages such as Rust contain many constructs (memory-manipulation primitives) and optimization passes that make code more efficient, which would be lost or need to be reinvented. This is critical, as a 2x increase in the EVM interpreter’s execution speed translates to a direct 2x increase in zkVM speed.
  • Maintainability. Today, EVM interpreters are written using programming languages. With the approaches above, one would need to understand a formal language that is generally less accessible. For the evm-asm approach, there is also the additional maintenance cost of assembly code, even if it is macro-generated.
  • Diversity. This is related to the previous points; we would converge on having only one or two EVM interpreters written in Lean or Rocq, fewer than the many different implementations available today.

Solution

Our proposition is to develop formally verified compilers for the main languages used to implement EVM interpreters, starting with Rust, which has been a popular choice to date for running programs on top of zkVMs.

Some ingredients are:

  • Building on top of the semantics of rocq-of-rust, extending the formalization of Revm which currently covers the core of it (funded by a grant from the EF)
  • Following the verifying compiler approach rather than the verified compiler, meaning modifying the Rust compiler so that it generates a formal proof of equivalence artifact in addition to assembly code. This is generally simpler, as one does not need to cover the general case, which is often where many corner cases are. Backward compatibility with the Rust compiler can be checked by comparing the generated binary code.
  • Using CompCert as a backend instead of LLVM to start with. It contains fewer optimizations, but we can switch to LLVM later once it is verified.
  • Following the proof strategy outlined in the paper RustCompCert, in particular for the borrow checker. A question can be, why not use it directly? It is not complete yet at the time of writing and might take time to reach parity with the official Rust compiler, especially since it is a verified compiler, but maybe I am wrong.
  • Like for any new projects today, leveraging AI for all the heavy work of making equivalence proofs.

Next

We do not have concrete plans yet, other than working on the project ourselves over the summer. We are happy to discuss what you think about it!

1 Like