# Formal Semantics for Agentic Tool Protocols: A Process Calculus Approach

arXiv: https://arxiv.org/abs/2603.24747 · HTML: https://mlsanity.com/paper/2603.24747/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Tool learning and function calling, one of 16 directions in LLM agents and tool use.
- Builds on 19 of its 50 references that are in the map.
- First posted on arXiv 25 Mar 2026.

## Placed in

- LLM agents and tool use / [Tool learning and function calling](https://mlsanity.com/agents/tool-learning-and-function-calling/)

## Builds on (most cited first, 19 of 19)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Gorilla: Large Language Model Connected with Massive APIs](https://mlsanity.com/paper/2305.15334/) (2023)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Towards Scalable Multi-domain Conversational Agents: The Schema-Guided Dialogue Dataset](https://mlsanity.com/paper/1909.05855/) (2019)
- [Prompting Is Programming: A Query Language for Large Language Models](https://mlsanity.com/paper/2212.06094/) (2022)
- [Towards Zero-Shot Frame Semantic Parsing for Domain Scaling](https://mlsanity.com/paper/1707.02363/) (2017)
- [MCP-Zero: Active Tool Discovery for Autonomous LLM Agents](https://mlsanity.com/paper/2506.01056/) (2025)
- [MCPAgentBench: A Real-world Task Benchmark for Evaluating LLM Agent MCP Tool Use](https://mlsanity.com/paper/2512.24565/) (2025)
- [A Fast and Robust BERT-based Dialogue State Tracker for Schema-Guided Dialogue Dataset](https://mlsanity.com/paper/2008.12335/) (2020)
- [PARSE: LLM Driven Schema Optimization for Reliable Entity Extraction](https://mlsanity.com/paper/2510.08623/) (2025)
- [Formalizing the Safety, Security, and Functional Properties of Agentic AI Systems](https://mlsanity.com/paper/2510.14133/) (2025)
- [The LLMbda Calculus: AI Agents, Conversations, and Information Flow](https://mlsanity.com/paper/2602.20064/) (2026)
- [Tracking Capabilities for Safer Agents](https://mlsanity.com/paper/2603.00991/) (2026)
- [LLM-Based SQL Generation: Prompting, Self-Refinement, and Adaptive Weighted Majority Voting](https://mlsanity.com/paper/2601.17942/) (2026)

## Abstract (arXiv)

The emergence of large language model agents capable of invoking external tools has created urgent need for formal verification of agent protocols. Two paradigms dominate this space: Schema-Guided Dialogue (SGD), a research framework for zero-shot API generalization, and the Model Context Protocol (MCP), an industry standard for agent-tool integration. While both enable dynamic service discovery through schema descriptions, their formal relationship remains unexplored. We present the first process calculus formalization of SGD and MCP, proving they are structurally bisimilar under a well-defined mapping Phi. We demonstrate that the reverse mapping Phi-1 is partial and lossy, revealing critical gaps in MCP's expressivity. Through bidirectional analysis, we identify four principles - semantic completeness, explicit action boundaries, failure mode documentation, and inter-tool relationship declaration -- as necessary and sufficient conditions for full behavioral equivalence. We formalize these principles as type-system extensions MCP+, proving MCP+ is fully equivalent to SGD. Our work provides the first formal foundation for verified agent systems and establishes schema quality as a provable safety property. Practically, this means that the current MCP specification has expressiveness gaps compared to SGD and would benefit from the proposed extensions.