The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK

arXiv:2607.14340 · cs.SE, cs.AI, cs.CR · Submitted 2026-07-15 · Read on arXiv

Tobias Philipp

cs.SE, cs.AI, cs.CR

Submitted: 2026-07-15

Code: https://github.com/tobiasphilipp/experimental-agentic-verified-software

License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/

Terminology

• Verification — 20× in this paper · explained in 2 episodes
• Verifier — 8× in this paper · explained in 2 episodes
• Formal Verification — 4× in this paper · explained in 2 episodes
• SMT solver — 4× in this paper · explained in 2 episodes
• AI Agents — 3× in this paper · explained in 2 episodes
• Formal Methods — 3× in this paper · explained in 3 episodes
• Allocator — 1× in this paper · explained in 1 episode
• Analyzer — 1× in this paper · explained in 1 episode
• Arbiter — 1× in this paper · explained in 1 episode
• Axioms — 1× in this paper · explained in 2 episodes
• Benchmark — 1× in this paper · explained in 2 episodes
• Reward Hacking — 1× in this paper · explained in 8 episodes

Sources

• Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK

Related papers

• Falsification-Based Verification of LLM-Generated Optimization Models: Sound Test Batteries and Their Detection Limits
• GitSkills: A Dataset of Agent Skills on GitHub
• SABER: Benchmarking Operational Safety of LLM Coding Agents in Stateful Project Workspaces
• PackMonitor: Enabling Zero Package Hallucinations Through Decoding-Time Monitoring
• IntentCoding: Amplifying User Intent in Code Generation
• Incentives and Outcomes in Bug Bounties