The Ethereum Foundation Formal Verification team has launched better.codes, an open autoresearch challenge developed with Yukon and zkSecurity. Participants can bring their own AI models, agent harnesses and tools to improve the proven soundness bound for koalaIRS12, a Reed–Solomon proximity problem connected to research on modern succinct non-interactive proof systems.
The defining feature is machine-verifiable progress. The theorem statement, parameter point and verification harness are pinned in advance, and every submission is checked by the Lean kernel. When a proof is accepted, it raises the public lower bound measured in bits and becomes part of the shared research base that other solvers and agents can build on. The current challenge is aimed at moving the proven bound toward a fixed 128-bit target.
better.codes is structured as a parallel open research environment rather than a single closed team effort. Independent participants can run different agentic setups against the same formal benchmark. New lemmas, proof techniques and even documented dead ends are upstreamed so later attempts can reuse successful ideas and avoid repeating approaches that have already failed.
For Ethereum, the experiment fits into a broader effort to strengthen formal foundations for cryptographic constructions used in ZK systems and the network's post-quantum roadmap. The project does not treat AI output as trustworthy by itself: correctness is anchored in the formal theorem and Lean verification. The central idea is to combine broad agent-driven exploration with a strict machine-checked acceptance boundary.