在正式启动 Miden zkVM 的安全审计之前，Trail of Bits 选择了一条不寻常的路径：先让 Agent 花费六个月时间，从零搭建一套专门服务于审计的工具链。这套工具并非通用产品，而是围绕 Miden 的底层语言 MASM 定制，涵盖 LSP 服务器、反编译器、静态分析引擎以及 Lean VM 执行器模型四个组成部分。

工具链的回报直接体现在漏洞发现上。其中，最严重的问题允许恶意 prover 伪造 Falcon 签名，进而盗取资金。这一高危漏洞若未被识别，可能对依赖 Miden zkVM 的系统造成实质性资产风险。

静态分析引擎在审查过程中定位了 400 多处类型验证缺陷，覆盖范围超出人工审查通常能触及的边界。与此同时，Lean 形式化工作产出了 95 个机器验证的正确性证明，为关键逻辑提供了可被机器检验的保障。

除上述系统性发现外，这套工具还暴露出两个单元测试未能捕获的细微 bug。这一结果说明，在 zkVM 这类复杂系统中，传统测试手段存在盲区，而针对性的自建工具与形式化方法能够形成有效补充。对 AI 行业而言，该案例展示了 Agent 在安全审计工具构建环节的工程价值。