一句话看懂：安全公司 Trail of Bits 在审计 Miden zkVM 时，没有直接让 AI 找漏洞，而是先用六个月时间让 Agent 从零搭出 LSP 服务器、反编译器、静态分析引擎和 Lean 形式化模型，结果工具本身先挖出一个可伪造 Falcon 签名、盗取账户资金的严重漏洞。
事件核心：发生了什么
2025 年底，Miden 团队委托 Trail of Bits 在正式上线前审计其零知识虚拟机。审计范围包含用自研汇编语言 MASM 编写的 Miden 核心密码学库。Miden VM 采用栈机架构，指令的输入输出都隐式地来自栈，加上生态几乎没有 IDE 支持、LSP 和各种 lint 工具，人工审查难度很高。
Trail of Bits 没有等代码写完再上手，而是利用六个月的准备期，让 Agent 从零构建了四类工具：VS Code 的 LSP 服务器（支持语法高亮、跳转定义、引用查找、悬停文档，并内联展示指令语义和栈效应）、MASM 反编译器、静态分析引擎，以及用 Lean 编写的 VM 执行器形式化模型。
这些工具发现了真实安全问题：一个未被校验的、由证明者提供的输入，可让恶意证明者伪造 Falcon 签名，进而从 Miden 账户持有人处窃取资金。Lean 部分还产出了 95 条机器验证的正确性证明，覆盖 Miden 核心库的很大一部分。
为什么重要
目前公开信息显示，业界关于 AI 安全审计的讨论大多集中在“Agent 扫代码找 bug”这一环节。Trail of Bits 的案例把 AI 的用途前移到了基础设施搭建阶段：在人工审查开始之前，先用 Agent 补齐缺失的开发工具和形式化模型。这改变了 AI 在安全流程中的定位——它不只是加速器，而是让原本因成本过高而无法开展的深度分析变得可行。
对零知识证明这类高保障项目而言，形式化验证和静态分析长期受制于工具链缺失。Agent 能低成本生成定制工具，意味着小众语言和新型 VM 的审计门槛可能下降，安全审查的深度与覆盖范围有望提升。
对用户/开发者/创作者的影响
对开发者来说，最直接的启发是：面对缺乏工具链的新语言或新运行时，可以先用 Agent 生成 LSP、反编译器和静态分析原型，再进入实际审查。对审计团队而言，预算分配可能从“纯人工审查时长”部分转向“工具与形式化模型的构建成本”。对依赖 zkVM 的链上项目，这类方法若能普及，账户资金安全的下限会被抬高，但前提是审计方愿意接受更长的准备周期。
值得关注的后续
一是 Trail of Bits 是否会将这套 LSP、反编译器和 Lean 模型开源，若开源，其他 zkVM 和 MASM 类项目的审计成本可能明显下降。二是 Miden 主网上线后，该 Falcon 签名漏洞的修复是否经过完整复验。三是其他安全公司是否跟进“先建工具、再审计”的流程，以及 Agent 生成的形式化模型能否被更广泛地机器验证。
