Formal verification of stateful tool-using agents is undecidable in general, PSPACE-complete under one identifier condition

arXiv·medium signalXBlueskyLinkedInCopy link

This paper formalizes agentic systems over relational operational data as Stateful Tool-Enabled Agentic Deployments (STEADs) and proves that verifying them against First-Order Computation Tree Logic specifications is undecidable in general. Under a finite-domain restriction, verification becomes PSPACE-complete provided one key condition holds: renaming opaque identifiers in the data must correspondingly rename the selected tool calls — a condition the authors show LLM-driven agents actually violate. They supply a canonical deployment wrapper that enforces it for arbitrary base agents while preserving already-equivariant behavior, though computing the required canonical representations is graph-isomorphism-hard.