Formalizing the Safety, Security, and Functional Properties of Agentic AI Systems
Open accessAbstract
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 central models: (1) 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; (2) 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 16 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 analysis, design, and deployment of correct, reliable, and robust agentic AI systems.
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Integrity signals
Registry
Cites
Statistics
Claims the paper makes
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
Allegrini et al. formalize 31 temporal logic properties for agentic AI safety on single-host systems, the most comprehensive formal property set prior to this work, but without addressing multi-agent delegation chains or composition.
“Allegrini et al. [27] formalize 31 temporal logic properties for agentic AI safety on singlehost systems-the most comprehensive formal property set prior to this work-but without addressing multi-agent delegation chains or composition.”
From SentinelAgent: Intent-Verified Delegation Chains for Securing Federal Multi-Agent AI Systems (2026) · cites this paper as [27]
The Abstract and §8 (Conclusion; page unavailable) state that the paper defines 16 host-agent and 14 task-lifecycle properties—30, not 31. The Introduction and §3 explicitly address multi-agent coordination, cross-protocol composition, and delegation-chain failures, contrary to the claim that these topics are not addressed. Our copy does not establish the comparative assertion that this was the most comprehensive property set. (LLM, conf=0.90)
Checked by a reasoning model — may be wrong.
Experimental — accuracy not yet measured
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
The self-check needs the paper’s full text.
Cites
No references could be resolved yet.
Research works printed but not linked: 33
- Christian Schroeder de Witt. Open challenges in multi-agent security: Towards secure systems of interacting ai agents. arXiv preprint arXiv:2505.02077, 2025. · arXiv
- Ali Dorri, Salil S. Kanhere, and Raja Jurdak. Multi-agent systems: A survey. IEEE Access, 2018.
- Zane Durante, Qiuyuan Huang, Naoki Wake, Ran Gong, Jae Sung Park, Bidipta Sarkar, Rohan Taori, Yusuke Noda, Demetri Terzopoulos, Yejin Choi, Katsushi Ikeuchi, Hoi Vo, Li Fei-Fei, and Jianfeng Gao. Agent ai: Surveying the horizons of multimodal interaction. arXiv preprint arXiv:2401.03568, 2024. · arXiv
- Kai Greshake, Sahar Abdelnabi, Shailesh Mishra, Christoph Endres, Thorsten Holz, and Mario Fritz. Not what you've signed up for: Compromising real-world LLM-integrated applications with indirect prompt injection. In ACM Workshop on Artificial Intelligence and Security, 2023.
- Taicheng Guo, Xiuying Chen, Yaqi Wang, Ruidi Chang, Shichao Pei, Nitesh V. Chawla, Olaf Wiest, and Xiangliang Zhang. Large language model based multi-agents: A survey of progress and challenges. In International Joint Conference on Artificial Intelligence, 2024.
- Idan Habler, Ken Huang, Vineeth Sai Narajala, and Prashant Kulkarni. Building a secure agentic ai application leveraging a2a protocol. arXiv preprint arXiv:2504.16902, 2025. · arXiv
- Lewis Hammond, Alan Chan, Jesse Clifton, Jason Hoelscher-Obermaier, Akbir Khan, Euan McLean, Chandler Smith, Wolfram Barfuss, Jakob Foerster, Tomáš Gavenčiak, The Anh Han, Edward Hughes, Vojtěch Kovařík, Jan Kulveit, Joel Z. Leibo, Caspar Oesterheld, Chris- tian Schroeder de Witt, Nisarg Shah, Michael Wellman, Paolo Bova, Theodor Cimpeanu, Carson Ezell, Quentin Feuillade-Montixi, Matija Franklin, Esben Kran, Igor Krawczuk, Max Lamparth, Niklas Lauffer, Alexander Meinke, Sumeet Motwani, Anka Reuel, Vincent Conitzer, Michael Dennis, Iason Gabriel, Adam Gleave, Gillian Hadfield, Nika Haghtalab, Atoosa Kasirzadeh, Sébastien Krier, Kate Larson, Joel Lehman, David C. Parkes, Georgios Piliouras, and Iyad Rah- wan. Multi-agent risks from advanced ai. arXiv preprint arXiv:2502.14143, 2025. · arXiv
- Shanshan Han, Qifan Zhang, Yuhang Yao, Weizhao Jin, and Zhaozhuo Xu. LLM multi-agent sys- tems: Challenges and open problems. arXiv preprint arXiv:2402.03578, 2025. · arXiv
- Pengfei He, Yuping Lin, Shen Dong, Han Xu, Yue Xing, and Hui Liu. Red-teaming LLM multi- agent systems via communication attacks. In Findings of the Association for Computational Linguistics, 2025.
- Xinyi Hou, Yanjie Zhao, Shenao Wang, and Haoyu Wang. Model context protocol (mcp): Land- scape, security threats, and future research directions. ACM Trans. Softw. Eng. Methodol., 2026.
- Jen-tse Huang, Jiaxu Zhou, Tailin Jin, Xuhui Zhou, Zixi Chen, Wenxuan Wang, Youliang Yuan, Maarten Sap, and Michael Lyu. On the resilience of LLM-based multi-agent collaboration with faulty agents. In International Conference on Machine Learning, 2025.
- Erik Jones, Anca Dragan, and Jacob Steinhardt. Adversaries can misuse combinations of safe mod- els. In International Conference on Machine Learning, 2025.
- Donghyun Lee and Mo Tiwari. Prompt infection: LLM-to-LLM prompt injection within multi-agent systems. arXiv preprint arXiv:2410.07283, 2025. · arXiv
- Guohao Li, Hasan Abed Al Kader Hammoud, Hani Itani, Dmitrii Khizbullin, and Bernard Ghanem. Camel: communicative agents for "mind" exploration of large language model society. In Inter- national Conference on Neural Information Processing Systems, 2023.
- Qiaomu Li and Ying Xie. From glue-code to protocols: A critical analysis of a2a and mcp integration for scalable agent systems. arXiv preprint arXiv:2505.03864, 2025. · arXiv
- Zhihao Li, Kun Li, Boyang Ma, Minghui Xu, Yue Zhang, and Xiuzhen Cheng. We urgently need privilege management in MCP: A measurement of API usage in MCP ecosystems. In 22nd IEEE International Conference on Mobile Ad-Hoc and Smart Systems, MASS 2025, Chicago, IL, USA, October 6-8, 2025, 2025.
- Yi Liu, Gelei Deng, Yuekang Li, Kailong Wang, Zihao Wang, Xiaofeng Wang, Tianwei Zhang, Yepang Liu, Haoyu Wang, Yan Zheng, and Yang Liu. Prompt injection attack against LLM- integrated applications. arXiv preprint arXiv:2306.05499, 2024a. · arXiv
- Yupei Liu, Yuqi Jia, Runpeng Geng, Jinyuan Jia, and Neil Zhenqiang Gong. Formalizing and bench- marking prompt injection attacks and defenses. In USENIX Security Symposium, 2024b.
- Sumeet Ramesh Motwani, Mikhail Baranchuk, Martin Strohmeier, Vijay Bolina, Philip Torr, Lewis Hammond, and Christian Schroeder de Witt. Secret collusion among AI agents: Multi-agent deception via steganography. In Neural Information Processing Systems, 2024.
- Nathalia Nascimento, Paulo Alencar, and Donald Cowan. Self-adaptive large language model (LLM)-based multiagent systems. In IEEE International Conference on Autonomic Computing and Self-Organizing Systems Companion, 2023.
- Nils J. Nilsson. Artificial Intelligence: A New Synthesis. Morgan Kaufmann Publishers Inc., 1998. ISBN 9780080499451.
- Joon Sung Park, Joseph O'Brien, Carrie Jun Cai, Meredith Ringel Morris, Percy Liang, and Michael S. Bernstein. Generative agents: Interactive simulacra of human behavior. In ACM Symposium on User Interface Software and Technology, 2023.
- Pierre Peigné, Mikolaj Kniejski, Filip Sondej, Matthieu David, Jason Hoelscher-Obermaier, Chris- tian Schroeder de Witt, and Esben Kran. Multi-agent security tax: Trading off security and collaboration capabilities in multi-agent systems. In AAAI Conference on Artificial Intelligence, 2025.
- Brandon Radosevich and John Halloran. Mcp safety audit: LLMs with the model context protocol allow major security exploits. arXiv preprint arXiv:2504.03767, 2025. · arXiv
- Stuart Russell and Peter Norvig. Artificial Intelligence: A Modern Approach. Prentice Hall Press, 2009. ISBN 0136042597.
- Yu Tian, Xiao Yang, Jingyuan Zhang, Yinpeng Dong, and Hang Su. Evil geniuses: Delving into the safety of LLM-based agents. arXiv preprint arXiv:2311.11855, 2024. · arXiv
- Alexander Wei, Nika Haghtalab, and Jacob Steinhardt. Jailbroken: How does LLM safety training fail? In Neural Information Processing Systems, 2023.
- Yizhe Xie, Congcong Zhu, Xinyue Zhang, Minghao Wang, Chi Liu, Minglu Zhu, and Tianqing Zhu. Who's the mole? modeling and detecting intention-hiding malicious agents in LLM-based multi-agent systems. arXiv preprint arXiv:2507.04724, 2025. · arXiv
- Yixuan Yang, Daoyuan Wu, and Yufan Chen. Mcpsecbench: A systematic security benchmark and playground for testing model context protocols. arXiv preprint arXiv:2508.13220, 2025. · arXiv
- Shunyu Yao, Dian Yu, Jeffrey Zhao, Izhak Shafran, Thomas L. Griffiths, Yuan Cao, and Karthik Narasimhan. Tree of thoughts: deliberate problem solving with large language models. In Inter- national Conference on Neural Information Processing Systems, 2023.
- Junjie Ye, Sixian Li, Guanyu Li, Caishuang Huang, Songyang Gao, Yilong Wu, Qi Zhang, Tao Gui, and Xuanjing Huang. ToolSword: Unveiling safety issues of large language models in tool learning across three stages. In Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), 2024.
- Dan Zhang, Gang Feng, Yang Shi, and Dipti Srinivasan. Physical safety and cyber security analysis of multi-agent systems: A survey of recent advances. IEEE/CAA Journal of Automatica Sinica, 2021.
- Hongxin Zhang, Weihua Du, Jiaming Shan, Qinhong Zhou, Yilun Du, Joshua B. Tenenbaum, Tian- min Shu, and Chuang Gan. Building cooperative embodied agents modularly with large language models. In International Conference on Learning Representations, 2024.
Cited by
Sorted by citations
- Authors
- Allegrini, E., Shreekumar, A., & Celik, Z. B.
- Affiliations
- Sapienza University of Rome (IT)
- Purdue University West Lafayette (US)
- Venue
- arXiv
- Publisher
- arXiv
- Published
- 2025
- ISSN
- 2331-8422 (ISSN-L)
- arXiv
- 2510.14133
- OpenAlex
- W7092291249
- Cited by
- 0
- References
- 0
- Type
- posted content
- Language
- en
- Open access
- green
- arxiv.org
- Locations
- arXiv (Cornell University) (submittedVersion)
- IRIS Research product catalog (Sapienza University of Rome) (submittedVersion)
- arXiv (Cornell University)
- Funders
- National Science Foundation (2229876)
- U.S. Department of Homeland Security
- Topics
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
- Physical Sciences › Computer Science › Artificial Intelligence › Multi-Agent Systems and Negotiation
- Physical Sciences › Computer Science › Artificial Intelligence › Logic, Reasoning, and Knowledge
- Keywords
- agentic AI systems, multi-agent systems, large language models, formal verification, temporal logic, Model Context Protocol, safety properties, liveness properties, fairness properties, deadlock detection, security vulnerabilities, agent coordination
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
