Formal verification challenges and programs for ZK: zk.golf, better.codes, Verified zkEVM
================================================================================

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.

zk.golf: zkSecurity — 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 — Active (launched 2026-07-02)
better.codes: Ethereum 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 — Active (launched 2026-08-20)
Verified zkEVM program: Ethereum 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 — 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.

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