Trail of Bits 披露利用 AI 构建定制工具链与 Lean 形式化证明审计 Miden zkVM 的过程

Trail of Bits 发布文章介绍其在审计 Miden VM（一种新的零知识虚拟机）时，利用 AI 代理在六个月内从零构建 LSP 服务器、反编译器、静态分析引擎及 Lean 形式化模型的经验。这些定制工具帮助发现了包括一个允许恶意证明者伪造 Falcon 签名的高危漏洞在内的多个安全问题，并生成了覆盖核心库二进制算术组件的 95 个机器验证正确性证明。