AI 如何助力 Miden 零知识虚拟机安全审计

Security auditing in the age of (good enough) AI

在 Miden 零知识虚拟机的安全审计中，我们利用 AI 代理在代码审查前构建了全套自定义工具。面对 MASM 汇编语言缺乏开发工具的困境，我们花费六个月让 AI 从零搭建了 LSP 服务器、反编译器、静态分析引擎以及 Lean 形式化模型。这些工具不仅发现了包括 Falcon 签名伪造在内的严重漏洞，还生成了 95 个机器验证的正确性证明。这次实践表明，在代码审查开始前，利用 AI 构建基础设施能显著提升审计的深度与质量。