ToolGate: Contract-Grounded and Verified Tool Execution for LLMs

TL;DR

ToolGate addresses the lack of formal guarantees in LLMs augmented with external tools by introducing a forward execution framework that maintains an explicit, typed symbolic world state $S$ within a state space $\Sigma$ and treats each tool as a Hoare-style contract $\{P_t\} t \{Q_t\}$. The system couples probabilistic reasoning with contract-based verification, using Top-$K$ retrieval and a weakest-precondition planning mechanism to ensure tool invocations are admissible and results are only committed when $A_t$ holds, thereby guaranteeing trajectory-level safety. Empirically, ToolGate delivers superior reliability and debuggability across ToolBench and MCP-Universe benchmarks, with model-agnostic improvements over strong baselines, and ablation studies confirming the critical role of pre/post-condition checks in pruning invalid paths and preventing error cascades. The framework advances trustworthy AI by providing a formal, verifiable foundation for tool use in LLMs, achieving robust multi-step reasoning while keeping state evolution transparent and auditable.

Abstract

Large Language Models (LLMs) augmented with external tools have demonstrated remarkable capabilities in complex reasoning tasks. However, existing frameworks rely heavily on natural language reasoning to determine when tools can be invoked and whether their results should be committed, lacking formal guarantees for logical safety and verifiability. We present \textbf{ToolGate}, a forward execution framework that provides logical safety guarantees and verifiable state evolution for LLM tool calling. ToolGate maintains an explicit symbolic state space as a typed key-value mapping representing trusted world information throughout the reasoning process. Each tool is formalized as a Hoare-style contract consisting of a precondition and a postcondition, where the precondition gates tool invocation by checking whether the current state satisfies the required conditions, and the postcondition determines whether the tool's result can be committed to update the state through runtime verification. Our approach guarantees that the symbolic state evolves only through verified tool executions, preventing invalid or hallucinated results from corrupting the world representation. Experimental validation demonstrates that ToolGate significantly improves the reliability and verifiability of tool-augmented LLM systems while maintaining competitive performance on complex multi-step reasoning tasks. This work establishes a foundation for building more trustworthy and debuggable AI systems that integrate language models with external tools.

Figures (2)

• Figure 1: ToolGate framework overview. The framework is built on Hoare Logic, formalizing the tool-calling process as a sequence of constrained logical reasoning steps, and continuously maintaining a trusted state $S$ to verify the conditions for tool invocation.
• Figure 2: Comparison of Average Tool-Calling Steps in Tool-Bench.