zkEVM Formal Verification Project

Project Overview

The Ethereum Foundation is launching this project to obtain the highest possible level of assurance for zkEVMs, the end goal being bug-free zkEVMs. This project will feature a combination of grants and bounties, with the project taking place until the end of 2026.

This project will also aim to:

• Raise awareness of formal verification methods applied to zkEVMs, document their application, and increase their use.
• Increase the coordination between different teams working in this ecosystem to work on an important problem.
• Develop tooling and standards of maintenance and extensibility as the verification targets will continue to evolve, and investigate how to better integrate formal verification methods in the software development and maintenance processes.

This project focuses on RISC-V zkVMs on which an EVM compiled to RISC-V can run (producing a zkEVM) and will be divided into three tracks.

RISC-V zkVM Track

The goal of the RISC-V zkVM track is to be able to verify the arithmetization of RISC-V zkVMs; that is, that the polynomial constraints exactly encode RISC-V instruction semantics, based on the official Sail RISC-V specification , and can be shown to satisfy

• Correctness: polynomial constraints guarantee the existence of an execution trace.
• Soundness: if the prover proves something, the result holds.
• Completeness: if something holds, the prover can prove it.

EVM Track

The goal of the EVM track is to be able to show that an EVM running on RISC-V correctly implements the EVM specification.

To be considered a good candidate for verification, an implementation of the EVM must be performant and compilable to RISC-V zkVMs. Extractions from formal models of the EVM, if performant, can also be considered.

Cryptography Track

The goal of the Cryptography track is to verify the specification, proofs of security for the expected security parameters, and implementation of the proof systems and other cryptographic primitives used by zkVMs.

Format

Supporting different approaches

We will support different approaches where possible to benefit from the varied expertise within the community and to make it possible to compare different approaches and to learn what works best for different components in terms of, for example, effort required, maintainability and ability to support external contributors.

If it becomes clear after a stage that one approach is better than the others, then we may focus solely on maintaining the results of that approach when moving on to the next stage. In cases where it would be advantageous to have the same method or language used for two tasks related to components that interact with each other, and it is possible to do so, this will be taken into account. Similarly, languages with a more active community (e.g., Lean and Rocq for interactive theorem proving) look more attractive maintenance-wise.

Maintenance

RISC-V zkVMs, the EVM, and the cryptographic proof systems used are still evolving so the ability to maintain and extend work (including by external contributors), rather than performing one-off proofs, is crucial. This project does not aim to slow down the development of zkVMs or require code freezes. Instead, it aims to provide tools and methods that can be used to verify the correctness of zkVMs and to help maintain and extend these verifications as the zkVMs are updated, supporting their progress.

Openness and collaboration

Everyone working on this project will contribute towards a common end goal. Accordingly, a high standard of openness is expected. This includes documenting work to facilitate its evaluation and use by others and being open to collaboration.

Stages

This project will be split into several stages. These are not strictly limited (i.e., work started in Stage 1 may overflow into Stage 2) but are intended to reflect current priorities and milestones of the project as it progresses.

Stage 1 (ongoing)

The goal of Stage 1 is to start from the ground up and establish maintainable and extensible frameworks that will allow us to formally verify specific artefacts later in the project.

Applications are particularly welcome (but not restricted to) to address the following:

• (RISC-V zkVM track) An extraction from SAIL to Lean to be able to use the existing SAIL formal RISC-V specification in Lean. (There already exists support for SAIL to Isabelle, HOL4, and Rocq.)
• (RISC-V zkVM track) Frameworks to formally verify properties of circuits and arithmetizations.
• (RISC-V zkVM track) Frameworks to formally verify zkVM precompiles.
• (EVM track) Approaches to formally verify EVM implementations. (Note: there is currently limited scope for this given that the EVM used by zkVMs is primarily revm.)

For work related to formalizing proof systems, please see zkLib.

Stage 2

Grants

Application requirements

All applications must have a written proposal in PDF format addressing the following details:

1. Proposal overview

   1. Proposed work, including goals, approach, and expected outcomes. Proposals should clearly explain what the proposal's target is and what a successful completion of the work would enable.
   2. Chosen methods and tools.
   3. Challenges, risks, and expected caveats.
   4. Timeline, including possible milestones. Do you need some other work to be completed (by yourself or others) before beginning your proposed work?
   5. Team composition.
   6. Costs.

2. Technical approach

   1. Breakdown of technical tasks.
   2. References to relevant work.

3. Project management

   1. Plans for coordination and communication about your work.
   2. Approach to maintaining or extending your work and enabling external contributions to facilitate this.
   3. Planned resource allocation (human and financial).

4. Team

   1. Background and expertise of your team members.
   2. Track record, including public repositories and published work relevant to your proposal.

Applications are open to any individuals, teams, and organizations, and will be selected for funding on a case-by-case basis. Submitting more than one proposal is allowed as long as each proposal is distinct and relevant to the project. Funding will be subject to a KYC process.

Several independent proposals may have similar goals. In such cases, it is possible for several proposals to be funded if comparing the results of different approaches to the same problem would be useful, or if several teams can work together on similar or complementary goals. Being flexible in this regard can be a plus.

If your proposal is for general tooling, please make sure to address what this will be useful for within the expected lifetime of this project (e.g., verifying a specific artefact) and how others will also be able to use it.

Applications are currently open

Proposals can be sent until further notice to [email protected]. Please note that it is often useful to discuss any ideas ahead of submitting a proposal to see how they may fit in the project, particularly with respect to previous and ongoing work, as well as planned work that may not yet be announced.

Grants Awarded

Bounties

There are currently no open bounties.

Contact