Trail of Bits 这次干的事有点反常规。拿到 Miden zkVM 的审计合同，他们没有立刻扑到代码上，而是先让一批 AI Agent 花了整整六个月，从零把工具链造齐——LSP 服务器、反编译器、静态分析引擎，外加一个用 Lean 写的 VM 执行器模型。工具到位之后，才轮到人去读代码。结果是：一条能让恶意 prover 伪造 Falcon 签名、直接把资金搬走的高危路径；400 多处类型验证缺陷；95 个机器验证的正确性证明；还有两个连单元测试都没逮住的细微 bug。这套打法把安全审计里的一个老问题翻了出来：当 AI Agent 能造工具的时候，审计的起点该往哪儿挪？
先造工具，再碰代码
MASM 的生态空白，正好交给 Agent 填
零知识虚拟机 Miden 的底层语言 MASM 一直处在尴尬位置。有语法，有编译器，但没有像样的开发者工具。没有语言服务器，写代码的人只能靠猜；没有反编译器，审计员看字节码等于看天书；没有静态分析，所有检查都得手工完成。这种活儿人类做起来极其枯燥——规则明确、重复度高、需要穷举，恰好是 Agent 的舒适区。Trail of Bits 没让 Agent 去「找漏洞」，而是让它去「造基础设施」，这个任务切分本身就值得琢磨。找漏洞依赖判断力，造基础设施依赖耐力，而后者更容易被拆成一个个可验证的小目标。
三件工具，三种抽象层级
反编译器负责把 MASM 的字节码还原成人能读的中间表示，它解决的是「看得见」。静态分析引擎在中间表示上跑类型推导和数据流追踪，解决的是「看得全」。LSP 服务器把这一切嵌进编辑器，让审计员写探针、读代码的时候立刻拿到反馈。三层叠在一起，本质是把人的注意力从机械劳动里抢出来，留给判断。这三件工具都不是从零发明——语言服务器、反编译器、静态分析在传统编译器领域全是成熟套路，难的是有人愿意为一个还没那么主流的 zkVM 语言把它们实现一遍。
Lean 模型走的是另一条路
第四件工具不走同样的路。团队用 Lean 定理证明器给 Miden VM 的执行器建了一个形式化模型。这不是为了跑代码，而是为了之后写下的每一句结论都能落到机器可验证的证明上。静态分析说「这里可能有问题」，Lean 模型说「在这组前提之下，这一定成立或者一定不成立」。两者不替代，互补。95 个机器验证的正确性证明就这么来的。用 Lean 描述一个 VM 执行器，工作量不小，可一旦模型立住，后续所有推理都变成了能累加的资产。
工具链筛出来的三样东西
恶意 prover 伪造 Falcon 签名，直接通向资金
最扎眼的一条发现和密码学有关。Miden 用 Falcon 签名方案，而工具链暴露出一个缺口：恶意 prover 能伪造签名，进而盗取资金。这不是理论边角，是直通资产的路径。这类漏洞最麻烦的地方在于，ZKP 系统里「证明」和「验证」的边界一旦有缝，攻击者不需要攻破底层数学，只需要利用协议实现里的假设偏差。审计员能定位到它，很大程度上是因为静态分析把类型验证的异常路径摊开了——那些平时被正常流程掩盖的边界情况，在分析引擎的输出里变成了成排的条目。
400 多处类型验证缺陷，单看都不致命
静态分析引擎标出了 400 多处与类型验证相关的问题。单看每一条，绝大多数够不上高危，甚至够不上中危。但类型系统在虚拟机里承担的是「边界守卫」的角色——它管的是什么东西能被当成什么用。守卫漏了 400 个口子，未必每个口子后面都站着攻击者，可攻击者只需要找到其中一个能串起来的口子。这就是覆盖率的价值：不是每一条都会变成漏洞，而是你没法事先知道哪一条会。报告里写「400 多处」，读者容易麻木，真正该问的是这 400 处里有多少处在同一条调用链上。
95 条证明，和两个漏网的 bug
Lean 工作产出了 95 个机器验证的正确性证明，覆盖执行器模型的关键性质。同一批工具还翻出了两个细微 bug——这两个 bug 此前的单元测试一直没抓到。这件事值得单独拎出来说。单元测试的设计逻辑是「我预料到什么，就测什么」，它天然受限于作者想象力的边界。形式化模型和静态分析的逻辑是「我把所有可能枚举一遍，看哪条路走不通」，它不依赖想象力。两种方法抓漏的能力不在一个量级，成本也不在一个量级。95 条证明听起来很多，真正的信息量在于：它们划出了一块「已经被彻底检查过」的区域，让审计员可以把精力投到证明覆盖不到的地方去。
六个月换一套工具，这笔账怎么算
Agent 的产出不是洞察，是覆盖率
如果把 Agent 当成「会自己发现漏洞的智能体」，多半会失望。它在这套流程里扮演的是高产出的工程劳动力：写 LSP、写反编译器、补测试、把形式化模型里繁琐的部分填满。它的价值不在某个灵光一现的判断，而在把过去需要人类团队几个月才能铺开的基础设施，在可接受的时间里铺开。审计员的角色没有消失，反而更集中在「决定查什么、判断查出来的东西有多严重」这两件事上。这个分工挺健康——机器干机器的活，人干人的活，中间不越界。
这套流程的复制门槛在哪
不是每个项目都值得这么干。MASM 这种「生态空白 + 语言规则明确 + 代码规模可控」的组合，才让 Agent 造工具有了明确的收敛目标。如果目标是一个有十年历史、几十种语言混用的巨型单体，Agent 造出来的半成品工具可能还不如现成的开源方案。判断标准其实很朴素：这个项目缺的工具，是「规则明确但没人写」，还是「连规则都没定下来」。前者适合交给 Agent，后者不适合。zkVM 这类新兴领域恰好大量属于前者——语言规范写得清清楚楚，缺的只是把它工程化的人手。
审计的起点在往前挪
过去的审计流程是：拿代码、读代码、找问题、写报告。现在多了一步前置动作——先判断这个项目有没有值得造的工具，如果有，先把工具造出来。这一步的成本不低，但它带来的收益不只是一次审计的结果。工具会留在生态里，下一个审计员、下一个开发者都能用。Trail of Bits 这次交出去的，除了漏洞清单，还有四件能继续跑的工具和一个被证明可用的工作流。对审计这门生意来说，交付物的定义本身在变。
