安全公司越来越多地利用人工智能超越代理代码审查，增强安全审计，在实际代码审查前构建定制工具和正式模型。例如，在审查缺乏开发工具的Miden虚拟机时，代理花费六个月时间创建了LSP服务器、反编译器、静态分析引擎和虚拟机执行器的精益模型。这些工具发现了重大安全漏洞，例如未经验证的校验者输入，可能导致Falcon签名伪造和资金盗窃。精益模型还为Miden核心库的大量内容产生了95个机器校验的正确性证明。Miden虚拟机是一款新型零知识虚拟机，拥有自己的汇编语言（MASM），由于其堆栈机架构和缺乏开发工具，带来了独特的评审挑战。为此，团队优先构建关键工具，首先是LSP服务器和VS Code扩展，用于语法高亮、代码导航和指令文档。接着，开发了MASM过程的反编译器，尽管存在隐式栈操作和未声明签名等复杂性，仍能提供高层语义信息。该反编译器历时数月，带来了宝贵的内部分析框架和静态分析的中间表示。利用这一中间表示，团队构建了一个静态分析的抽象解释引擎，实现了验证验证者提供的值、强制类型约束并确保局部变量初始化的通行证。这导致发现了400多个潜在的类型验证改进和一个高严重性漏洞：mod_12289过程中一个受限不足的建议值。该漏洞使恶意校验者能够操控剩余值，可能伪造Falcon签名并耗尽Miden账户。除了发现漏洞外，代理还探索了利用精益进行形式验证，建模Miden虚拟机执行器，并自动将MASM过程转换为精益。这种由代理驱动的形式建模为二进制算术组件提供了95个正确性证明，揭示了现有单元测试遗漏的两个细微缺陷：64位右转（rotr）中的一个边缘案例和256位乘法（wrapping_mul）中的一个问题。这些先进的工具和形式建模工作，得益于近期人工智能代理的进步，显著提升了安全审查的深度和质量，这在时间和资源限制下是此前难以实现的准备工作水平。