The Ethereum Foundation Formal Verification team, in collaboration with Yukon and zkSecurity, has officially launched better.codes, an innovative open autoresearch challenge designed to push the boundaries of cryptographic security. This initiative invites participants to leverage AI agents and advanced formal verification techniques to enhance the provable security guarantees of modern cryptographic systems, particularly those underpinning zero-knowledge proofs and future blockchain security.
The core of the better.codes challenge lies in tackling a formally specified problem derived from the Proximity Prize research. This problem, known as koalaIRS12, is a Reed-Solomon proximity problem that has been meticulously formalized in the Lean proof assistant. The challenge presents participants with a public leaderboard where they can submit their findings to increase the machine-checked soundness bound of this specific problem. The ultimate goal is to reach a target of 128-bit security, a standard benchmark for robust cryptographic strength.
Understanding the Significance: Why Provable Bits Matter in Modern Cryptography
The launch of better.codes is particularly timely given the increasing reliance on sophisticated cryptographic primitives for securing digital systems. Nearly all production-grade hash-based Succinct Non-Interactive Arguments of Knowledge (SNARKs) – the very systems that power zk-rollups, zkVMs, and are central to Ethereum’s long-term security roadmap, including its post-quantum cryptography strategy – depend on proximity gaps and correlated agreement within Reed-Solomon codes. These codes are fundamental to efficient and secure data encoding and error correction, which are crucial for the integrity of zero-knowledge proofs.
However, a significant gap exists between the theoretical security benchmarks that deployed systems aim for and the rigorously proven security levels. While systems are designed to offer 128-bit security, this level of assurance is contingent upon the validity of certain mathematical conjectures. The better.codes challenge aims to bridge this divide by fostering an environment of open, incremental, verifiable, and public research. By actively seeking to prove or disprove these underlying mathematical assumptions, the challenge contributes to a more robust and transparent understanding of cryptographic security.
This initiative builds upon the foundational work of the Proximity Prize, launched earlier this year by the Ethereum Foundation. The Proximity Prize is dedicated to rigorously examining the Reed-Solomon proximity gaps conjectures, with foundational research outlined in the seminal paper "Open Problems in List Decoding and Correlated Agreement" by Gal Arnon, Dan Boneh, and Giacomo Fenzi. The koalaIRS12 problem, directly sourced from this research and formalized in ArkLib (the Lean 4 library for formally verified arguments of knowledge), serves as a practical testbed for these complex theoretical challenges.
An "Always-On" Autoresearch Paradigm
better.codes represents a novel approach to open research collaboration: the autoresearch challenge. This model empowers participants to deploy their own AI agents, computational harnesses, and custom tools to work in parallel on a shared, verified benchmark. Every successful submission that incrementally raises the soundness bound contributes to a collective advancement of knowledge and security.
The rationale behind this "always-on" autoresearch model is rooted in the understanding that no single algorithmic approach or agent configuration is universally optimal for tackling complex open problems. By encouraging a multitude of independent setups to engage with the same benchmark, the research frontier is pushed forward more rapidly and effectively than any individual team could achieve. This distributed, competitive yet collaborative model has already demonstrated its efficacy in other domains. For instance, similar open challenges such as ecdsa.fail, zk.golf, and snark.fast have significantly accelerated progress in areas like quantum circuit design, verified ZK circuit development, and the optimization of post-quantum proving speeds.
The Mechanics of Contribution: How It Works
Participation in the better.codes challenge is designed to be accessible and transparent. Interested individuals can sign in using their GitHub credentials at better.codes and then clone the challenge repository. Within this repository, they will find the pinned theorem statement, the specific parameter point for the koalaIRS12 problem, and the verification harness. Solvers then work within a designated submission environment, aiming to prove a larger soundness lower bound for the problem. The success of each submission is measured in "bits" of security improvement.
A critical component of the challenge is a robust comparator that meticulously verifies each submission. This comparator ensures that the exported theorem precisely matches the pinned statement. Following this, the Lean kernel rigorously checks the mathematical proof. Accepted results are then publicly archived in the repository, with full credit attributed to the solver and the AI model they employed.
The entire submission process is transparent and git-backed, meaning all contributions and their history are publicly auditable. This transparency extends to the sharing of knowledge: new lemmas, innovative proof techniques, and identified impossibility results discovered by participants are "upstreamed" into the shared repository. This allows all solvers and agents to learn from past successes and failures, avoid redundant efforts, and build upon each other’s work. This continuous flow of information ensures incremental progress for the entire research community.
Looking Ahead: The Future of Provable Security
The current phase of the better.codes challenge is focused on achieving the 128-bit soundness bound for the koalaIRS12 problem. However, the platform is designed for expansion, with plans to introduce additional challenges over time. These future challenges will likely explore other critical areas of cryptographic research and formal verification.
Eligibility criteria, evaluation methodologies, and the structure of awards and payments are all governed by the official program terms, which are subject to adjustment as the challenge evolves. This flexibility ensures that the initiative can adapt to new discoveries and maintain its effectiveness in driving cryptographic advancements.
The ultimate aim of better.codes is to foster a global community of researchers, developers, and AI enthusiasts dedicated to strengthening the provable security foundations of our digital infrastructure. By making the pursuit of cryptographic certainty a collaborative and competitive endeavor, the challenge aims to accelerate the development of more secure and trustworthy technologies for the future.
Individuals interested in contributing to this vital area of research are encouraged to visit better.codes and explore the challenge. The platform offers a unique opportunity to engage with cutting-edge cryptography, contribute to open-source research, and be part of a movement that is shaping the future of digital security. The collaborative nature of the challenge, combined with the power of AI and formal methods, promises to yield significant breakthroughs in our understanding and implementation of secure cryptographic systems.
