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

• URL: http://arxiv.org/abs/2607.14340v1
• Date: Wed, 15 Jul 2026 20:09:05 GMT
• Title: The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK
• Abstract summary: In 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.<n>GNATprove discharged 49,280 proof obligations, established functional correctness for selected primitives, and proved the absence of run-time errors for the rest.<n>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.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• Adversarial Testing of Automated Program Repair Agents for Security Vulnerabilities [14.543680943818975]
  Software agents with Large Language Models (LLMs) are designed for Automated Program Repair (APR) tasks.<n>Can we trust an APR agent to produce both correct and secure code in such situations?<n>What if attackers target production APR agents with adversarial issues that seem benign but may influence the agents to produce correct but insecure code?
  arXiv  Detail & Related papers  (2026-09-14T17:53:49Z)
• Zero-Knowledge Predicate Proofs Between AI Agents: A Measured, Cross-Protocol Gateway and the Source-Integrity Gap [0.0]
  Multi-agent AI platforms move quickly from staging to production, but the way agents establish trust remains rudimentary.<n>We take provable data minimisation between agents from proposal to running system.<n>A 32-bit threshold predicate proves in 6.2 ms and verifies in 1.0 ms with a 608-byte Bulletproofs proof.
  arXiv  Detail & Related papers  (2026-08-30T23:16:17Z)
• Agent-Driven Verification of Memory Safety for liblzma Decoder Components with VST [32.505127447635864]
  We report on the verification of memory safety for decoder components of liblzma.<n>The verification exposed undefined behavior in raw LZMA1 zero-input handling.<n>Unlike similar work that synthesizes verified code, we verify pre-existing, production-scale C.
  arXiv  Detail & Related papers  (2026-08-30T10:50:56Z)
• $Z^2$-ACT: End-to-End Verifiable Agentic Intent Control for Open 6G RAN [43.15181031994434]
  We propose a zero-knowledge auditable control and zero-trust verifiable agentic intent architecture.<n>A live large language model is used in the non-real-time path to translate operator intents into Intent Contracts.<n>Results indicate improved actuation filtering and attack resilience at modest latency and signaling cost.
  arXiv  Detail & Related papers  (2026-08-21T12:44:03Z)
• Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
  Vero is the first benchmark to evaluate joint implementation and proof at the repository level.<n>It contains 43 multi-module instances from real-world repositories spanning Python, Dafny, Verus, and Coq.<n>To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification.
  arXiv  Detail & Related papers  (2026-08-13T17:41:27Z)
• NiyamAI - An Intent-Bound AI Agent with Cryptographically Verifiable Guardrails using Zero-Knowledge Proofs [0.20215383828623398]
  We introduce Niyam-AI, a framework that makes safety enforcement provable.<n>We evaluate Niyam-AI on 2,000 real-world scenarios from Agent-SafetyBench against NeMo Guardrails, Meta's Llama Prompt Guard 2, and OpenAI's GPT-OSS-Safeguard.<n>Niyam-AI wins 390 discordant scenarios against NeMo (vs 20 losses), 115 against Prompt Guard 2 (vs 13), and 384 against GPT-OSS-Safeguard.
  arXiv  Detail & Related papers  (2026-08-07T12:36:52Z)
• Coding Agents as Test-Suite Auditors: Finding What Official Suites Miss While Approaching What They Catch [47.836680625916266]
  An off-the-shelf coding agent, serving as a test-suite auditor, both builds adversarial test suites to expose what official suites miss.<n>A certification chain determines whether each agent-flagged submission is genuinely buggy without relying on the official judge.<n>On post-cutoff Codeforces problems with no available official suites, the same test-building method leads all five reproduced baselines at every tested input budget.
  arXiv  Detail & Related papers  (2026-08-03T05:24:03Z)
• Is Agent Code Less Maintainable Than Human Code? [17.226150835020146]
  We investigate how agent code compares to human code in maintenance settings.<n>We find that agents are less effective at resolving tasks when building on agent code compared to human code.
  arXiv  Detail & Related papers  (2026-06-19T23:56:14Z)
• Code-Augur: Agentic Vulnerability Detection via Specification Inference [8.217845898392293]
  Audits conducted entirely by autonomous LLM agents are uncovering critical vulnerabilities in software.<n>We propose a security-specification-first paradigm that exposes the agent's tacit assumptions explicitly as security specifications.<n>We realize our approach in Code-Augur, a novel harness for agentic vulnerability detection.
  arXiv  Detail & Related papers  (2026-06-17T02:32:45Z)
• Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization [26.123396123145415]
  We study specification autoformalization: whether LLM agents can translate informal programming problems into faithful formal specifications.<n>We introduce Verus-SpecBench, a benchmark of 581 spec-writing tasks derived from Codeforces problems.<n>Our analysis of failure modes shows that model-generated specs can accept important input assumptions, accept incorrect outputs, & reject valid ones.
  arXiv  Detail & Related papers  (2026-05-26T02:12:48Z)
• Distributional Energy-Based Models for Uncertainty-Aware Structured LLM Reasoning [40.342912574072024]
  Large Language Models produce structured outputs such as travel plans or code solutions.<n>Individual reasoning steps may appear correct while the output as a whole violates budgets, fails test cases, or contradicts earlier deductions.<n>We propose a learned quality scorer with deterministic analytical constraint penalties for verifying structured LLM outputs.
  arXiv  Detail & Related papers  (2026-05-15T17:08:27Z)
• SecureForge: Finding and Preventing Vulnerabilities in LLM-Generated Code via Prompt Optimization [61.91729298584227]
  We introduce SecureForge, an automated pipeline that audits security risks of frontier models and produces auditing-informed secure system prompts.<n>SecureForge first identifies benign prompts that produce statically detectable vulnerabilities, and then amplifies them into a large synthetic prompt corpus of diverse scenarios.<n>On frontier models, SecureForge yields a statistically significant improvement in both unit test success and output security, with output vulnerabilities reduced by up to 48%.
  arXiv  Detail & Related papers  (2026-05-08T18:40:47Z)
• Synthesizing Multi-Agent Harnesses for Vulnerability Discovery [8.518689779459974]
  LLM agents have begun to find real security vulnerabilities that human auditors and automated fuzzers missed for decades.<n>In practice the work is split among several agents, wired together by a harness: the program that fixes which roles exist, how they pass information, which tools each may call, and how retries are coordinated.<n>AgentFlow addresses both limitations with a typed graph DSL whose search space jointly covers agent roles, prompts, tools, communication topology, and coordination protocol.
  arXiv  Detail & Related papers  (2026-04-22T17:27:40Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
  arXiv  Detail & Related papers  (2026-01-30T08:29:01Z)
• Holistic Agent Leaderboard: The Missing Infrastructure for AI Agent Evaluation [87.47155146067962]
  We provide a standardized evaluation harness that orchestrates parallel evaluations across hundreds of tasks.<n>We conduct three-dimensional analysis spanning models, scaffolds, and benchmarks.<n>Our analysis reveals surprising insights, such as higher reasoning effort reducing accuracy in the majority of runs.
  arXiv  Detail & Related papers  (2025-10-13T22:22:28Z)
• VulAgent: Hypothesis-Validation based Multi-Agent Vulnerability Detection [55.957275374847484]
  VulAgent is a multi-agent vulnerability detection framework based on hypothesis validation.<n>It implements a semantics-sensitive, multi-view detection pipeline, each aligned to a specific analysis perspective.<n>On average, VulAgent improves overall accuracy by 6.6%, increases the correct identification rate of vulnerable--fixed code pairs by up to 450%, and reduces the false positive rate by about 36%.
  arXiv  Detail & Related papers  (2025-09-15T02:25:38Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  Large language models (LLMs) are increasingly integrated into real-world personalized applications.<n>The valuable and often proprietary nature of the knowledge bases used in RAG introduces the risk of unauthorized usage by adversaries.<n>Existing methods that can be generalized as watermarking techniques to protect these knowledge bases typically involve poisoning or backdoor attacks.<n>We propose name for harmless' copyright protection of knowledge bases.
  arXiv  Detail & Related papers  (2025-02-10T09:15:56Z)
• CodeAgent: Autonomous Communicative Agents for Code Review [12.163258651539236]
  This work introduces tool, a novel multi-agent Large Language Model (LLM) system for code review automation. CodeAgent incorporates a supervisory agent, QA-Checker, to ensure that all the agents' contributions address the initial review question. Results demonstrate CodeAgent's effectiveness, contributing to a new state-of-the-art in code review automation.
  arXiv  Detail & Related papers  (2024-02-03T14:43:14Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.