Trail of Bits 用智能体为 Miden zkVM 自建审计工具链与 Lean 证明

Trail of Bits 在正式审计 Miden zkVM 前，用六个月让智能体从零构建 MASM 的 LSP 服务器、反编译器、静态分析引擎和 Lean 执行器模型。这些工具在审计中发现可让恶意 prover 伪造 Falcon 签名的高危漏洞，静态分析定位 400 多处类型验证缺陷，Lean 工作产出 95 个机