The Ethereum Foundation’s Formal Verification team, in a strategic partnership with research organizations Yukon and zkSecurity, has officially launched better.codes, a novel open-source autoresearch initiative. The platform serves as a high-stakes, collaborative environment where researchers and AI agents work to resolve long-standing theoretical gaps in the security of succinct non-interactive proof systems (SNARKs). By gamifying the process of formal verification using the Lean theorem prover, the project seeks to bridge the chasm between theoretical cryptographic conjectures and the rigorous mathematical proofs required for secure, production-grade blockchain infrastructure.
The Cryptographic Security Gap
At the heart of modern blockchain scalability lies the SNARK—a mathematical construct that allows one party to prove the validity of a computation without revealing the underlying data. These systems are the backbone of zkRollups and zkVMs, technologies currently enabling Ethereum to scale by processing transactions off-chain while maintaining mainnet-level security. However, these systems rely heavily on Reed-Solomon proximity gaps and correlated agreement conjectures.
While industry standards currently target 128-bit security—a threshold generally considered unbreakable by classical computing standards—this security is often based on mathematical conjectures rather than absolute, machine-checked proofs. If these underlying assumptions are found to be weaker than anticipated, the integrity of the entire cryptographic stack could be compromised. The better.codes initiative specifically targets the koalaIRS12 problem, a key challenge derived from the broader Proximity Prize research effort, to solidify these foundations.
Chronology of the Proximity Initiative
The launch of better.codes is the latest milestone in a sustained effort to formalize the mathematical bedrock of zero-knowledge proofs. Earlier this year, the Ethereum Foundation introduced the Proximity Prize initiative, a research-focused program aimed at incentivizing the academic and engineering communities to solve critical problems in list decoding and correlated agreement.
The trajectory of this effort can be traced back to the academic publication Open Problems in List Decoding and Correlated Agreement, authored by researchers Gal Arnon, Dan Boneh, and Giacomo Fenzi. This paper provided the conceptual roadmap for the challenges now being hosted on the better.codes platform. By formalizing these problems in ArkLib—a library specifically designed for Lean 4-based formal verification of knowledge arguments—the team has created a machine-readable environment where proofs can be verified with absolute certainty by the Lean kernel.
Mechanics of the Autoresearch Challenge
Unlike traditional academic research, which often unfolds in silos, better.codes employs an "always-on" model of autoresearch. The platform functions as a public leaderboard where participants, using their own AI agents and custom computational harnesses, attempt to raise the machine-checked soundness bound of koalaIRS12.
The workflow is designed for transparency and cumulative progress:
- Challenge Submission: Participants clone the repository, which contains the fixed theorem statement and the verification harness.
- Automated Verification: Once a researcher or agent develops a proof, the Lean kernel validates the result. Because the system is machine-checked, there is no ambiguity regarding the correctness of the proof.
- Upstreaming Results: Every successful submission that increases the soundness bound is promoted to the public repository. Crucially, the techniques, lemmas, and even the proofs of impossibility discovered during the process are shared. This ensures that the collective effort avoids redundant research paths and builds upon the latest breakthroughs.
This iterative, git-backed structure allows the global community to iterate on the problem in real-time, effectively crowdsourcing the path toward the 128-bit target.
Precedent and the Evolution of Open Research
The architectural philosophy behind better.codes is not entirely without precedent. The project draws significant inspiration from previous successful experiments in collaborative research, such as ecdsa.fail, zk.golf, and snark.fast. These initiatives have demonstrated that when complex cryptographic problems are framed as open, gamified challenges, they move the research frontier significantly faster than traditional, isolated academic research.
For instance, zk.golf successfully pushed the boundaries of efficient ZK circuit design, while other initiatives have drastically improved the speed of post-quantum proving systems. By adopting this "autoresearch" model, the Ethereum Foundation is effectively treating core cryptographic security as an engineering pipeline, where modular improvements are treated like code commits.
Implications for Blockchain Infrastructure
The implications of this project for the Ethereum ecosystem and the broader Web3 space are substantial. As Ethereum moves toward a post-quantum future, the reliability of hash-based SNARKs becomes paramount. Currently, most deployed systems rely on "best-effort" security benchmarks. By closing the gap between conjectured security and proven security, better.codes is essentially hardening the infrastructure that will handle billions of dollars in decentralized finance (DeFi) activity.
Furthermore, the integration of AI agents into the formal verification process represents a paradigm shift. In the past, formal verification was a labor-intensive, slow-moving discipline requiring highly specialized expertise. By providing a structured, incentivized interface for AI-assisted proving, the platform lowers the barrier to entry, allowing both human researchers and machine learning models to contribute to the mathematical verification of critical software.
Technical Hurdles and Future Outlook
The challenge of reaching 128-bit security for koalaIRS12 is significant. The problem requires finding, or proving the non-existence of, specific mathematical structures that could be exploited to weaken the proof system. As participants push the lower bound upward, the problems inevitably become more computationally expensive and mathematically nuanced.
While the current scope of better.codes is limited to the koalaIRS12 problem, the project organizers have indicated that they intend to add further challenges as the initiative matures. The eligibility, evaluation criteria, and reward structures remain flexible, managed through a program that prioritizes the advancement of the field over static rules.
For the cryptographic community, the launch of better.codes signifies a move toward a more rigorous, verifiable, and open methodology. By moving away from the era of "trusting the conjecture" and toward an era of "verifying the bound," the Ethereum Foundation is setting a new standard for how high-stakes software infrastructure should be developed and maintained.
As the platform gains traction, it is expected that a diverse array of automated solvers and human-led research teams will join the fray. Whether this collective intelligence can successfully reach the 128-bit target remains an open question, but the process of arriving there will undoubtedly yield invaluable insights into the limits of modern proof systems and the future of machine-verified mathematics. Interested parties can track the live leaderboard and contribute to the challenge at the official portal, marking a significant step forward in the quest for provably secure decentralized systems.
