Proof Shows AI Agent Behavior Resists Formal Verification

No algorithm can verify AI agent behavior against a rule set in the general case, a new proof posted to arXiv shows.

It matters for anyone building agents on live data who wants proof, not just testing, that an agent won't take a forbidden action. More compute doesn't close the gap. The paper frames it as a fundamental limit, not a resource problem.

The paper formalizes these systems, agents that call tools against changing data, as Stateful Tool-Enabled Agentic Deployments. It checks their behavior against First-Order CTL specs, the temporal logic formalism used to state what an agent must or must never do.

Restrict the data to a finite domain and the problem becomes solvable, PSPACE-complete instead of undecidable. That only holds if renaming an opaque identifier in the data correspondingly renames which tool calls the agent picks. The paper shows real LLM-driven agents violate that condition.

The authors built a wrapper that enforces the condition anyway. Computing the canonical representation it needs is graph-isomorphism-hard, a problem with no known fast algorithm. Nothing here ships Monday.