Ethproofs

Here is our proposal to make end-to-end formally verified zkEVMs for the next version of Ethereum. Gain Between 2x and 4x more TPS (more at the end), unlocking a huge utility increase. 🏁 Why? End-to-end formal verification is needed as security issues in ZK proofs are hard to track and can be catastrophic given the value at stake (several billion dollars on the Ethereum mainnet). Scope The EVM implementations, like Revm, with a correctness proof down to the RISC-V compiled assembly code of the interpreters. We do not cover the formal verification of the circuits and cryptographic primitives here. What exists For now, there is a verified translation from the core of the Revm implementation to the formal language Rocq through "rocq-of-rust" (our work), and a compilation pipeline, Peregrine, built on top of CompCert, to compile an EVM interpreter in Rocq to RISC-V in a formally verified way. These projects are either done or in active progress. Limitations The main limitations of relying on an EVM written in Rocq (or any formal language) are: - Speed. This is hard to beat an imperative language like Rust with a mature optimizing toolchain like LLVM. - Diversity. Leveraging existing EVM interpreters brings battle-tested solutions and enhances security through implementation diversity. Proposition Making a pipeline to compile (a subset of) Rust programs down to assembly code. This is a huge project. We also need to be able to reason on the semantics of Rust that we compile to show it is equivalent to other EVM implementations (something that "rocq-of-rust" provides for some parts). There are some ingredients to make it manageable, including AI, certifying compilation rather than certified compilation, and using a simpler Rust backend than LLVM to start with, such as CompCert. Computing the gains We estimate that, compared to an EVM implementation in a formal language (Rocq or Lean), switching to a language with explicit memory management, such as Rust, should yield a 2x performance improvement. Going all the way with LLVM verification, we get an additional 2x compared to using optimization in the formally verified C compiler CompCert. So, there is between 2x and 4x improvement based on these estimates. We assume there needs to be at least one zkVM that is formally verified end-to-end to validate each block. Thanks for reading through. Happy to discuss or collaborate on this project! 🚀