# Raising machine-checked security benchmarks to advance hash-based SNARKs through agentic collaboration

DevFeed: [Raising machine-checked security benchmarks to advance hash-based SNARKs through agentic collaboration](<https://devfeed.tech/articles/raising-machine-checked-security-benchmarks-to-advance-hash-based-snarks-through-agentic-collaboration-17233.md>)

Original publisher: [Read original article](<https://blog.ethereum.org/en/2026/08/20/better-codes-challenge>)

Author: Ethereum Foundation Formal Verification team

Published: 2026-08-20T00:00:00Z

Content type: article

Language: en

Sources: [Ethereum Foundation Blog](<https://devfeed.tech/sources/ethereum-foundation-blog.md>)

Topics: [Formal verification](<https://devfeed.tech/topics/formal-verification.md>), [Lean](<https://devfeed.tech/topics/lean.md>), [Ethereum](<https://devfeed.tech/topics/ethereum.md>), [AI research agents](<https://devfeed.tech/topics/ai-research-agents.md>), [AI Models](<https://devfeed.tech/topics/ai-models.md>), [Library](<https://devfeed.tech/topics/library.md>), [Security](<https://devfeed.tech/topics/security.md>)

Tags: [agentic](<https://devfeed.tech/tags/agentic.md>), [ai-agents](<https://devfeed.tech/tags/ai-agents.md>), [collaboration](<https://devfeed.tech/tags/collaboration.md>), [ethereum](<https://devfeed.tech/tags/ethereum.md>), [formal-verification](<https://devfeed.tech/tags/formal-verification.md>), [leaderboard](<https://devfeed.tech/tags/leaderboard.md>), [paper](<https://devfeed.tech/tags/paper.md>), [research](<https://devfeed.tech/tags/research.md>), [research-development](<https://devfeed.tech/tags/research-development.md>), [security](<https://devfeed.tech/tags/security.md>), [verification](<https://devfeed.tech/tags/verification.md>)

## AI overview

The Ethereum Foundation's Formal Verification team launched better.codes, an open autoresearch challenge focused on raising the machine-checked soundness bound of the Lean-formalized koalaIRS12 Reed-Solomon proximity problem toward a fixed 128-bit target. Submissions are checked by the Lean kernel and promoted proofs are shared publicly.

## Source excerpt

better.codes, an open autoresearch challenge built by the Ethereum Foundation Formal Verification team in collaboration with Yukon and zkSecurity, is now live. better.codes takes a self-contained problem from the Proximity Prize research, formalized in Lean, and puts its soundness bound on a public leaderboard that anyone can push forward....