Search papers, labs, and topics across Lattice.
This paper explores the use of AI coding agents to autonomously produce and verify security software in Ada/SPARK, achieving significant efficiency improvements in code verification. By implementing a verifier-driven loop, the authors demonstrated that AI agents could write and validate complex software, including cryptographic protocols, while discharging 49,280 proof obligations with a supervision cost 20-40 times lower than traditional methods. However, the study also highlights limitations in the verification process, revealing that some defects were undetected and required additional testing and human oversight, emphasizing the importance of robust feedback mechanisms for AI agents.
AI agents can autonomously verify security software with astonishing efficiency, but their trustworthiness is limited by the strength of their feedback mechanisms.
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.
