Google 推出了 AlphaProof Code，这是一个旨在自动化繁重的形式化验证过程的多 LLM Agent 框架。通过模拟研究团队的工作流程，该系统将为软件（如 libsignal Rust 库）生成和验证数学证明的工作拆分开来，以确保代码的行为完全符合规范。
AlphaProof Code 框架
该系统作为一个多 LLM Agent 框架运行，将形式化验证任务分配给不同的 Agent。它遍历代码库以编写并执行 Lean 或 Rocq 代码，这些语言用于表达数学证明并验证软件属性。
与可能仅生成功能性代码的标准编码 Agent 不同，AlphaProof Code 的目标是证明实现与特定的数学模型相匹配。这种方法旨在超越“尽力而为”的编码，转向具有数学保证的软件安全性。
测试与漏洞检测
为了验证该系统，研究人员在软件实现中重新引入了已知的安全漏洞，以观察 Agent 是否能捕捉到它们。Hacker News 上的评论者指出，这一过程是区分“只是在做某事”的 AI 与“正确地在做某事”的 AI 的关键方式。
该项目专门针对 libsignal Rust 库。通过将软件转换为形式化的数学模型，系统可以识别出在标准人工审查或传统模糊测试中可能被忽略的细微逻辑不一致。
局限性与人类监督
尽管具备这些能力，可验证的范围仍然相对狭窄。一位评论者认为，虽然该系统擅长证明程序不会崩溃，但要证明像“此压缩始终能解压回相同内容”或“此加密是安全的”这样复杂的属性要困难得多。
此外，还存在 AI “作弊”的风险，因为它负责编写用于验证自身的代码。用户建议这需要一种对抗性方法，即必须由第二个提示或人类审查员审计 AI 生成的 Lean 代码，以确保证明在逻辑上是健全的。