Verified zkEVM program
Direct answerThe Verified zkEVM program is the Ethereum Foundation initiative that funds and coordinates most of the ZK verification tooling on this index: Clean (zkSecurity), zkLean (Galois), Halva (Nethermind), ArkLib, LLZK (Veridise), the Sail RISC-V Lean model, KEVM equivalence work (Runtime Verification), VCV-io and hax's Lean backend (Cryspen), with a stated goal of formally verified zk(E)VMs by 2027.
- Maintainer
- Ethereum Foundation
- Website
- https://verified-zkevm.org
- Repository
- https://github.com/Verified-zkEVM/Overview
- Category
- Challenges and programs
- Targets
- CleanzkLeanHalvaArkLibLLZKSail RISC-V LeanKEVM equivalencehax Lean backend
- Approach
- Grants and coordination for a formally verified, bug-free zk(E)VM stack, targeted for 2027
- Access
- Program; individual projects are open source
- Status (2026-09-13)
- Active
What Verified zkEVM program does
The program's December 2025 security roadmap sets dated targets: soundcalc integration by February 2026, 100-bit provable security by May 2026, 128-bit security and a formal soundness argument for recursion by the end of 2026. Its Overview repository is the best single map of who verifies what.
Where it is strong
- Single source of truth for funded, interoperable projects.
- Dated public milestones.
- Independent reviews (for example of sp1-lean) published openly.
Limits and caveats
- Ethereum-centric scope.
- Program, not a tool.
- Milestones can slip; check dates.
When to choose it
Read the Overview before choosing a framework; alignment with the program is the strongest predictor of maintenance and interoperability.
Who works with Verified zkEVM program
No firm on this index lists Verified zkEVM program as a core tool yet; the firms below cover the same problem class.
Top-listed for verified-circuit work: zkSecurity
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website