arxivcs.SEcs.AIcs.CR2026-07-15
The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK
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 crypto…