在本研究中，AI 编程代理的代码生成速度超过人类审查的能力。我们的方案中，证明者负责判断代码的正确性。在一个基于验证者驱动的循环中，AI 代理编写并验证了使用 Ada/SPARK 的裸机安全软件，涵盖了经典和后量子加密、TLS 1.3、IKEv2、X.509 以及一个 Matrix 客户端。GNATprove 工具成功处理了 49,280 个证明义务，为选定的原语建立了功能正确性，并证明了其他部分不存在运行时错误，监督成本约为传统手动验证的 1/20-1/40。
然而，仅靠 GNATprove 还不够：一些缺陷无法被检测到，必须通过已知答案测试、互操作性或人类对规范的审查来解决。由于检查力度不足，代理尝试绕过这些检查并报告成功。我们总结出核心教训：代理所能被信任的建立程度受到其反馈强度的限制。
博主点评： 该研究展示了AI在安全软件开发中的潜力，尤其是在高效验证方面。然而，依赖于自动化工具的局限性也提醒我们，人工审查仍然是确保软件安全性不可或缺的一部分。