# Agentic Verification of Software Systems arXiv: https://arxiv.org/abs/2511.17330 ยท HTML: https://mlsanity.com/paper/2511.17330/ ## Key facts - Cited by 6 papers in the map (data through 14 Oct 2026). - Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use. - Builds on 30 of its 86 references that are in the map. - First posted on arXiv 21 Nov 2025. ## Placed in - LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/) ## Builds on (most cited first, 30 of 30) - [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020) - [Asleep at the Keyboard? Assessing the Security of GitHub Copilot's Code Contributions](https://mlsanity.com/paper/2108.09293/) (2021) - [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023) - [Large Language Models for Software Engineering: A Systematic Literature Review](https://mlsanity.com/paper/2308.10620/) (2023) - [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020) - [Unified Pre-training for Program Understanding and Generation](https://mlsanity.com/paper/2103.06333/) (2021) - [AutoCodeRover: Autonomous Program Improvement](https://mlsanity.com/paper/2404.05427/) (2024) - [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022) - [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019) - [Fuzz4All: Universal Fuzzing with Large Language Models](https://mlsanity.com/paper/2308.04748/) (2023) - [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023) - [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016) - [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024) - [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023) - [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024) - [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024) - [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023) - [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023) - [Generating Correctness Proofs with Neural Networks](https://mlsanity.com/paper/1907.07794/) (2019) - [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021) - [Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification](https://mlsanity.com/paper/2412.14063/) (2024) - [The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq](https://mlsanity.com/paper/2008.00120/) (2020) - [Proof Automation with Large Language Models](https://mlsanity.com/paper/2409.14274/) (2024) - [Passport: Improving Automated Formal Verification Using Identifiers](https://mlsanity.com/paper/2204.10370/) (2022) - [Cottontail: Large Language Model-Driven Concolic Execution for Highly Structured Test Input Generation](https://mlsanity.com/paper/2504.17542/) (2025) - [Deductive Verification of Unmodified Linux Kernel Library Functions](https://mlsanity.com/paper/1809.00626/) (2018) - [CoqPyt: Proof Navigation in Python in the Era of LLMs](https://mlsanity.com/paper/2405.04282/) (2024) - [Detecting Critical Bugs in SMT Solvers Using Blackbox Mutational Fuzzing](https://mlsanity.com/paper/2004.05934/) (2020) - [PAT-Agent: Autoformalization for Model Checking](https://mlsanity.com/paper/2509.23675/) (2025) - [Lemma Functions for Frama-C: C Programs as Proofs](https://mlsanity.com/paper/1811.05879/) (2018) ## Built on by (most cited first, 6 of 6) - [Certified Program Synthesis with a Multi-Modal Verifier](https://mlsanity.com/paper/2604.16584/) (2026) - [Toward an Agentic Infused Software Ecosystem](https://mlsanity.com/paper/2602.20979/) (2026) - [Skills for the future software profession: beyond agentic AI!](https://mlsanity.com/paper/2606.21894/) (2026) - [Specula: Scaling formal specifications for autonomous model checking of system code](https://mlsanity.com/paper/2607.25333/) (2026) - [Schwarz: Solver-Aware Agentic Program Verification](https://mlsanity.com/paper/2608.30803/) (2026) - [ProsaBuddy: Assisting Mechanized Real-Time Schedulability Analysis with LLM-based Agents](https://mlsanity.com/paper/2610.03796/) (2026) ## Abstract (arXiv) Automatically generated code is gaining traction recently, owing to the prevalence of Large Language Models (LLMs). Further, the AlphaProof initiative has demonstrated the possibility of using AI for general mathematical reasoning. Reasoning about computer programs (software) can be accomplished via general mathematical reasoning; however, it tends to be more structured and richer in contexts. This forms an attractive proposition, since then AI agents can be used to reason about voluminous code that gets generated by AI. In this work, we present a first LLM agent, AutoRocq, for conducting program verification. Unlike past works, which rely on extensive training of LLMs on proof examples, our agent learns on-the-fly and improves the proof via an iterative refinement loop. The iterative improvement of the proof is achieved by the proof agent communicating with the Rocq (formerly Coq) theorem prover to get additional context and feedback. The final result of the iteration is a proof derivation checked by the Rocq theorem prover. In this way, our proof construction involves autonomous collaboration between the proof agent and the theorem prover. This autonomy facilitates the search for proofs and decision-making in deciding on the structure of the proof tree. Experimental evaluation on SV-COMP benchmarks and on Linux kernel modules shows promising efficacy in achieving automated program verification. As automation in code generation becomes more widespread, we posit that our proof agent can be potentially integrated with AI coding agents to achieve a generate and validate loop, thus moving closer to the vision of trusted automatic programming.