Formal Verification of Agentic Systems over Operational Data
Alejandro J. Mercado, Alessio Lomuscio
Why It Matters
What makes this one worth your time
As LLM-driven systems become more prevalent in operational workflows, ensuring their compliance with business logic and data integrity is crucial for reliable deployment.
The paper proposes a framework for verifying agentic systems using LLMs against logical specifications, addressing undecidability and complexity issues.
Summary
The paper addresses the formal verification of agentic systems that utilize large language models and tool orchestration over operational data. It introduces the concept of Stateful Tool-Enabled Agentic Deployments (STEADs) and explores their verification against First-Order Computation Tree Logic (FO-CTL) specifications, finding the problem undecidable in general but PSPACE-complete under certain conditions. The paper proposes a canonical deployment wrapper to ensure compliance with these conditions and discusses the computational complexity involved.
Key contributions
- Formalization of Stateful Tool-Enabled Agentic Deployments (STEADs).
- Identification of conditions under which verification is PSPACE-complete.
- Introduction of a canonical deployment wrapper to ensure compliance with verification conditions.
Notable insights
- Verification of agentic systems is undecidable in general but becomes PSPACE-complete under finite-domain restrictions.
- A canonical deployment wrapper can enforce compliance with verification conditions, though it is graph-isomorphism-hard to compute.
Possible limitations
- Not stated in the abstract
Abstract
arXiv:2608.03609v1 Announce Type: new Abstract: 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.