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 distributed across several stages over the next 18-24 months.

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.

The scope of this project is restricted to 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 that a RISC-V zkVM correctly implements a RISC-V CPU and the correctness of the arithmetization and circuits, specifically:

That a circuit is not under-constrained or over-constrained, and performs the correct computation.
The correctness (polynomial constraints guarantee the existence of an execution trace), soundness (if the prover proves something, the result holds) and completeness (if something holds, the prover can prove it) of the arithmetization.

Formally verified precompiles are also within the scope of this track given that they are treated like extensions to the zkVM.

Choice of RISC-V specification

The current standard in existing RISC-V zkVMs is the RV32I base integer instruction set. The M extension for integer multiplication and division is also typically used, and the ability to support other extensions is expected.

Choice of arithmetization

The aim is to be flexible concerning choices of arithmetizations, but support for AIR (as required by Circle STARKs) is expected.

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.

Choice of EVM implementation

To be considered a good candidate for verification, an implementation of the EVM must be performant and compilable on RISC-V zkVMs; for example, revm/Reth. 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 cryptographic primitives and protocols used by zkVMs.

Choice of PCS and PIOP

Current RISC-V zkVMs currently primarily rely on FRI + Circle STARks (wrapping into Groth16 or Plonk for on-chain verification), making this our focus, although it does preclude considering alternatives.

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 Coq 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.

Openness and collaboration

Everyone working on this project will contribute towards a common end goal so 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 different focuses and milestones as the project advances.

Stage 1

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

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 Coq.)
(RISC-V zkVM track) Frameworks to formally verify properties of circuits and arithmetizations.
(RISC-V zkVM track) Frameworks to obtain formally verified precompiles that can be re-used by different RISC-V zkVMs.
(EVM track) Approaches to formally verify EVM implementations running on RISC-V.

The Cryptography track is not a priority at this stage, although there is an overlap with precompiles, but work that can establish the basis required to later verify the desired PCS and PIOP may be considered.

Stage 2

Stage is expected to begin in the beginning of early 2025 and build upon the work completed in Stage 1, with a greater focus on proving and bounties where possible.

Grants

Application requirements

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

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.
Technical approach
1. Breakdown of technical tasks.
2. References to relevant work.
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).
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 for Stage 1 are now open

Proposals for Stage 1 can be sent until further notice to [email protected]. The application review process will begin on September 16, 2024.

Bounties

There are currently no open bounties.

Contact

alexander dot hicks at ethereum dot org