AI-powered security research launches for Ethereum
better.codes raises security bounds for hash-based SNARKs
1Launch of better.codes
The Ethereum Foundation Formal Verification team, in collaboration with Yukon and zkSecurity, has launched better.codes, an open auto-research platform. The platform is based on a Reed-Solomon proximity problem (koalaIRS12) formalized in Lean. Participants will use their own AI agents to attempt to raise the machine-verified security bounds of this problem. Each successful submission will bring the community closer to the 128-bit target.
2Background of Proximity Prize
Earlier this year, the Ethereum Foundation initiated the Proximity Prize to prove or disprove Reed-Solomon proximity gap conjectures. The grand challenges outlined by Gal Arnon, Dan Boneh, and Giacomo Fenzi include open problems in list decoding and correlated agreement. The koalaIRS12 problem in better.codes directly stems from this work and has been end-to-end formalized in ArkLib (the Lean 4 library for formally verified arguments of knowledge).
3Importance of hash-based SNARKs
Nearly all production hash-based SNARKs, from those securing zkRollups and zkVMs to those central to Ethereum's post-quantum roadmap, rely on proximity gaps and correlated agreement for Reed-Solomon codes. Current proofs fall short of what researchers believe the security benchmarks might be. The 128-bit security target can only be fully guaranteed if the conjectures hold true.
4Open collaboration model
better.codes offers a new open collaboration model where participants can run their own AI models and tools in parallel against a common verified benchmark. Since no single agentic setup is optimal for an open problem, multiple independent setups working on the same benchmark can advance the frontier faster than any single team. Open challenges like ecdsa.fail, zk.golf, and snark.fast have already pushed research boundaries in quantum circuit design and verified ZK circuits.
5Participation process
Participants can sign in to better.codes with GitHub and clone the challenge repository. The theorem statement, parameter point, and verification harness are pinned; solvers work within a designated submission surface to prove a larger soundness lower bound. A comparator checks that each submission's exported theorem exactly matches the pinned statement, while the Lean kernel verifies the proof. Accepted results are promoted to the public repository with credit given to the solver and the AI model used.
6Transparency and collaboration
Submissions are transparent and git-backed. New lemmas, proof techniques, and impossibility results are upstreamed, allowing anyone to review past diffs and submission notes, build on prior work, and avoid dead ends. This aims to incrementally advance progress for all solvers and agents. better.codes seeks to bridge the gap between conjectured and proven security benchmarks through open, incremental, verifiable, and public research.
7Next steps
Today's launch focuses on the soundness challenge to raise the proven lower bound for koalaIRS12 to 128 bits. Additional challenges may be added over time. Eligibility, evaluation, awards, and payments are governed by program terms and may be adjusted as the challenge progresses. better.codes aims to contribute to the advancement of post-quantum Ethereum. Such open research models could herald a new era in solving complex cryptographic problems.
8Industry implications
The proliferation of auto-research platforms like better.codes could drive significant advances in blockchain security and post-quantum cryptography. Ethereum's initiative may serve as a model for other blockchain projects. Open collaboration models can enhance research efficiency, enabling faster development of innovative solutions. These platforms may pioneer new standards at the intersection of AI and cryptography.