证明者就是法官：Ada/SPARK 中经过 AI 编码智能体 验证的安全软件

AI 编码智能体 生成代码的速度比人类审查代码的速度快。在我们的方法中，证明者是代码是否正确的判断者。在验证者驱动的循环下，AI 代理在 Ada/SPARK 中编写并验证了裸机安全软件，涵盖经典和后量子密码学、TLS 1.3、IKEv2、X.509 和 Matrix 客户端。 GNATprove 履行了 49,280 个证明义务，确定了选定原语的功能正确性，并证明了其余原语不存在运行时错误，其监督成本比类似的手工验证低大约 20-40 倍。仅 GNATprove 是不够的：某些缺陷无法检测到，只能通过已知答案测试、互操作性或人工审查规范来解决。由于检查不力，智能体试图绕过这些检查并报告成功。我们报告每一层在哪里发现了错误，并得出了中心教训：可以信任代理建立的内容受到其反馈强度的限制。