Ethereum’s better.codes contest now measures a cryptographic proof gap that researchers can attack from both sides.
At 15:44:47 UTC on Aug. 21, the live leaderboard showed a 63.99-bit lower certificate and a 116.13-bit upper certificate for koalaIRS12. The two results left 52.14 bits unresolved after nine promoted submissions from seven solvers.
KoalaIRS12 is a fixed parameter profile for an interleaved Reed–Solomon reduction used in proof-system research. The challenge repository defines its score as a spot-check quantity and expressly excludes interpreting it as minus-log2 of whole-system soundness or as full-protocol security.
Researchers now have a public, reproducible measure of the distance between what the challenge has proved safe and what its upper certificate still rules unsafe.
What the leaderboard proves
The contest uses two tracks to close the interval.
The soundness track raises the lower certificate. At a certified radius, a successful submission proves that the benchmark’s executable reduction-error bound meets the encoded target, then maps that radius to the score displayed on the board.
The attack track lowers the upper certificate. Its theorem certifies an unsafe suffix under the benchmark’s winning-set-density condition. The repository covers that suffix directly because the formalization assumes no monotonicity theorem for winning-set density.
| Machine-checked result | Live score | Certified scope |
|---|---|---|
| Soundness lower certificate | 63.99 bits | Conservative safe point for koalaIRS12 |
| Attack upper certificate | 116.13 bits | Unsafe suffix for the same parameter profile |
| Open interval | 52.14 bits | Distance between the promoted certificates |
| Ethereum M3 requirement | 128 bits | Full zkEVM provable-security target |
The upper-certificate track’s score describes the formal boundary for koalaIRS12, while an Ethereum attack cost would require a separate whole-system analysis.
The Ethereum Foundation launch announcement says the theorem statement, parameter point, and verification harness are pinned. Each submission exports the required theorem, a comparator checks that statement against the target, and the Lean kernel verifies the proof before promotion.
An accepted result proves the submitted theorem inside that pinned environment. Production assurance must also cover the model’s completeness, the assumptions embedded in its definitions, implementation fidelity, and the composition of separately analyzed components.
The Foundation’s May review of an SP1 formal-verification effort shows why those additional layers matter. Specifications and theorem statements are code, inputs and versions need reproducible pinning, and component-level results require broader reasoning before they support conclusions about a full system.
An academic paper by Gal Arnon, Dan Boneh and Giacomo Fenzi identifies list decoding, Reed–Solomon proximity gaps, correlated agreement and mutual correlated agreement as open questions for succinct proof systems. Published before the current leaderboard snapshot, the paper explains the importance of the problem family without evaluating today’s scores.
The Foundation frames better.codes as a machine-checked research path for hash-based SNARK security. Improving the koalaIRS12 certificates would sharpen one reduction within that agenda.
The 116.13-bit certificate has the same reach: it applies to the parameter point encoded in the challenge. Other parameter choices, constructions, and system components remain separate research questions.
That two-sided movement makes the interval more informative. Every promotion changes a checkable boundary while the pinned theorem keeps successive results comparable.
The gap to Ethereum’s December target
The Foundation’s December 2025 zkEVM security roadmap called for 128-bit provable security, a final proof size of 300 KiB or less, and a formal soundness argument for the recursion architecture.
A February security-sprint update moved the M3 deadline to early December 2026 and aligned the architecture-security argument with a Dec. 1 deliverable. The roadmap asks teams to connect component bounds to an auditable system package.
For koalaIRS12, a lower certificate reaching the encoded 128-bit target would settle the soundness side of this benchmark at its fixed parameter point. A production zkEVM claim would additionally need soundness accounting across every relevant component, proof-size compliance, a documented recursion topology, an argument for how its parts compose, and evidence that specifications match implementations.
The Foundation’s public progress page, last synced Aug. 20, lists zkVM readiness and ISA compliance results and names real-time proving and soundcalc integration as criteria. Its rendered tables contain no completion marker for the full early-December package and remain silent on work tracked elsewhere.
A May update on optional execution proofs described a non-consensus-critical phase in which zkEVM proofs supplement mainnet testing while ordinary execution-client re-execution continues to drive attestation.
That optional role keeps the leaderboard’s immediate consequence in the research domain. Movement in the certificates changes the evidence available for future security arguments without changing Ethereum’s current consensus-critical validation path.
On better.codes, soundness submissions can lift the 63.99-bit lower certificate and attack submissions can pull the 116.13-bit upper certificate down. Across the zkEVM roadmap, teams must publish the system-level accounting, proof sizes, recursion arguments, and implementation evidence required for the early-December review.
At present, the 52.14-bit interval is a live measure of unfinished work on koalaIRS12. Ethereum’s 128-bit production case will depend on how that component evidence fits into the larger proof.
