Ethereum Foundation Opens AI Proof Challenge to Close a Known Security Gap in ZK Systems
The Ethereum Foundation has launched *better.codes*, a publicly accessible challenge asking participants to use AI agents to formally verify the soundness of hash-based SNARKs. The challenge is closely tied to a December 31, 2026 deadline the EF has labeled "H-star," the date by which all zkEVM teams competing for Ethereum L1 integration must achieve 128-bit provable security.
Published August 20, 2026, the challenge was announced by the EF's Formal Verification team in collaboration with Yukon, a collaborating organization, and zkSecurity.
It asks developers, researchers, and automated systems worldwide to submit machine-checked proofs in Lean 4, a proof assistant whose kernel accepts or rejects every submission cryptographically.
The goal is to raise the provably demonstrated soundness of hash-based SNARKs to 128 bits, a threshold that production zkRollup systems have long claimed but not yet formally established.
The Gap Between "Assumed" and "Proven"
Hash-based SNARKs are the cryptographic backbone of all major zero-knowledge virtual machines and rollups, including those running on Starknet, zkSync, Scroll, and Polygon.
Their security depends on a property called the proximity gap, which creates an all-or-nothing test: either a proof evaluation is overwhelmingly valid, or it almost certainly fails. This is what allows a verifier to reliably reject fraudulent proofs.
For years, teams deploying these systems assumed that proximity gap conjectures held at their theoretical limits, which would guarantee 128-bit security at standard parameters.
That assumption has come under pressure. A 2025 paper by Giacomo Fenzi of EPFL (IACR ePrint 2025/2197) found that the actual provable success probability for an adversary against typical deployed configurations is roughly 2 to the power of negative 116.5, approximately 11.5 bits short of the 128-bit target. Fenzi also serves as one of the three judges of the $1,000,000 Proximity Prize that better.codes feeds into as a formal sub-challenge, described further below. He is, in other words, both the researcher who documented the security gap and a judge of the prize designed to close it; the source material does not identify this as a conflict of interest, but readers should be aware of the relationship.
No deployed system was immediately broken, but the gap between what has been conjectured and what has been proven is now measurable and documented.
Separately, researchers Elizabeth Crites and Alistair Stewart of the Web3 Foundation published a result (IACR ePrint 2025/2046) disproving three distinct conjectures directly targeted by the Proximity Prize: the correlated agreement up-to-capacity conjecture; the mutual correlated agreement (MCA) conjecture, which underpins WHIR; and the list-decodability up-to-capacity conjecture, which underpins DEEP-FRI.
The Web3 Foundation described their finding in a post on X as a "breakthrough result" that "disproves a class of mathematical conjectures relevant for the security and efficiency of many deployed SNARKs."
How the Challenge Works
Better.codes is structured around a single formalized problem called koalaIRS12 (a problem identifier drawn from the challenge codebase), a self-contained Reed-Solomon proximity problem drawn from the Proximity Prize research effort and encoded in Lean 4.
Participants sign in with a GitHub account, clone the repository, deploy their own AI models and automated proving harnesses, and submit proof improvements. Every contribution is verified cryptographically by the Lean kernel. Successful lemmas are merged into the public codebase so subsequent participants can build on them. The formal work is conducted within ArkLib, a Lean 4 library for formally verified arguments of knowledge.
The EF is explicitly framing this as "open autoresearch," meaning participants are expected to deploy AI agents rather than work manually.
The foundation has already demonstrated the approach is viable at low cost: according to CryptoSlate, EF researchers used AI to prove a complex lemma in hash-based SNARKs for $200 in eight hours.
zkSecurity, one of the collaborating organizations, has been building a formally verified zkEVM in Lean 4 for the EF and developed Clean, an embedded domain-specific language for writing ZK circuits targeting AIR arithmetization. Their involvement extends that work into the proof-system soundness layer.
The $1,000,000 Proximity Prize, which better.codes feeds into as a formal sub-challenge, is judged by Dan Boneh of Stanford, Giacomo Fenzi of EPFL, and Gal Arnon of Bocconi University. Fenzi is also the author of the 2025 soundness paper cited earlier in this article, the work that first quantified the 11.5-bit gap the challenge is designed to close.
Regional Stakes Are Real
The December 31 deadline, which the EF has labeled "H-star," carries concrete consequences. All zkEVM teams competing for Ethereum L1 integration must reach 128-bit provable security by that date, with proof sizes under 300 KB and formal security arguments for their recursion topology.
"Speed is no longer enough," according to CryptoSlate's reporting on the EF's stated position.
For developers outside the United States, this matters in practical terms. India is now the world's leading source of new blockchain developers, having overtaken the US, and Asia accounts for 32% of global blockchain developer activity as of mid-2026.
South Asian and African developers building on STARK-based infrastructure (a class of hash-based SNARKs) for remittances, stablecoin settlement, and digital identity are directly exposed to the soundness assumptions being challenged here. Africa is a substantive stakeholder in this outcome: peer-to-peer crypto volumes are significant across Nigeria, Kenya, and South Africa; stablecoin corridors serve cross-border remittances at scale; and ZK-based government identity frameworks are in active development across the continent.
ZK rollup transaction costs dropped roughly 85% following Ethereum's Dencun upgrade, and volume grew approximately fivefold as a result.
That volume runs on the same proof systems better.codes is trying to formally secure.
The open, GitHub-based structure of the challenge is significant for resource-constrained teams. Institutional affiliation is not required. A developer in Bangalore, Lagos, or Karachi with access to a Lean 4 environment and some compute can contribute directly.
What Comes Next
The EF confirmed that real-time proving for zkEVMs crossed a practical milestone on December 18, 2025, when 99% of mainnet blocks were proven in under 10 seconds.
The remaining open question is whether the security foundations of those proofs can be formally verified before the H-star deadline.
With better.codes, the EF is distributing that research task across a global community, backed by AI tooling and machine verification. The open autoresearch model is presented as complementary to existing academic work, expanding who can contribute rather than bypassing the research that has come before.
Whether open autoresearch can close an 11.5-bit gap in approximately four and a half months is the central question the challenge is designed to answer.