使用 LLM 引导约束合成实现 zkEVM 的自动形式验证

零知识以太坊虚拟机 (zkEVM) 通过生成保证链下执行正确性的零知识证明来保护以太坊汇总。然而，微妙的实现错误（例如，不正确的 Gas 计算）可能会导致有效的证明证明语义上的错误状态，从而默默地破坏加密保证。通过 SMT 求解器进行形式验证可以防止这种情况发生，但受到规范的限制：当前的 zkEVM 开发实践缺乏将 Rust 操作码处理程序转换为验证模型的自动化方法。当前的实践依赖于不可持续的手动规范，而基于 LLM 的方法则遭受幻觉并缺乏正式的保证。为了解决这个问题，我们提出了 VeriSynth，一个从 Rust zkEVM 代码合成可执行 Python/Z3 验证模型的框架。 VeriSynth 强制执行混合范例：LLM 严格充当形式化前端，将代码转换为符号约束，而 SMT 求解器则充当正确性仲裁器。为了处理复杂的多组件状态转换，VeriSynth 将语义分解、基于检索的提示和验证引导的自动修复集成到闭环管道中。我们在第一个源代码级 zkEVM 验证基准上评估 VeriSynth，包括正确和错误的操作码实现。 VeriSynth 的错误检测率超过 90%，大大优于直接和对话式 LLM 基线以及生产级手写突变测试套件。消融研究证实，每个管道组件对于框架的整体有效性至关重要。