Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis
本文介绍了 VeriSynth，这是一个利用混合 LLM-SMT 流水线自动从 Rust zkEVM 代码中合成可执行验证模型的创新框架，通过克服人工规范的局限性和 LLM 的幻觉问题，实现了超过 90% 的缺陷检测率。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，互联网是一个巨大的、全球性的数字账本，每个人都能看到每一笔交易，但没有任何一个人可以控制它。这就是区块链的世界，而以太坊是其中最著名的居民。为了让这个系统更快、更便宜，开发者构建了“二层”（Layer-2）网络，它们在后台进行繁重的计算工作，只将最终结果展示给主网。为了证明这些后台结果是诚实的，而不必泄露其中的秘密细节，他们使用了一种神奇的技巧，叫做“零知识证明”（Zero-Knowledge Proof）。这就像一位巫师向你展示一个锁着的盒子，并向你证明，无需打开盒子，里面的宝藏正是他们所承诺的那样。
但问题在于：为了让魔法生效，巫师的咒语书（计算机代码）必须是完美的。如果巫师在咒语中犯了一个微小的错误——比如数错了金币的数量，或者忘记更新地图——即使盒子看起来依然锁得严实且有效，里面也可能空无一物，或者装满了假币。这是安全领域的噩梦。为了阻止这种情况，专家们使用“形式化验证”（Formal Verification），这是一种由一位极其严苛的机器人数学家逐行检查咒语书，以确保逻辑无懈可击的方法。然而，为这个机器人编写指令是非常困难的，就像试图将一本用秘密语言编写的复杂电子游戏说明书，翻译成机器人能读懂的数学教科书一样。
这正是名为 VeriSynth 的新工具大显身手的地方。研究人员意识到，虽然人工智能（AI）擅长编写代码，但它也容易产生“幻觉”——即编造听起来很真实但实际上是错误的事实。因此，他们并没有仅仅要求 AI 去寻找漏洞，而是构建了一个团队：让 AI 充当创意翻译官，将混乱的、秘密的代码转化为给机器人数学家的草稿，而机器人则充当严厉的法官，判定“是的，这是正确的”或“不，这是胡说八道，重试”。
问题所在：沉默的漏洞
在零知识以太坊虚拟机（zkEVM）的世界里，运行核心业务的代码是用一种叫做 Rust 的语言编写的。这种语言功能强大但也非常棘手。有时，开发者可能会不小心写错一行代码，导致计算 Gas（交易手续费）出错，或者忘记更新内存槽。如果发生这种情况，系统可能会为一个实际上已经损坏的交易生成一个“有效”的证明。这就像一名银行柜员不小心给了你 100 美元而不是 10 美元，但收据上却显示一切完美无缺。因为证明看起来是有效的，这个错误会被忽略，从而悄无声息地破坏了整个系统的安全性。
通常的修复方法是让人类编写详细的测试用例，希望能捕捉到每一个可能的错误。但人类会疲劳，而且无法想象计算机可能遇到的每一种奇特的场景。另一种方法是使用大语言模型（LLM）——即那些编写文章或代码的同类 AI——来寻找漏洞。但本文认为，仅仅要求 AI “寻找漏洞”是不可靠的。AI 可能会在没有漏洞的地方臆测出漏洞，或者完全错过漏洞，因为它缺乏安全领域所需的严格数学确定性。
解决方案：翻译官与法官的搭档
该论文的作者 Shichen Huang 及其团队创建了一个名为 VeriSynth 的框架。他们将这个问题处理得像一场高规格的“传声筒”游戏，其中信息传递必须完美无误。
- 翻译官（LLM）： 首先，系统将复杂的 Rust 代码分解成细小的、易于处理的块，就像把一个巨大的拼图拆分成单个碎片一样。然后，它要求 AI 将每个部分翻译成一个“验证模型”。这不仅仅是一个描述，而是一套严格的数学规则（使用 Python/Z3 语言编写），告诉机器人数学家代码应该如何表现。
- 参考库： 为了防止 AI 编造事实，VeriSynth 为它提供了一份“小抄”，其中包含先前经过验证的示例。这就像在要求 AI 搭建新的乐高模型之前，先给它看一张正确组装好的乐高成品图，这样它就知道零件应该是什么样子的。
- 法官（SMT 求解器）： 这是最重要的部分。AI 的翻译永远不会被立即信任。它会被交给一位超级严苛的机器人数学家（SMT 求解器）。机器人会根据规则检查翻译内容。如果翻译存在语法错误、缺失部件或逻辑矛盾，机器人就会拒绝它。
- 自动修复： 如果机器人拒绝了翻译，它并不会仅仅说“失败”。它会向 AI 发送一条具体的错误消息：“你使用的数字大小不对，”或者“你忘记更新内存了。”随后，AI 会尝试修复错误并重新发送。这个循环会一直持续，直到机器人满意为止。
他们的发现
团队在他们构建的一个包含 95 个隐藏错误代码实例的自定义“有缺陷”数据集上测试了 VeriSynth。这些错误涵盖了从简单的数学错误到处理不同程序间调用时的复杂问题。
结果令人瞩目：
- VeriSynth 找到了 95 个中的 87 个 漏洞，实现了 91.6% 的检测率。
- 相比之下，如果只是让 AI 在没有严格机器人法官的情况下寻找漏洞，它只能找到 44 个（46.3%）。
- 即使让他们让 AI 与机器人进行对话并尝试再次运行（一种“对话式”方法），它也只能找到 58 个（61.1%）。
论文还将 VeriSynth 与一个名为 Scroll 的主要项目所使用的现实世界测试方法进行了比较。Scroll 的专家团队编写了自己的测试集来捕捉漏洞。他们的测试捕捉到了 95 个中的 55 个。而 VeriSynth 捕捉到了 87 个，这意味着它比人类编写的测试多发现了 32 个 被遗漏的漏洞。
为什么这很重要
研究人员强调，这并不是要取代人类开发者，也不是在说 AI 是完美的。相反，这是关于将 AI 作为一种强大的工具来承担繁重的翻译工作，同时保留一个严格、不眨眼的机器人作为最终权威。“自动修复”功能是最关键的部分；如果没有它，系统的成功率会降至 66.3%，这证明了自我修复的能力才是系统奏效的关键。
这项研究表明，通过将 AI 的创造力与数学求解器的严格逻辑相结合，我们可以为区块链的未来构建一个比人类独自构建的更强大的安全网。它提醒我们，在数字安全领域，最好的防御是建立一个由“创意提出，逻辑决策”的团队。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。