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. Building on prior work establishing the conceptual convergence of these paradigms, we present the first process calculus formalization of SGD and MCP, proving they are structurally bisimilar under a well-defined mapping Phi. However, we demonstrate that the reverse mapping Phi^{-1} is partial and lossy, revealing critical gaps in MCP's expressivity. Through bidirectional analysis, we identify five principles -- semantic completeness, explicit action boundaries, failure mode documentation, progressive disclosure compatibility, 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 isomorphic to SGD. Our work provides the first formal foundation for verified agent systems and establishes schema quality as a provable safety property.

翻译：大型语言模型智能体调用外部工具的能力涌现，催生了智能体协议形式化验证的迫切需求。该领域存在两种主导范式：面向零样本API泛化的研究框架Schema导向对话（SGD），以及智能体-工具集成的行业标准模型上下文协议（MCP）。尽管两者都通过模式描述实现动态服务发现，但其形式化关系尚未得到探索。在前人建立的概念趋同研究基础上，我们首次提出SGD和MCP的进程演算形式化，证明它们在定义良好的映射Phi下结构互模拟。然而，我们证明反向映射Phi^{-1}是部分且丢失信息的，揭示了MCP表达能力的重大缺陷。通过双向分析，我们识别出五个原则——语义完备性、显式动作边界、故障模式文档化、渐进式兼容性、工具间关系声明——作为完全行为等价的充要条件。我们将这些原则形式化为类型系统扩展MCP+，证明MCP+与SGD同构。本研究为可验证智能体系统奠定了首个形式化基础，并将模式质量确立为可证安全属性。