Title: Establishing Formal Semantics for Agentic Tool Protocols via Process Calculus

Abstract: The rise of large language model agents that can trigger external tools has generated an immediate demand for the formal verification of agent protocols. Currently, two primary approaches define this domain: the Model Context Protocol (MCP), which serves as an industry benchmark for integrating agents with tools, and Schema-Guided Dialogue (SGD), a research-oriented framework designed for zero-shot API generalization. Although both methodologies facilitate dynamic service discovery by utilizing schema descriptions, their formal interconnections have not yet been investigated. Leveraging previous studies that highlighted the conceptual alignment of these two paradigms, this paper introduces the initial process calculus formalization of both SGD and MCP. We demonstrate that, when subjected to a clearly defined mapping denoted as $\Phi$, the two protocols are structurally bisimilar. Conversely, our analysis reveals that the inverse mapping, $\Phi^{-1}$, is both partial and lossy, thereby exposing significant limitations in the expressivity of MCP. By conducting a bidirectional analysis, we isolate five specific principles—semantic completeness, explicit action boundaries, failure mode documentation, progressive disclosure compatibility, and inter-tool relationship declaration—which are shown to be both necessary and sufficient to achieve full behavioral equivalence. We encode these principles as extensions to the type system, creating MCP+, and prove that MCP+ is isomorphic to SGD. This research lays the groundwork for a formal foundation for verified agent systems and defines schema quality as a safety property that can be formally proven.

Source: arXiv Generated at: 2026-06-04 00:00:00 UTC