Ethereum researchers are testing a useful division of labour for AI: let agents search for mathematical advances, but let a proof checker decide what counts. Two weeks after the Ethereum Foundation launched better.codes, its public leaderboard showed 57 promoted submissions from 19 solvers and a proven lower bound of 67.67 bits for its first challenge, checked on 3 September.
That is measurable progress on a narrow cryptographic problem. It is not evidence that Ethereum itself has become quantum-safe, nor that an AI model can be trusted to review arbitrary protocol code.
The challenge asks participants to use their own AI agents and tools to improve a formal proof about koalaIRS12, a Reed–Solomon proximity problem. These coding-theory problems matter because hash-based SNARKs used in zero-knowledge systems depend on assumptions about proximity gaps and correlated agreement.
Each submission works against a pinned theorem statement and verification harness. A comparator checks that the exported theorem matches the required statement; the Lean kernel then checks the proof. Accepted work is promoted to a public Git repository, where later participants can inspect and build on it.
This changes the role assigned to the model. The agent is not the authority. It is a search process that proposes proof steps. Acceptance comes from a small, deterministic proof-checking kernel rather than another model grading whether an answer looks convincing.
At the time of our check, better.codes displayed a current interval of 67.67 to 116.13 bits and described the provable soundness gap as 7.678% narrower. The live figures are leaderboard results for the koalaIRS12 benchmark, not a security rating for Ethereum.
The repository makes the limitation explicit: its score is a spot-check quantity induced by a certified threshold radius, “not a full-protocol security claim”. That distinction matters. A stronger bound improves the evidence around one building block; it does not automatically establish end-to-end security for a rollup, zkVM or blockchain.
The wider research problem also predates this contest. A 2026 paper by Gal Arnon, Dan Boneh and Giacomo Fenzi catalogues open questions in list decoding and correlated agreement for Reed–Solomon codes. The Ethereum Foundation’s Proximity Prize offers awards for resolving those broader challenges. better.codes turns one self-contained part of that work into an always-on, machine-checkable target for agent-assisted research.
For teams applying AI to security work, the important design choice is the acceptance boundary. “An agent reviewed it” is weak evidence. A stronger workflow pins the task, constrains what may change, runs a deterministic verifier, preserves every accepted diff and labels exactly what the result covers.
The same pattern will not fit every security question. Many audits depend on ambiguous specifications, system context and adversarial judgement that cannot yet be reduced to a proof kernel. Even here, better.codes has not closed the target: the displayed lower bound remained well below 128 bits at our check.
The project is still early, but its evidence is unusually inspectable. The next useful signal is not how many agent runs are attempted. It is whether promoted, kernel-checked submissions continue to raise the lower bound—and whether those advances survive review by cryptographers outside the challenge team.
Leaderboard figures checked 3 September 2026 at 03:21 UTC. CryptoWeekly will update this brief if the displayed bound changes materially.
Subscribe to stay informed and receive latest updates on the latest happenings in the crypto world!
Subscribe to stay informed and receive latest updates on the latest happenings in the crypto world!
