Ethereum Advances Hash-Based SNARKs With Machine-Checked Security

Ethereum’s push toward post-quantum cryptography is entering a more formal phase as researchers combine machine-checked mathematics with open, AI-assisted research to strengthen the security foundations of hash-based SNARKs.

The work sits within Ethereum’s broader post-quantum strategy, which calls for replacing quantum-vulnerable public-key primitives while using proof systems to manage the larger computational and communication costs associated with post-quantum signatures.

The Ethereum Foundation’s official post-quantum documentation identifies hash-based signatures and a SNARK-based aggregation system around leanVM as part of the proposed consensus-layer architecture. The Foundation also stresses that formal verification is needed alongside cryptographic migration because implementation errors can create risks even when the underlying mathematics is sound.

The latest research push is therefore less about launching a new token or blockchain feature and more about reducing uncertainty around the mathematical assumptions that future Ethereum infrastructure could depend on.

Hash-Based SNARKs Become a Security Priority

Hash-based SNARKs are attractive for Ethereum’s post-quantum roadmap because they can avoid reliance on elliptic-curve assumptions vulnerable to sufficiently powerful quantum computers.

Ethereum’s official post-quantum roadmap says the consensus layer is expected to move away from BLS signatures toward hash-based alternatives such as leanXMSS. Because those signatures are larger and do not provide BLS-style native aggregation, the Foundation is researching SNARK-based aggregation through leanVM to restore scalability.

That creates an important dependency: the proof system used for aggregation must itself have credible security guarantees.

The challenge is particularly relevant because hash-based proof systems often rely on assumptions from coding theory, including questions around Reed-Solomon codes, proximity gaps and correlated agreement.

A paper by Gal Arnon, Stanford professor Dan Boneh and EPFL researcher Giacomo Fenzi describes the open mathematical problems associated with the Ethereum Foundation’s $1 million Proximity Prize. The authors specifically connect those problems with the design of succinct proof systems and Reed-Solomon-based constructions.

The paper was submitted to the Cryptology ePrint Archive in April 2026 and received its third revision in July. Its July update added a comparison involving recent results and concrete estimates concerning known attacks, showing that the underlying security questions are still an active research area rather than settled mathematics.

Machine-Checked Proofs Change the Research Process

The newer element is the use of machine-checked verification as a filter for proposed mathematical advances.

The distinction matters. An AI system can suggest a conjecture, identify a possible counterexample or generate a candidate proof, but that does not establish the result. A formal proof assistant such as Lean can mechanically check whether the submitted argument follows from its stated definitions and assumptions.

A current project built around the Proximity Prize describes this workflow directly: agents can search the open problem space, while accepted mathematical contributions must survive exact arithmetic checks or formal verification rather than relying solely on an AI model’s explanation.

This approach also reflects the Ethereum Foundation’s broader emphasis on formal verification. Its post-quantum documentation says the Foundation’s protocol work includes formal verification of cryptographic components and identifies verification as an important part of the migration process.

For a blockchain that could ultimately depend on these proof systems for validator signature aggregation, that distinction is important. A faster prover is useful only if the resulting proof system remains sound under the assumptions used to configure it.

AI Agents Expand the Search for Cryptographic Improvements

The agentic component is being developed alongside the mathematical research rather than replacing cryptographers.

Eigen Labs’ August 12 announcement of Yukon describes an open research platform in which independent researchers, AI agents and different agent harnesses attack measurable scientific or engineering objectives in parallel. Every submission is evaluated against a defined benchmark and verified results can become the baseline for subsequent attempts.

One of the platform’s challenges, SNARK.fast, focuses on improving the performance of Flock, a hash-based SNARK developed by researchers Benedikt Bünz, Ron Rothblum and William Wang.

Eigen Labs reported that SNARK.fast, developed with Succinct, Espresso and the Ethereum Foundation, increased the performance target for post-quantum Ethereum proving by 3.5 times during its early challenge period.

That performance work is separate from the mathematical Proximity Prize, but the two efforts address complementary bottlenecks.

The Proximity Prize focuses on the mathematical security assumptions underpinning proof systems. SNARK.fast focuses on making a hash-based proving implementation faster. Together, they illustrate the two-sided problem facing post-quantum Ethereum: the cryptography must be defensible, and the resulting system must also be practical enough to run at blockchain scale.

Flock itself was introduced in a July 2026 research paper as a hash-based SNARK for proving large batches of standard hash computations. The authors reported single-core throughput of about 82,000 BLAKE3 compressions, 42,000 SHA-256 compressions and 30,000 Keccak permutations per second on an M4 Max processor, with substantially higher throughput across 10 cores.

Why the Security Work Matters for Ethereum

Ethereum’s post-quantum migration is not limited to replacing one signature algorithm.

The Foundation’s roadmap spans the execution, consensus and data layers. At the consensus layer, hash-based signatures create a scaling problem because they are larger and do not aggregate naturally like BLS signatures. The proposed solution therefore depends on efficient proof-based aggregation.

That makes the security of the SNARK layer strategically important.

There is also a timing issue. The Foundation’s current documentation says that a cryptographically relevant quantum computer is not considered imminent, while emphasizing that a decentralized network requires years of engineering, coordination and formal verification before a cryptographic transition can be completed.

The result is a research strategy built around preparation rather than an immediate emergency response.

The Proximity Prize is one component of that strategy. The Foundation announced the $1 million initiative as a way to address coding-theoretic problems relevant to succinct proof systems, while its wider post-quantum program includes leanVM, leanXMSS and ongoing client and protocol research.

Risks and Unanswered Questions

The use of AI agents does not by itself establish a cryptographic breakthrough.

Agent-generated mathematical claims still require verification, and machine-checking only proves the formalized statement that has actually been encoded. A flawed definition, missing assumption or mismatch between a formal theorem and the deployed cryptographic construction can leave important risks outside the proof.

There is also an unresolved gap between mathematical security and production security.

A proof system can have a formally verified theorem and still contain implementation vulnerabilities, performance problems or integration weaknesses. Ethereum’s own documentation recognizes this distinction by treating implementation maturity, auditing and formal verification as separate requirements for post-quantum deployment.

The Proximity Prize research also demonstrates why the area remains unsettled. Its authors are reviewing open problems involving list decoding, proximity gaps and correlated agreement rather than presenting those questions as fully resolved.

For Ethereum, that means research results should not be interpreted as evidence that the network has already completed its post-quantum transition.

What Happens Next

The immediate focus is likely to remain on two tracks: proving the mathematical claims used by hash-based systems and improving the performance of implementations such as Flock.

The agentic research model could make that process broader by allowing researchers and AI systems using different models, prompts and tools to attack the same measurable objective independently. Yukon says each verified improvement can become the new baseline, creating a cumulative research loop rather than a sequence of isolated experiments.

Ethereum’s official post-quantum roadmap remains a research and engineering roadmap rather than a finalized protocol commitment. The Foundation explicitly says its roadmap can change as research and implementation develop, with final protocol direction determined through Ethereum’s open governance processes.

For readers tracking the technology, the most useful indicators will therefore be independently verified improvements in hash-based proving performance, new machine-checked results concerning proximity and correlated-agreement assumptions, updates to leanVM and evidence that the resulting systems can meet Ethereum’s real-time consensus requirements.

The key development is not that AI has solved post-quantum cryptography. It is that Ethereum and its research partners are increasingly treating cryptographic progress as a measurable, reproducible and machine-checkable engineering process.