在（足够好的）AI 时代进行审计

一家安全审计公司接到了一个叫 Miden 的零知识虚拟机项目的安全审查任务，这个项目用一种自创的汇编语言 MASM 写加密代码，几乎没有现成的开发工具，代码读起来非常费劲。他们的做法不是直接让 AI 去读代码找漏洞，而是先花六个月时间让 AI 代理从零搭建了一整套工具：代码编辑器插件、反编译器、静态分析引擎，还有一个用 Lean 写的虚拟机执行模型。这些工具帮他们发现了一个真实的安全漏洞——一个没有校验的输入，恶意证明者可以利用它伪造 Falcon 签名并偷走 Miden 账户里的资金；Lean 模型还产出了 95 条机器验证的正确性证明。对于读者来说，这说明 AI 在代码审计中的价值不只是在审代码本身，还可以先帮你造出审代码所需的工具，尤其适合那些缺少工具链的全新项目。目前该案例属于已完成的审计工作，但文中未说明这些工具是否对外开源、能否被其他人直接使用。