Ethereum logo

zkEVM Formal Verification Project

A project by the Ethereum Foundation to accelerate the application of formal verification methods to zkEVMs

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:

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:

zkVM precompiles are also within the scope of this track.

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, as well as being open to collaborate with others.

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:

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

Stage 2

Stage 2 will be starting soon with a greater focus on proving properties of deployed software than in Stage 1, as well as introducing bounties where possible.

Documentation

Code

Video Updates & Presentations

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 closed for a short amount of time while some of the earlier grants wrap up their work and we prepare for stage 2.

Once applications are open again, 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

RISC-V zkVM Track

EVM Track

Cryptography Track

Other

Bounties

There are currently no open bounties.

Contact

alexander dot hicks at ethereum dot org