Ethereum turns AI agents loose on an unproven crypto assumption

The Ethereum Foundation's Formal Verification team, working with Yukon and zkSecurity, launched better.codes on Wednesday, the team announced, a public challenge that pays anyone's AI agents to chip away at a security assumption most of Ethereum's zero-knowledge infrastructure currently takes on faith rather than proof.

Hash-based SNARKs, the proof systems behind zk-rollups, zkVMs, and a chunk of Ethereum's post-quantum roadmap, rely on something called proximity gaps and correlated agreement for Reed-Solomon codes. Deployed systems are built to hit 128-bit security, but that guarantee only holds in full if the underlying mathematical conjectures about those codes turn out to be true, and right now what researchers can formally prove falls short of what they believe. Better.codes targets one specific piece of that gap: a Reed-Solomon proximity problem called koalaIRS12, drawn from the Foundation's earlier Proximity Prize initiative and the open problems Gal Arnon, Dan Boneh, and Giacomo Fenzi laid out in a paper on list decoding and correlated agreement.

• Target security level for koalaIRS12: 128 bits, currently unproven at that strength
• Problem source: the Foundation's Proximity Prize initiative and a paper by Arnon, Boneh, and Fenzi
• Formalization tool: Lean 4, via the ArkLib library for verified arguments of knowledge
• Entry method: sign in with GitHub at better.codes and submit inside a pinned problem statement
• Prior challenges using this format: ecdsa.fail, zk.golf, snark.fast

The mechanics run through code rather than committee review. The theorem statement, parameter point, and verification harness stay fixed, and each solver submits a proof inside that pinned surface. A comparator checks that the submitted theorem matches the pinned statement exactly, then Lean's own kernel checks the proof itself, no human referee involved in either step. Accepted submissions get promoted to a public leaderboard, credited to both the solver and the specific AI model that produced the proof, and their new lemmas and techniques get folded back into the shared codebase so the next solver starts from wherever the last one left off.

A SNARK lets one party prove a computation ran correctly without making the other side redo the work or see every input, which is what lets a rollup post a single proof to Ethereum instead of every transaction it processed. Soundness is the property that stops someone from forging a proof for a computation that never happened, and it is the one property a rollup user depends on directly: if soundness fails, an attacker can convince the chain a false state transition is valid. Right now the industry runs on the belief that soundness holds at 128 bits for the codes these systems use, backed by years of cryptanalysis rather than a machine-checked proof. Closing that gap does not change how any live rollup behaves today, but it changes what a security researcher can say about it with certainty rather than confidence.

The Foundation calls this format autoresearch: instead of one team working a hard problem in isolation, many independent groups run their own AI agents against the same locked benchmark at once, and any accepted proof raises the floor for everyone still working the problem. It is the same appetite for handing AI agents open-ended, verifiable work that Generalist AI is betting on with robots that learn from a single demo, except here the task is a formal proof a machine can check line by line rather than a physical motion a camera has to judge. Today's challenge covers only the soundness bound for koalaIRS12, and the Foundation says further challenges may follow, with eligibility, evaluation, and any awards governed by program terms that can still change as the effort develops.

This piece is informational, not a recommendation to buy, sell, or hold any asset.