Ethereum scaling and DeFi infrastructure efforts are increasingly moving toward zero-knowledge–based execution models, where correctness must be provable at every layer of the stack.

Certora has been awarded a research grant from the Ethereum Foundation as part of the zkEVM Formal Verification Project. The grant supports work to verify the correctness of autoprecompiles, an optimization technique for zero-knowledge computation developed by Powdr Labs.

Why zkEVM Correctness Matters

The zkEVM is a foundational component in Ethereum’s path toward scalable, zero-knowledge execution, and its correctness is critical to the long-term security of the network.

The zkEVM replaces the traditional smart contract execution model with a zero-knowledge alternative. By proving execution correctness cryptographically, zkEVMs enable lower gas costs, faster execution, stronger security guarantees, and improved scalability across the Ethereum ecosystem.

As zkEVM implementations mature, performance optimizations are becoming increasingly sophisticated—and increasingly critical. Ensuring these optimizations are correct under all possible conditions is essential to maintaining trust in the execution layer.

Verifying Autoprecompiles

Autoprecompiles are automatically inferred, low-level ZK circuit components that are reused to accelerate cryptographic and arithmetic operations inside the zkEVM. Instead of relying on manually written precompiles, autoprecompiles are generated programmatically to improve performance while reducing engineering overhead.

Because autoprecompiles are reused across execution paths, any correctness issue can have systemic impact rather than isolated failure. As a result, optimizations at this level significantly raise the stakes: even small errors in generation or reuse could compromise correctness across the entire execution pipeline.

Through this grant, Certora is collaborating with Powdr Labs to develop formal verification techniques that mathematically prove the correctness of the autoprecompile generation and reuse process.

The goal is to ensure that these optimizations preserve correctness in all cases, not just in typical execution paths. This work brings formal methods directly into the zkEVM toolchain, helping ensure that performance improvements do not come at the cost of safety.

“Autoprecompiles make the zkEVM execution layer viable, but they also increase the importance of verifying the correctness of the entire toolchain,” said Seth Hallem, CEO of Certora.

“We’re grateful to the Ethereum Foundation for supporting this work, which brings mathematical verification to the very foundation of ZK computation.”

Open-Source Outcomes

A core goal of this work is to produce reusable, public verification infrastructure for the broader zkEVM ecosystem.

All specifications, proofs, and verification frameworks developed under this grant will be open-sourced. These artifacts are intended to serve as reusable infrastructure for:

• zkEVM implementations
• Rollup developers
• Researchers working on zero-knowledge protocols

By making this work public, we aim to strengthen the broader ecosystem and enable other teams to build on top of formally verified foundations.
“Precompiles have been key to zkEVM performance, and autoprecompiles can take this even further by verifying these optimizations automatically as they are generated,” said Alexander Hicks, Researcher at the Ethereum Foundation.

“This also reduces the need to manually verify precompiles and may lead to verification techniques applicable beyond zkEVMs.”

Looking Ahead

This effort contributes to a zkEVM execution model that is efficient, scalable, and grounded in proven correctness, supporting the long-term security and sustainability of Ethereum’s zero-knowledge future.

We’ll share updates as the work progresses.