Ethereum’s better.codes Turns ZK Security Into a Machine-Checked Research Race

The Ethereum Foundation’s Formal Verification team has launched better.codes, an open research challenge aimed at a difficult but foundational question in zero-knowledge technology: how much of the security claimed by hash-based SNARKs has actually been proved rather than assumed?

The challenge focuses on koalaIRS12, a Reed–Solomon proximity problem connected to the Proximity Prize initiative and formalized end to end in Lean through ArkLib. Participants can bring their own AI models, proof-search tools, and verification harnesses. Their goal is to prove a larger soundness lower bound inside a fixed theorem statement and parameter setting.

This changes the usual role of AI in cryptography. An agent is not being asked to produce an impressive-looking proof or a benchmark score that depends on an opaque evaluator. Each submission is checked by a comparator against the pinned theorem statement, then re-checked by the Lean kernel. Accepted results are promoted to a public repository, with the solver and the AI model credited.

The target is important because production hash-based SNARKs—including systems used by zk-rollups and zkVMs—depend on Reed–Solomon proximity gaps and correlated-agreement results. The Foundation says deployed systems commonly target 128-bit security, while the currently proven mathematical bounds do not fully reach the benchmarks researchers associate with that target. better.codes is therefore designed to narrow the gap between conjectured security and machine-checked security.

The most interesting engineering detail is the shared baseline. New lemmas, proof techniques, and impossibility results from accepted submissions are upstreamed so future participants can build on them. The leaderboard is not merely ranking agents; it is intended to make progress cumulative and auditable.

A May 2026 experience report from the Ethereum Foundation’s zkEVM Verification Project shows why this workflow is becoming practical. Researchers connected Rust-to-Lean extraction tools such as Aeneas and Hax with formal cryptographic libraries including ArkLib and CompPoly, then used AI provers to close selected obligations in Plonky3 and RISC Zero cryptographic code. The paper reports that the Lean kernel re-checks every proof, while also documenting real limitations: toolchain drift, extraction boundaries, missing lemmas, and proof tasks that still required manual work.

That distinction matters for ZK builders. better.codes does not certify every deployed prover, and it does not make an AI-generated argument trustworthy by itself. It creates a constrained, reproducible environment in which only a kernel-checked proof can improve the published bound.

The 128-bit figure is a challenge target, not a result achieved at launch. The Foundation also says that eligibility, evaluation, awards, and payments may change as the program develops. For developers, the immediate lesson is narrower but useful: formal verification is moving from isolated audits toward public, reusable proof infrastructure—and AI is being tested as a search assistant inside that trust boundary, not as the final authority.