Search papers, labs, and topics across Lattice.
This paper investigates the formal verification of agentic systems driven by large language models (LLMs) in operational contexts, addressing the gap in existing methods that only analyze agent behavior at the interface level. The authors introduce the concept of Stateful Tool-Enabled Agentic Deployments (STEADs) and demonstrate that verifying these systems against First-Order Computation Tree Logic (FO-CTL) specifications is undecidable, while providing sufficient conditions under which verification becomes PSPACE-complete. A key innovation is the development of a canonical deployment wrapper that ensures compliance with FO-CTL specifications by managing opaque identifiers, which is critical for maintaining system integrity in real-world applications.
LLM-driven agents can violate verification conditions, but a new canonical wrapper can enforce compliance while preserving behavior.
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.
