Formal Verification of Agentic Systems over Operational Data

• URL: http://arxiv.org/abs/2608.03609v1
• Date: Tue, 04 Aug 2026 13:01:30 GMT
• Title: Formal Verification of Agentic Systems over Operational Data
• Abstract summary: Agentic systems driven by large language models (LLMs) are increasingly deployed in real-world where they act on persistent operational data.<n>Existing approaches do not provide such system-level guarantees.<n>We study here the verification of agentic systems comprising a single LLM and a tool orchestration harness over relational operational data.
• Score: 59.98246281888422
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• 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.

Related papers

• Execution-First Synthetic Tool-Use Trace Generation for LLM Agents [10.291533584425252]
  SyntheticAgentTraceQA is an execution- first framework for generating scalable supervision data for tool- augmented agents.<n>We evaluate the framework across four tool ecosystems and use the resulting data to fine-tune and evaluate Qwen model variants.
  arXiv  Detail & Related papers  (2026-07-31T08:52:26Z)
• PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
  We present PhyAgentOS, a foundation delivering scheduling, verification, memory, benchmarking, and safety as system-level services.<n>Its Session-Centered treats a session, not an action, as the minimum unit of scheduling, compatibility, supervised execution, evidence collection, and acceptance.<n>SessionVerifier distinguishes execution termination from semantic task completion via evidence-grounded verdicts of success, failure, or replan.<n> Benchmarking reuses the deployment session and verification path, so results trace to real execution.
  arXiv  Detail & Related papers  (2026-07-18T04:46:53Z)
• VADAOrchestra: Neurosymbolic Orchestration of Adaptive Reasoning Workflows [47.70653885737167]
  Decision-making in real-world settings rarely follows a fixed script. Instead, it unfolds as a dynamic reasoning process.<n>We introduce VADAOrchestra, a neurosymbolic framework that models complex as evolving reasoning processes.
  arXiv  Detail & Related papers  (2026-06-21T13:10:48Z)
• GRACE-DS: a Guarded Reward-guided Agent Correction Environment in Data Science [39.146761527401424]
  GRACE-DS is a Reward-guided Agent Correction Environment in Data Science for pre-deployment evaluation of LLM-powered AutoML agents.<n>It exposes agents to realistic workflow stages, from planning and data inspection through feature engineering, model development, validation, and code repair to final submission.<n>These results establish GRACE-DS as a robust platform for assessing the capacity of LLM-based AutoML agents to execute machine learning under production-like conditions.
  arXiv  Detail & Related papers  (2026-06-14T19:58:06Z)
• An Organization-Scoped LLM Agent Runtime Architecture for Regulated Cybersecurity Operations [0.3013679260442808]
  Regulated cybersecurity lack a runtime substrate that enforces organization-level scope.<n>Recent large language model (LLM) agent systems report strong results on isolated cybersecurity tasks.<n>This paper proposes an organization-scoped agent runtime architecture for financial cybersecurity.
  arXiv  Detail & Related papers  (2026-05-28T21:51:38Z)
• Towards Security-Auditable LLM Agents: A Unified Graph Representation [22.355591892994642]
  We propose Agent-BOM, a unified structural representation for agent security auditing.<n>We show that Agent-BOM can reconstruct stealthy attack chains, including cross-session memory poisoning and tool misuse.<n>Agent-BOM provides a unified and auditable foundation for root-cause analysis and security adjudication in complex agentic ecosystems.
  arXiv  Detail & Related papers  (2026-05-07T18:14:29Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• Towards Verifiably Safe Tool Use for LLM Agents [53.55621104327779]
  Large language model (LLM)-based AI agents extend capabilities by enabling access to tools such as data sources, APIs, search engines, code sandboxes, and even other agents.<n>LLMs may invoke unintended tool interactions and introduce risks, such as leaking sensitive data or overwriting critical records.<n>Current approaches to mitigate these risks, such as model-based safeguards, enhance agents' reliability but cannot guarantee system safety.
  arXiv  Detail & Related papers  (2026-01-12T21:31:38Z)
• AGENTIF: Benchmarking Instruction Following of Large Language Models in Agentic Scenarios [51.46347732659174]
  Large Language Models (LLMs) have demonstrated advanced capabilities in real-world agentic applications.<n>AgentIF is the first benchmark for systematically evaluating LLM instruction following ability in agentic scenarios.
  arXiv  Detail & Related papers  (2025-05-22T17:31:10Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.