AI
AI-Guided Framework Automates Verification of zkEVM Security Flaws
Researchers propose VeriSynth, a system that uses large language models and SMT solvers to automatically detect bugs in zero-knowledge Ethereum rollup implementations.
A new automated verification framework aims to solve a critical security gap in zero-knowledge Ethereum Virtual Machines (zkEVMs)—the systems that power Ethereum rollups. While zkEVMs are designed to cryptographically guarantee that off-chain transactions are executed correctly, subtle coding errors can slip through, silently invalidating these security guarantees.
The Problem with Manual Verification#
zkEVMs generate zero-knowledge proofs to ensure rollup execution is correct. However, implementation bugs—such as incorrect gas accounting—can allow faulty states to be certified as valid. Current approaches to catch these issues rely on laborious hand-written formal specifications, a process that doesn't scale well as codebases evolve. Meanwhile, attempts to use large language models to generate specifications have struggled with hallucinations and lack of formal correctness assurances.
VeriSynth: A Hybrid Approach#
Researchers have introduced VeriSynth, a framework that synthesizes formal verification models directly from Rust zkEVM code. The system assigns different roles to different tools: LLMs translate code into symbolic constraints as a "formalization frontend," while SMT solvers act as the final arbiter of correctness—ensuring that any generated specifications are mathematically sound.
To handle the complexity of multi-component state transitions, VeriSynth combines semantic decomposition, retrieval-grounded prompting, and verification-guided auto-repair into an integrated pipeline.
Evaluation and Results#
Testing on a newly developed source-level zkEVM verification benchmark, VeriSynth achieved a bug detection rate exceeding 90%. This performance substantially exceeded direct LLM approaches, conversational LLM baselines, and even a production-grade handwritten mutation-testing suite. Ablation studies confirmed that each component of the pipeline contributes meaningfully to overall effectiveness.
The research was submitted to arXiv on July 22, 2026.
