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.

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