ZK Proof Security Gets a Public Benchmark: better.codes Makes Soundness Progress Machine-Checkable

A new Ethereum Foundation research challenge is changing how progress on ZK security can be measured. better.codes asks researchers—and the AI agents they build—to raise the machine-checked soundness bound of koalaIRS12, a Reed–Solomon proximity problem connected to modern hash-based SNARKs.

The challenge went live on August 20, 2026, through the Ethereum Foundation’s Formal Verification team, in collaboration with Yukon and zkSecurity. Instead of asking participants to publish an informal claim or a benchmark number, it gives them a pinned theorem statement, parameter point, and verification harness. Submissions must export the expected theorem, and the Lean kernel checks the proof before a result can be promoted.

That distinction matters because many hash-based proof systems rely on coding-theoretic assumptions about proximity testing and correlated agreement. These assumptions help a verifier determine whether data is close to a valid codeword. If an adversary can supply data that passes those tests while remaining meaningfully invalid, the resulting soundness analysis weakens.

The Ethereum Foundation says deployed systems commonly target 128-bit security, while some of the underlying bounds are still stronger as conjectures than as machine-checked theorems. better.codes is designed to make that gap visible. Each accepted improvement is scored in bits, recorded in a public repository, and accompanied by the lemmas, proof techniques, or impossibility results that produced it.

The challenge is also a notable use of AI in cryptographic research. Participants can point their own models and agentic toolchains at the same formal problem, but the agents do not get to define success. The shared Lean checker does. That creates a useful boundary: AI can search for tactics, constructions, and proof ideas, while a small trusted kernel decides whether the submitted argument type-checks.

The formalization is connected to ArkLib, an open-source Lean library from the Verified-zkEVM project. ArkLib describes itself as a modular framework for formally verifying succinct non-interactive arguments of knowledge. Its stated goals include executable protocol specifications and machine-checked completeness and knowledge-soundness proofs for components such as sum-check, FRI, WHIR, and related coding-theory primitives.

For ZK builders, the practical lesson is not that a new proving system is ready to deploy. It is that security claims are gradually becoming auditable artifacts. A protocol team can ask which theorem supports a claimed soundness level, which assumptions remain conjectural, and whether the formal statement matches the implementation’s parameters.

There is an important limit. The 128-bit figure is the challenge’s target, not a reported result. A stronger formal bound for koalaIRS12 would improve confidence in one component of a proof-system analysis; it would not, by itself, prove the security of every SNARK, zkVM, circuit implementation, compiler, or deployment that uses related ideas. Zero-knowledge privacy is also a separate property from soundness and is not what this benchmark measures.

That separation is the real development to watch. As ZK systems move into production, the most valuable progress may be less visible than faster proving: public benchmarks that show exactly which parts of the security argument are proved, which are assumed, and which still need work.