# AgentGuard: Runtime Verification of AI Agents

arXiv: https://arxiv.org/abs/2509.23864 · HTML: https://mlsanity.com/paper/2509.23864/

## Key facts

- Cited by 17 papers in the map (data through 14 Oct 2026).
- Placed in Agent threats, guardrails and governance, one of 16 directions in LLM agents and tool use.
- Builds on 19 of its 28 references that are in the map.
- First posted on arXiv 28 Sep 2025.

## Placed in

- LLM agents and tool use / [Agent threats, guardrails and governance](https://mlsanity.com/agents/agent-threats-guardrails-and-governance/)

## Builds on (most cited first, 19 of 19)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [RepairAgent: An Autonomous, LLM-Based Agent for Program Repair](https://mlsanity.com/paper/2403.17134/) (2024)
- [TRiSM for Agentic AI: A Review of Trust, Risk, and Security Management in LLM-based Agentic Multi-Agent Systems](https://mlsanity.com/paper/2506.04133/) (2025)
- [Formal-LLM: Integrating Formal Language and Natural Language for Controllable LLM-based Agents](https://mlsanity.com/paper/2402.00798/) (2024)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [A Survey on Context-Aware Multi-Agent Systems: Techniques, Challenges and Future Directions](https://mlsanity.com/paper/2402.01968/) (2024)
- [The Fusion of Large Language Models and Formal Methods for Trustworthy AI Agents: A Roadmap](https://mlsanity.com/paper/2412.06512/) (2024)
- [VeriPlan: Integrating Formal Verification and LLMs into End-User Planning](https://mlsanity.com/paper/2502.17898/) (2025)
- [Agentic AI Needs a Systems Theory](https://mlsanity.com/paper/2503.00237/) (2025)
- [AI Agents: Evolution, Architecture, and Real-World Applications](https://mlsanity.com/paper/2503.12687/) (2025)
- [Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification](https://mlsanity.com/paper/2506.04592/) (2025)
- [Formally Specifying the High-Level Behavior of LLM-Based Agents](https://mlsanity.com/paper/2310.08535/) (2023)
- [Probabilistic Model Checking and Autonomy](https://mlsanity.com/paper/2111.10630/) (2021)
- [Saarthi: The First AI Formal Verification Engineer](https://mlsanity.com/paper/2502.16662/) (2025)
- [Fully Automatic Neural Network Reduction for Formal Verification](https://mlsanity.com/paper/2305.01932/) (2023)
- [Supporting Software Formal Verification with Large Language Models: An Experimental Study](https://mlsanity.com/paper/2507.04857/) (2025)
- [Step-Wise Formal Verification for LLM-Based Mathematical Problem Solving](https://mlsanity.com/paper/2505.20869/) (2025)
- [Hey AI, Generate Me a Hardware Code! Agentic AI-based Hardware Design & Verification](https://mlsanity.com/paper/2507.02660/) (2025)
- [A Short Survey on Formalising Software Requirements using Large Language Models](https://mlsanity.com/paper/2506.11874/) (2025)

## Built on by (most cited first, 17 of 17)

- [AgentRx: Diagnosing AI Agent Failures from Execution Trajectories](https://mlsanity.com/paper/2602.02475/) (2026)
- [SkillLearnBench: Benchmarking Continual Learning Methods for Agent Skill Generation on Real-World Tasks](https://mlsanity.com/paper/2604.20087/) (2026)
- [From Fluent to Verifiable: Claim-Level Auditability for Deep Research Agents](https://mlsanity.com/paper/2602.13855/) (2026)
- [Agentic Services Computing](https://mlsanity.com/paper/2509.24380/) (2025)
- [Traversal-as-Policy: Log-Distilled Gated Behavior Trees as Externalized, Verifiable Policies for Safe, Robust, and Efficient Agents](https://mlsanity.com/paper/2603.05517/) (2026)
- [TriCEGAR: A Trace-Driven Abstraction Mechanism for Agentic AI](https://mlsanity.com/paper/2601.22997/) (2026)
- [Toward Safe LLM Agents: A Survey of Specification, Verification, and Enforcement](https://mlsanity.com/paper/2608.14590/) (2026)
- [From Thinker to Society: Security in Hierarchical Autonomy Evolution of AI Agents](https://mlsanity.com/paper/2603.07496/) (2026)
- [Alignment Contracts for Agentic Security Systems](https://mlsanity.com/paper/2605.00081/) (2026)
- [AIVV: Neuro-Symbolic LLM Agent-Integrated Verification and Validation for Trustworthy Autonomous Systems](https://mlsanity.com/paper/2604.02478/) (2026)
- [From CRUD to Autonomous Agents: Formal Validation and Zero-Trust Security for Semantic Gateways in AI-Native Enterprise Systems](https://mlsanity.com/paper/2604.25555/) (2026)
- [TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples](https://mlsanity.com/paper/2605.07935/) (2026)
- [Ceci n'est pas une pipe: AI systems as semantic abstractions](https://mlsanity.com/paper/2607.09489/) (2026)
- [Beyond Component Testing: Validating Agentic AI Systems](https://mlsanity.com/paper/2607.29405/) (2026)
- [ATLAS: Discovering Agent Strategies through LLM-Guided Abstraction and Automata Learning](https://mlsanity.com/paper/2608.14352/) (2026)
- [Agents as Software: A Programming Languages Agenda for Agent Reliability](https://mlsanity.com/paper/2609.32198/) (2026)
- [Sentry: Learning to Recover from LLM Agent Failures at Test Time](https://mlsanity.com/paper/2610.02994/) (2026)

## Abstract (arXiv)

The rapid evolution to autonomous, agentic AI systems introduces significant risks due to their inherent unpredictability and emergent behaviors; this also renders traditional verification methods inadequate and necessitates a shift towards probabilistic guarantees where the question is no longer if a system will fail, but the probability of its failure within given constraints. This paper presents AgentGuard, a framework for runtime verification of Agentic AI systems that provides continuous, quantitative assurance through a new paradigm called Dynamic Probabilistic Assurance. AgentGuard operates as an inspection layer that observes an agent's raw I/O and abstracts it into formal events corresponding to transitions in a state model. It then uses online learning to dynamically build and update a Markov Decision Process (MDP) that formally models the agent's emergent behavior. Using probabilistic model checking, the framework then verifies quantitative properties in real-time.