Verified zkEVM program: The Ethereum Foundation program funding Lean verification of zkVMs and their proof systems
================================================================================

The 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
Category: Challenges and programs
Targets: Clean, zkLean, Halva, ArkLib, LLZK, Sail RISC-V Lean, KEVM equivalence, hax 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: Active
Strengths: Single source of truth for funded, interoperable projects. | Dated public milestones. | Independent reviews (for example of sp1-lean) published openly.
Limits: Ethereum-centric scope. | Program, not a tool. | Milestones can slip; check dates.
Firms using it: none listed
Sources: https://verified-zkevm.org | https://github.com/Verified-zkEVM/Overview | https://blog.ethereum.org/2025/12/18/zkevm-security-foundations

Source page: https://sorryfree.com/frameworks/verified-zkevm/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13