Challenges and programs
Live venues where verified artifacts are produced competitively or under a coordinated program: zk.golf (cheapest circuit with a Lean proof of soundness and completeness), better.codes (raise a Lean-checked soundness bound for Reed-Solomon proximity), and the Ethereum Foundation's Verified zkEVM program that funds most of the frameworks on this index.
Two 2026 launches turned formal verification into a spectator sport. zk.golf scores circuits by allocations plus constraints, but a submission only counts if its Lean proof of soundness and completeness kernel-checks in a sandbox. better.codes hands AI agents a formalised open problem from the Proximity Prize and promotes every proof that improves the machine-checked bound. Both are useful to a team that wants to learn what a verified deliverable looks like before commissioning one.
The Verified zkEVM program is the funding and coordination layer behind Clean, zkLean, Halva, ArkLib, LLZK, the Sail RISC-V Lean model, KEVM equivalence and hax's Lean backend, with a stated goal of formally verified zk(E)VMs by 2027.
Frameworks in this category
| Framework | Targets | Approach | Access | Status |
|---|---|---|---|---|
| zk.golfzkSecurity | R1CS over BN254 · GF(2) hash compression track · Clean circuits | Fixed Lean interface and specification per challenge; submissions are Clean circuits plus kernel-checked proofs; score = allocations + constraints | Open challenge; challenges repository public | Active (launched 2026-07-02) |
| better.codesEthereum Foundation Formal Verification team, Yukon and zkSecurity | koalaIRS12 proximity problem · FRI / STIR / WHIR soundness · Lean 4 | A formalised open problem from the Proximity Prize; solvers point AI agents at improving the machine-checked lower bound; every submission is kernel-checked and promoted proofs are credited | Open challenge; program terms on the site | Active (launched 2026-08-20) |
| Verified zkEVM programEthereum Foundation | Clean · zkLean · Halva · ArkLib · LLZK · Sail RISC-V Lean · KEVM equivalence · hax Lean backend | Grants and coordination for a formally verified, bug-free zk(E)VM stack, targeted for 2027 | Program; individual projects are open source | Active |
How to choose
- Learn how a sound-and-complete circuit proof is structured, or benchmark an optimisation: zk.golf.
- Contribute to or watch AI-assisted theorem proving on a real cryptographic bound: better.codes.
- Track which frameworks are funded, maintained and interoperable: the Verified zkEVM program page and its Overview repository.
Firms that do this work
zkSecurity, Galois, Veridise, Nethermind (Formal Verification team), Formal Land, Cryspen, Reilabs, Runtime Verification, Certora, Trail of Bits, Symbolic Software
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 ↗
Other categories
ZK circuit verification, Proof systems and computational proofs, Symbolic protocol analysis, Verified implementations, Proof assistants and general verifiers