Formal Semantics for Agentic Tool Protocols: A Process Calculus Approach

• URL: http://arxiv.org/abs/2603.24747v1
• Date: Wed, 25 Mar 2026 19:18:27 GMT
• Title: Formal Semantics for Agentic Tool Protocols: A Process Calculus Approach
• Abstract summary: Two paradigms dominate this space: theGuided Dialogue (SGD) and the Model Context Protocol (MCP)<n>We present the first process calculus formalization of SGD and MCP, proving they are structurally bisimilar under a well-defined mapping Phi.<n>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.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: 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.

Related papers

• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  Agentic systems driven by large language models (LLMs) are increasingly deployed in real-world where they act on persistent operational data.<n>Existing approaches do not provide such system-level guarantees.<n>We study here the verification of agentic systems comprising a single LLM and a tool orchestration harness over relational operational data.
  arXiv  Detail & Related papers  (2026-08-04T13:01:30Z)
• A Technical Taxonomy of LLM Agent Communication Protocols [60.76747983053368]
  This study develops a technical taxonomy to classify and analyze large language models (LLMs) agent communication protocols.<n>The framework guides protocol selection and highlights open research gaps such as privacy and policy enforcement.
  arXiv  Detail & Related papers  (2026-06-17T14:45:20Z)
• I-SAFE: Wasserstein Coherence Metrics for Structural Auditing of Scientific AI Models [5.562984399879219]
  We introduce the textscI-SAFE (Interventional Secure, Accurate, Fair and Explainable) framework for scientific AI models.<n>textscI-SAFE evaluates raw model outputs under structurally guided perturbations of the input.<n>We instantiate textscI-SAFE on drug--target interaction (DTI) prediction using the Davis kinase benchmark.
  arXiv  Detail & Related papers  (2026-05-20T20:44:30Z)
• Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications [1.0071849243353403]
  We propose an agentic methodology that automatically extracts verification-ready properties from unstructured specifications.<n>We show that the pipeline generates syntactically and semantically aligned formal properties with a 77.8% accuracy.
  arXiv  Detail & Related papers  (2026-04-20T13:12:04Z)
• The Auton Agentic AI Framework [5.410458076724158]
  The field of Artificial Intelligence is undergoing a transition from Generative AI to Agentic AI.<n>This transition exposes a fundamental architectural mismatch: Large Language Models (LLMs) produce unstructured outputs, whereas the backend infrastructure they must control requires deterministic, schema-conformant inputs.<n>The present paper describes the Auton Agentic AI Framework, a principled architecture for the creation, creation, and governance of autonomous agent.
  arXiv  Detail & Related papers  (2026-02-27T06:42:08Z)
• The Convergence of Schema-Guided Dialogue Systems and the Model Context Protocol [0.0]
  This paper establishes a fundamental convergence: compatibility-Guided Dialogue (SGD) and the Model Context Protocol (MCP)<n>SGD and MCP represent two manifestations of a unified paradigm for deterministic, auditable LLM-agent interaction.
  arXiv  Detail & Related papers  (2026-02-21T09:02:35Z)
• Ontology-to-tools compilation for executable semantic constraint enforcement in LLM agents [0.0]
  We present a proof-of-principle mechanism for coupling large language models (LLMs) with formal domain knowledge semantics.<n>Ontological specifications are compiled into executable tool tools that LLM-based agents must use to create and modify knowledge graph instances.<n>We show how executable ontological semantics guide LLM interfaces and reduce manual schema and prompt engineering, establishing a general paradigm for embedding formal knowledge into generative systems.
  arXiv  Detail & Related papers  (2026-02-03T12:03:26Z)
• Alita-G: Self-Evolving Generative Agent for Agent Generation [54.49365835457433]
  We present ALITA-G, a framework that transforms a general-purpose agent into a domain expert.<n>In this framework, a generalist agent executes a curated suite of target-domain tasks.<n>It attains strong gains while reducing computation costs.
  arXiv  Detail & Related papers  (2025-10-27T17:59:14Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  Autoformalization addresses the scarcity of data for Automated Theorem Proving (ATP) by translating mathematical problems from natural language into formal statements.<n>Existing formalizer still struggles to consistently generate valid statements that meet syntactic validity and semantic consistency.<n>We propose the Autoformalizer with Tool Feedback (ATF), a novel approach that incorporates syntactic and consistency information as tools into the formalization process.
  arXiv  Detail & Related papers  (2025-10-08T10:25:12Z)
• PAT-Agent: Autoformalization for Model Checking [17.082027022913998]
  PAT-Agent is an end-to-end framework for natural language autoformalization and formal model repair.<n>It combines the generative capabilities of large language models with the rigor of formal verification.
  arXiv  Detail & Related papers  (2025-09-28T06:32:14Z)
• ProtoReasoning: Prototypes as the Foundation for Generalizable Reasoning in LLMs [54.154593699263074]
  ProtoReasoning is a framework that enhances the reasoning ability of Large Reasoning Models.<n>ProtoReasoning transforms problems into corresponding prototype representations.<n>ProtoReasoning achieves 4.7% improvement over baseline models on logical reasoning.
  arXiv  Detail & Related papers  (2025-06-18T07:44:09Z)
• Guiding the PLMs with Semantic Anchors as Intermediate Supervision: Towards Interpretable Semantic Parsing [57.11806632758607]
  We propose to incorporate the current pretrained language models with a hierarchical decoder network. By taking the first-principle structures as the semantic anchors, we propose two novel intermediate supervision tasks. We conduct intensive experiments on several semantic parsing benchmarks and demonstrate that our approach can consistently outperform the baselines.
  arXiv  Detail & Related papers  (2022-10-04T07:27:29Z)
• Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version) [67.99023219822564]
  We introduce the general framework of relational action bases (RABs) RABs generalize existing models by lifting both restrictions. We demonstrate the effectiveness of this approach on a benchmark of data-aware business processes.
  arXiv  Detail & Related papers  (2022-08-12T17:03:50Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.