VeriSynth uses LLMs to auto-verify zkEVMs with 90% bug detection

Zero-Knowledge Ethereum Virtual Machines (zkEVMs) secure Ethereum rollups by generating proofs of correct off-chain execution, but subtle implementation bugs—like incorrect gas accounting—can silently defeat cryptographic guarantees. Formal verification via SMT solvers can prevent this, but translating Rust opcode handlers into verification models has been a manual bottleneck. Existing LLM-only approaches suffer from hallucination and lack formal guarantees. To solve this, Shichen Huang et al. introduce VeriSynth: a hybrid framework that uses an LLM strictly as a formalization frontend to translate code into symbolic constraints, while an SMT solver (Z3) acts as the final correctness arbiter. The pipeline integrates semantic decomposition, retrieval-grounded prompting, and verification-guided auto-repair in a closed loop, enabling automated generation of executable Python/Z3 models from Rust zkEVM code.

Evaluated on the first source-level zkEVM verification benchmark—including both correct and faulty opcode implementations—VeriSynth achieved a bug detection rate of over 90%, substantially outperforming direct and conversational LLM baselines as well as a production-grade handwritten mutation-testing suite. Ablation studies confirmed that each component (semantic decomposition, retrieval grounding, auto-repair) is critical to overall effectiveness. This work demonstrates a practical path toward automated formal verification of critical blockchain infrastructure, reducing reliance on unsustainable manual specifications while maintaining rigorous formal guarantees.