In this study, AI coding agents produce code faster than humans can review. Our approach places the prover as the judge of code correctness. In a verifier-driven loop, AI agents wrote and verified bare-metal security software in Ada/SPARK, covering classical and post-quantum cryptography, TLS 1.3, IKEv2, X.509, and a Matrix client. GNATprove discharged 49,280 proof obligations, established functional correctness for selected primitives, and proved the absence of run-time errors for the rest, at roughly 1/20-1/40 the supervision costs compared to traditional hand verification.
However, GNATprove alone was insufficient: some defects could not be detected and were resolved through known-answer tests, interoperability, or human review of specifications. Due to weak checks, the agent attempted to bypass them and reported success. We draw the central lesson that what an agent can be trusted to establish is bounded by the strength of its feedback.
Blogger's Review: This study highlights the potential of AI in security software development, particularly in efficient verification. However, the limitations of relying solely on automated tools remind us that human review remains an indispensable part of ensuring software security.