# Formal Verification of Agentic Systems over Operational Data

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use.
- Builds on 14 of its 30 references that are in the map.
- First posted on arXiv 4 Aug 2026.

## Placed in

- LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/)

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

- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [WebArena: A Realistic Web Environment for Building Autonomous Agents](https://mlsanity.com/paper/2307.13854/) (2023)
- [Quantifying Language Models' Sensitivity to Spurious Features in Prompt Design or: How I learned to start worrying about prompt formatting](https://mlsanity.com/paper/2310.11324/) (2023)
- [τ2-Bench: Evaluating Conversational Agents in a Dual-Control Environment](https://mlsanity.com/paper/2506.07982/) (2025)
- [State of What Art? A Call for Multi-Prompt LLM Evaluation](https://mlsanity.com/paper/2401.00595/) (2023)
- [ToolSandbox: A Stateful, Conversational, Interactive Evaluation Benchmark for LLM Tool Use Capabilities](https://mlsanity.com/paper/2408.04682/) (2024)
- [AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM Agents](https://mlsanity.com/paper/2503.18666/) (2025)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [ShieldAgent: Shielding Agents via Verifiable Safety Policy Reasoning](https://mlsanity.com/paper/2503.22738/) (2025)
- [SAFER: A Structure-free Approach for Certified Robustness to Adversarial Word Substitutions](https://mlsanity.com/paper/2005.14424/) (2020)
- [Enforcing Temporal Constraints for LLM Agents](https://mlsanity.com/paper/2512.23738/) (2025)
- [ProbGuard: Proactive Runtime Monitoring for LLM Agent Safety via Probabilistic Prediction](https://mlsanity.com/paper/2508.00500/) (2025)
- [The Attack and Defense Landscape of Agentic AI: A Comprehensive Survey](https://mlsanity.com/paper/2603.11088/) (2026)
- [Verification of Agent-Based Artifact Systems](https://mlsanity.com/paper/1301.2678/) (2013)

## Abstract (arXiv)

Agentic systems driven by large language models (LLMs) are increasingly deployed in real-world workflows where they act on persistent operational data. Before deployment, these systems need to be verified against business requirements that govern workflow execution and data evolution. However, existing approaches do not provide such system-level guarantees, as they mainly constrain or analyse behaviour at the agent's interface level. We study here the verification of agentic systems comprising a single LLM and a tool orchestration harness over relational operational data. We formalise them as Stateful Tool-Enabled Agentic Deployments (STEADs), give their semantics, define the problem of verifying them against First-Order Computation Tree Logic (FO-CTL) specifications, and show that it is undecidable. We identify sufficient conditions for exact preservation of FO-CTL specifications under a finite-domain restriction, over which verification is PSPACE-complete. The key requirement is that renaming opaque identifiers in the data must correspondingly rename the selected tool calls. We show that LLM-driven agents can violate this condition and introduce a canonical deployment wrapper that guarantees it for arbitrary base agents while preserving already-equivariant behaviour. We prove that computing canonical representations required by this construction is graph-isomorphism-hard. Finally, we illustrate our framework on an LLM agent orchestrating a case-management workflow.