AI 中文总结
研究针对zkEVM因实现错误可能破坏加密保证的问题，提出VeriSynth框架，通过大语言模型引导从Rust代码合成验证模型，采用混合范式及集成多种技术处理状态转换，在验证基准上错误检测率超90%，远超基线。
AI 中文摘要
零知识以太坊虚拟机（zkEVM）通过生成零知识证明来确保以太坊汇总的链下执行正确性。然而，微妙的实现错误可能导致有效证明认证语义错误状态。通过SMT求解器进行形式验证可防止此问题，但受限于规范。当前zkEVM开发实践缺乏将Rust操作码处理程序转换为验证模型的自动化方法。我们提出VeriSynth框架，从Rust zkEVM代码合成可执行的Python/Z3验证模型。它采用混合范式，大语言模型作为形式化前端，SMT求解器作为正确性仲裁器。还集成多种技术处理复杂状态转换。在首个源级zkEVM验证基准上评估，其错误检测率超90%，远超基线。消融研究证实各组件对框架有效性至关重要。
英文摘要
Zero-Knowledge Ethereum Virtual Machines (zkEVMs) secure Ethereum rollups by generating zero-knowledge proofs that guarantee off-chain execution correctness. However, subtle implementation bugs (e.g., incorrect gas accounting) can lead to valid proofs certifying semantically faulty states, thereby silently defeating cryptographic guarantees. Formal verification via SMT solvers can prevent this, but is bottlenecked by specification: current zkEVM development practice lacks automated methods to translate Rust opcode handlers into verification models. Current practices rely on unsustainable manual specifications, while LLM-based approaches suffer from hallucination and lack formal guarantees. To address this, we propose VeriSynth, a framework that synthesizes executable Python/Z3 verification models from Rust zkEVM code. VeriSynth enforces a hybrid paradigm: an LLM acts strictly as a formalization frontend to translate code into symbolic constraints, while an SMT solver serves as the correctness arbiter. To handle complex multi-component state transitions, VeriSynth integrates semantic decomposition, retrieval-grounded prompting, and verification-guided auto-repair into a closed-loop pipeline. We evaluate VeriSynth on the first source-level zkEVM verification benchmark, encompassing both correct and faulty opcode implementations. VeriSynth achieves 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 confirm that each pipeline component is critical to the framework's overall effectiveness.
Comments11 pages
