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

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

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

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