TLDR: This research introduces a new modeling framework for agentic AI systems to address the fragmentation of communication protocols (like MCP and A2A) that currently hinders rigorous analysis of safety, security, and functionality. The framework consists of two foundational models: the Host Agent model, which formalizes the top-level entity orchestrating tasks, and the Task Lifecycle model, which details sub-task states and transitions. By providing a unified semantic framework, these models enable formal verification of 31 critical properties (liveness, safety, completeness, fairness) using temporal logic, helping to detect coordination edge cases, prevent deadlocks, and mitigate security vulnerabilities in complex multi-AI agent environments.
Agentic AI systems, which utilize multiple autonomous agents and Large Language Models (LLMs), are becoming increasingly vital for tackling complex, multi-step tasks. Imagine an automated financial planner that takes your request to ‘create a budget and invest $1,000.’ This seemingly simple task is broken down into subtasks, handled by various specialized agents: a data agent gathers market information, a planning agent calculates risk, and a transaction agent executes the investment. These agents communicate and coordinate to achieve the overall goal.
However, the current landscape of inter-agent communication is fragmented. Protocols like the Model Context Protocol (MCP) for tool access and the Agent-to-Agent (A2A) protocol for coordination are often analyzed in isolation. This creates a significant ‘semantic gap,’ making it difficult to rigorously analyze crucial system properties like safety, security, and functionality. This fragmentation can lead to risks such as architectural misalignments, where different parts of the system don’t understand each other correctly, and exploitable coordination issues, like agents getting stuck in endless loops or malicious agents gaining unauthorized access.
To address these challenges, researchers Edoardo Allegrini, Ananth Shreekumar, and Z. Berkay Celik have introduced a novel modeling framework for agentic AI systems. Their work, detailed in the paper Formalizing the Safety, Security, and Functional Properties of Agentic AI Systems, proposes two foundational models to bridge this semantic gap and enable rigorous analysis.
The Host Agent Model
The first model is the Host Agent (HA) model. This formalizes the top-level entity that acts as the user’s primary interface. The Host Agent is responsible for accepting user requests, breaking them down into smaller, manageable subtasks, and then orchestrating their execution by leveraging external agents (via A2A) and tools (via MCP). It acts as both a conductor and a monitor, ensuring that tasks are delegated safely and that the system’s state remains consistent throughout the task’s journey.
The Task Lifecycle Model
Complementing the Host Agent model is the Task Lifecycle model. This model provides a detailed view of how individual subtasks progress from their creation to completion or failure. It outlines the various states a subtask can be in (e.g., CREATED, AWAITING DEPENDENCY, READY, IN PROGRESS, COMPLETED, FAILED, ERROR) and the transitions between these states. This fine-grained perspective is crucial for managing dependencies between subtasks and handling errors effectively.
Together, these two models offer a unified semantic framework. This means they provide a common language and structure for understanding and reasoning about the complex behavior of multi-AI agent systems. This unified view is essential for uncovering coordination issues, verifying system properties, and preventing problems like deadlocks and security vulnerabilities before they arise in real-world deployments.
Also Read:
- Ensuring Robotic Safety: A Multi-Level Approach for LLM-Powered Agents
- The Gatekeeper Protocol: A New Framework for Reliable and Efficient AI Agents
Formal Properties for System Assurance
Grounded in this framework, the researchers define 31 formal properties for both the Host Agent and the Task Lifecycle, categorized into liveness, safety, completeness, and fairness. These properties are expressed using temporal logic, a powerful tool for precisely defining how a system should behave over time. For example:
- Liveness properties ensure that the system eventually makes progress towards a goal, preventing deadlocks. An example is ensuring every user prompt eventually receives a final response.
- Safety properties guarantee that the system never enters undesirable or harmful states. For instance, a transaction agent should not execute an investment before the planning agent has successfully calculated the risk.
- Completeness properties ensure that if a solution exists, the system will find it, avoiding unfulfilled tasks due to suboptimal coordination.
- Fairness properties ensure that all delegated subtasks eventually reach a completed or error state, preventing starvation.
The paper also presents a case study demonstrating how these models can be used to verify architectural controls against adversarial behaviors. By encoding security constraints as temporal logic invariants at different architectural layers (Host Agent Core, Registry, Orchestrator, Communication Layer), the framework helps detect and mitigate threats like prompt injection, unauthorized access, and privilege escalation.
This work represents a significant step towards a rigorously grounded, domain-agnostic framework for the systematic analysis, design, and deployment of correct, reliable, and robust agentic AI systems, ensuring their safe and secure operation in high-stakes applications.
