Project Overview
The Ethereum Foundation is running this project to obtain the highest possible level of assurance for zkEVMs, the end goal being bug-free zkEVMs. The project has supported work through grants. Grant applications are closed.
This project aims to:
-
Develop and apply state-of-the-art formal verification methods to the zkEVM stack, developing tooling, standards, and maintenance processes along the way;
-
Raise awareness of formal verification methods applied to zkEVMs;
-
Increase coordination between different teams in the ecosystem.
Format and Philosophy
This is a community project, with the aim of benefitting from existing ecosystem expertise as well as developing it.
Different problems have different solutions, and sometimes several good solutions are available. We aim to support different approaches to benefit from the diverse set of tools and expertise in the ecosystem, as well as to compare different approaches in terms of not only their end results but also the effort required to produce and maintain them. Shared methods/languages for interacting components are preferred. A high standard of openness and documentation is expected to facilitate evaluation and collaborative work on complex projects.
As zkVMs evolve, there is a crucial need for maintainability and extensibility. We aim to support development and the push for greater performance, not slow it down.
Tracks
The work is organized around three primary tracks. Explore each track's scope, awarded grants, and related resources:
zkVM
Verification of zkVM arithmetizations against the official RISC-V Sail semantics.
EVM
Verifying that the EVM guest program executed inside a zkVM correctly implements the EVM specification, with the assurance carried down to the RISC-V the prover actually runs.
Cryptography
Verification of proof systems, security arguments, and cryptographic components used by zkVMs and zkEVMs.