# Trail of Bits 用 AI Agent 给 Miden zkVM 审计造了全套工具：LSP、反编译器、Lean 证明

> 原标题：Trail of Bits 用 Agent 为 Miden zkVM 审计自建 LSP、反编译器和 Lean 形式化证明

- 来源：AI HOT 精选
- 发布时间：2026-09-18T11:00:00.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/57337
- 原文：https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai

## 摘要

Trail of Bits 在审计 Miden zkVM 之前，花了六个月让 AI agent 从零搭建了一套工具链，包括一个 LSP 服务器（让代码能跳转、看文档）、一个反编译器、一个静态分析引擎，以及一套 Lean 形式化模型。这些工具发现了真实漏洞，比如一个未校验的输入能让恶意证明者伪造 Falcon 签名、偷走账户资金。Lean 那边产出了 9...

## 推荐理由

Trail of Bits 花了六个月让 AI agent 从零搭了一套审计工具链，还挖出了能偷钱的真实漏洞，这是 AI 辅助安全审计里少见的硬核案例。三条 HKR 都踩中了，但安全垂直领域太专，普通读者门槛偏高，扣 3 分。

## 锐评

这篇博客最有意思的地方不是“AI 又找到漏洞了”，而是他们把 AI agent 用在了审计准备阶段：给一个全新的、连 IDE 支持都没有的定制汇编语言（MASM）搭了一整套工具链。这包括让代码能跳转看文档的 LSP 服务器、一个反编译器、一个静态分析引擎，以及一套 Lean 形式化模型。这些工具不是摆设，它们直接挖出了一个真实漏洞：一个没做校验的输入能让恶意证明者伪造 Falcon 签名，偷走账户资金。Lean 那边产出了 95 个机器验证的正确性证明，覆盖了核心库的一大块。

不过文章在关键信息上很模糊。它只提到 Claude 搭了 LSP 原型，其他工具用了什么模型、花了多少 token、成本多少，全都没说。这让人很难判断这套做法的可复制性——是砸了大量算力才跑通，还是真的可以低成本复用？另外，这些工具发现漏洞的能力和人工审计相比到底提升了多少，也没有量化对比。

还缺一个关键视角：这些由 AI 生成的工具本身会不会引入新的盲区？如果 LSP 或静态分析引擎有 bug，会不会导致审计人员漏掉某些类型的漏洞？正文没讨论这一点。