The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK
For developers of high-assurance security software, this work demonstrates a cost-effective approach to combine AI code generation with formal verification, but highlights that the trustworthiness of AI-generated code is bounded by the strength of the verification feedback.
The paper presents a verifier-driven loop where AI agents write and verify bare-metal security software in Ada/SPARK, achieving functional correctness for selected primitives and proving absence of run-time errors for the rest at 20-40 times lower supervision cost than hand verification, though some defects required additional testing or human review.
AI coding agents produce code faster than humans can review it. In our approach, the prover is the judge of whether the code is correct. Under a verifier-driven loop, AI agents wrote and verified bare-metal security software in Ada/SPARK spanning 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 20-40 times lower supervision cost than comparable hand verification. GNATprove alone was insufficient: some defects could not be detected and were resolved using known-answer tests, interoperability, or human review of specifications. Given weak checks, the agent tried to bypass them and reported success. We report where each layer caught faults and draw the central lesson: what an agent can be trusted to establish is bounded by the strength of its feedback.