Formalizing the Safety, Security, and Functional Properties of Agentic AI Systems

TL;DR

The paper tackles the fragmentation of inter-agent protocols by proposing two foundational models—the Host Agent (HA) and the Task Lifecycle—to form a unified semantic framework for safety, security, and functionality in agentic AI systems. It defines 31 formal properties (17 for the HA and 14 for the Task Lifecycle) expressed in temporal logic to enable rigorous verification of system behavior and to detect coordination edge cases such as deadlocks and privilege escalation. By integrating MCP and A2A within this framework, the approach supports end-to-end task orchestration across heterogeneous agents and tools. A case study demonstrates how architectural controls against adversarial behavior can be verified using these properties, highlighting evaluation points like intent integrity, trust anchoring, delegation monitoring, and zero-trust communications. The work articulates a domain-agnostic path toward verifiable, robust agentic AI deployments and outlines future directions for automatic property violation detection derived from code and model extraction.

Abstract

Agentic AI systems, which leverage multiple autonomous agents and Large Language Models (LLMs), are increasingly used to address complex, multi-step tasks. The safety, security, and functionality of these systems are critical, especially in high-stakes applications. However, the current ecosystem of inter-agent communication is fragmented, with protocols such as the Model Context Protocol (MCP) for tool access and the Agent-to-Agent (A2A) protocol for coordination being analyzed in isolation. This fragmentation creates a semantic gap that prevents the rigorous analysis of system properties and introduces risks such as architectural misalignment and exploitable coordination issues. To address these challenges, we introduce a modeling framework for agentic AI systems composed of two foundational models. The first, the host agent model, formalizes the top-level entity that interacts with the user, decomposes tasks, and orchestrates their execution by leveraging external agents and tools. The second, the task lifecycle model, details the states and transitions of individual sub-tasks from creation to completion, providing a fine-grained view of task management and error handling. Together, these models provide a unified semantic framework for reasoning about the behavior of multi-AI agent systems. Grounded in this framework, we define 17 properties for the host agent and 14 for the task lifecycle, categorized into liveness, safety, completeness, and fairness. Expressed in temporal logic, these properties enable formal verification of system behavior, detection of coordination edge cases, and prevention of deadlocks and security vulnerabilities. Through this effort, we introduce the first rigorously grounded, domain-agnostic framework for the systematic analysis, design, and deployment of correct, reliable, and robust agentic AI systems.

Figures (2)

• Figure 1: Overview of the host agent model with an Agentic AI system. The model mediates user interactions and coordinates task execution across a heterogeneous set of external entities, specifically MCP anthropicMCP and A2A googleA2A servers. Internally, the HA employs a modular design comprising the Host Agent Core (), the Orchestrator (), and the Communication Layer (). The execution lifecycle proceeds as follows: processes the user prompt and resolves intent; enables dynamic discovery of external entities; , , and collaborate on DAG-based sub-task planning. Execution involves secure task invocation managed by , followed by aggregation and resolution of results by before the final response returns to the user. This architecture supports scalable, interpretable, and compositional collaboration among autonomous AI agents and tools ().
• Figure 2: The task lifecycle model that details sub-task state transitions from creation to termination. The lifecycle begins in the CREATED state, proceeds through AWAITING DEPENDENCY (if prerequisites exist), and moves to READY. Execution transitions either directly to IN PROGRESS (internal handling) or via DISPATCHING (external delegation). Successful execution leads to COMPLETED. Failures transition to FAILED, enabling recovery via RETRY SCHEDULED or FALLBACK SELECTED, before terminating in ERROR. Sub-tasks may be CANCELED at any stage.