Advancing Hash-Based SNARK Security Through Machine-Checked Agentic Collaboration

According to the Ethereum Foundation’s Formal Verification team, the new better.codes challenge puts that gap inside a machine-checked, public workflow. For zk-rollup and zkVM engineers, this matters because the security margin of deployed proof systems depends on conjectures that are not yet fully formalized.

The benchmark is the security boundary

better.codes takes the koalaIRS12 proximity problem from the Proximity Prize research initiative and formalizes it in Lean. The challenge fixes the theorem statement, parameter point, and verification harness. Participants must submit a larger soundness lower bound through a defined submission surface.

The Lean kernel checks the proof. A comparator checks that the exported theorem matches the pinned statement. A submission is not promoted because an AI agent produced plausible text or because a test suite passed. It is promoted only after the machine-checked verification path succeeds.

This is the relevant distinction for security work. The benchmark measures a proven bound, not an argument that has merely survived selected examples. Every accepted result adds its lemmas, proof techniques, or impossibility results to a public repository. The state is git-backed and transparent. Later solvers can inspect previous diffs and avoid documented dead ends.

The initial target is a proven 128-bit soundness bound for koalaIRS12. CryptoSlate reports that the benchmark currently has a 52.14-bit cryptographic proof gap and that researchers are working toward the 128-bit target by December 2026. That figure and timeline come from the publication’s snippet, not from the Ethereum Foundation’s detailed announcement.

Why this reaches L2 security

Hash-based SNARKs used in systems securing zk-rollups and zkVMs rely on proximity gaps and correlated agreement for Reed–Solomon codes. The Ethereum Foundation states that deployed systems target 128-bit security, but that guarantee holds in full only if the underlying conjectures hold.

The attack vector here is not a malformed calldata branch or an unchecked state mutation in an EVM contract. It is a proof-system assumption sitting below the contract layer. If the soundness bound is weaker than the deployed security claim, the invariant between “the proof verifies” and “the claimed computation is secure” is not fully established.

That does not mean the challenge has identified an exploit in a live rollup or zkVM. The published material describes a gap between conjectured and machine-checked security benchmarks. The purpose of better.codes is to reduce that gap through incremental, reproducible proofs.

The agentic model changes the search process, not the acceptance rule. Independent teams can run different AI models, harnesses, and tools against the same pinned problem. The verification surface remains deterministic. An agent can propose a lemma. Lean decides whether the resulting proof is valid.

What engineers should verify now

For teams building or auditing L2 proving infrastructure, the practical checks are narrow:

• Separate claimed security from proven security. Record which bounds are machine-checked and which still depend on conjectures.
• Pin the theorem and parameters. A benchmark is meaningful only when the statement, parameter point, and verification harness cannot drift between submissions.
• Verify the exported theorem. The comparator must confirm that the submitted theorem is exactly the one under evaluation.
• Require kernel acceptance. Heuristic output, generated proof text, and passing examples are not substitutes for Lean’s proof check.
• Track proof provenance. Accepted lemmas, techniques, impossibility results, and prior diffs should remain inspectable and reproducible.
• Do not convert a stronger bound into a broader claim. Raising a benchmark for koalaIRS12 does not, by itself, prove the security of every hash-based SNARK, zk-rollup, or zkVM.

The immediate deliverable is not a new protocol. It is a stricter security benchmark. That is the correct unit of progress: a larger bound, a pinned statement, and a proof that the kernel accepts.