审计还没开始，AI先把工具造出来了

Trail of Bits 9 月 18 日写了一篇 Miden zkVM 审计复盘。Miden 的核心库用了自定义汇编语言 MASM，几乎没有 IDE 支持、代码导航和检查器。团队没有直接把 Agent 丢进代码库里找问题，先问了一个很实际的问题：审计开始前，缺什么工具？

接下来的六个月，Claude 和 Codex 做了 LSP、VS Code 扩展、反编译器、静态分析器和 Lean 执行器模型。Agent 负责规划、写代码和互相检查，人负责确定要证明的性质、看结果是否说得通。

审计时，静态分析找出 400 多处类型校验可以加强的位置，全部能从公开 API 触达。其中有一个高危问题：程序没有验证 prover 提供的余数，攻击者可能利用它伪造 Falcon 签名，抽走由这类密钥控制的资金。原文说的是可被利用的风险，没有披露真实资金已经被盗。

Lean 还产出了 95 个机器验证的正确性证明，并找到了两个现有单元测试没覆盖到的细小 bug。一个和 64 位右旋有关，另一个出在 256 位乘法的栈处理上。

很多 AI 安全演示都在说 Agent 能一次读多少代码、报出多少漏洞。Trail of Bits 这篇文章换了个顺序：先让 Agent 把人想要的工具做出来，再让工具和人一起审计。LSP 解决阅读问题，反编译器把陌生汇编变成可分析的中间表示，静态分析和 Lean 负责反复检查。

这条路的经济账也变了。以前很难为一个结果不确定的半年工具项目拿预算；现在失败的试验主要消耗模型调用和工程时间。工具如果能留在团队里，下一次审计还能继续用。

这是一家安全公司的单个项目，代码有明确范围，团队也有足够时间把工具做深。普通团队照抄六个月周期，未必划算。已有成熟编译器、类型系统和测试的项目，新增工具的收益会小很多；自定义语言、协议和数据格式，才更适合先让 Agent 补基础设施。

形式化证明也只证明写下来的性质。定理写错、模型漏掉边界，证明照样能通过。Trail of Bits 仍然需要人工审计定理和高危发现，说明 Agent 负责扩大检查面，人负责确认问题是否属于真实风险。