PaxLabs Research
Andres G. and the PaxLabs Research Team · PaxLabs Inc.
Tool Grounding and the Postcondition Problem: Verifiable Execution in Agentic Systems
Andres G. and the PaxLabs Research Team PaxLabs Inc. Correspondence: legal@paxeer.app
Agentic systems that invoke external tools face a fundamental verification gap. When a large language model (LLM) selects a tool, constructs parameters, and receives a return value, it has no systematic mechanism to confirm that the intended postcondition actually holds in the external environment. We formalize this as the Postcondition Problem and show that current tool-use architectures rely on implicit trust in return values, a reliance that produces silent failures, false successes, and compounding errors in multi-step agent trajectories. We propose receipt-based verification as a structural remedy: every tool invocation produces an inspectable receipt object that encodes what the tool actually did, which the agent can then compare against expected postconditions. We present a taxonomy of tool grounding failures, define an evaluation protocol for measuring tool grounding reliability, and discuss design implications for typed tool schemas, postcondition specifications, and receipt-first architectures. Our framework does not eliminate tool failures, but it makes them visible, auditable, and recoverable, properties that are necessary for deploying agentic systems in high-stakes environments.
tool use, large language models, agents, verification, postconditions, grounding, receipt-based execution, formal methods, agentic systems
Large language models have increasingly become orchestrators of external action. Systems such as AutoGPT [1], Toolformer [2], and various API-calling frameworks now delegate subtasks to tools that interact with file systems, databases, web services, and physical devices. This transition from text generation to tool-mediated action introduces a class of problems that do not arise in purely generative settings: the model proposes an action, a tool executes it, and the model receives a return value, but the model has no principled way to verify that the action produced its intended effect.
Consider a simple example. An agent is instructed to create a new user account in a database. It calls a tool with the appropriate parameters and receives a success response. The agent proceeds as though the account exists. But the tool may have silently failed: the database could have rejected the write due to a constraint violation that the tool's wrapper swallowed, the connection could have timed out with a cached success response, or the tool could have written to a staging database rather than the production one. The agent's belief state (the account exists) diverges from reality (the account does not exist), and this divergence compounds as the agent takes further actions that depend on the false belief.
We call this the Postcondition Problem. Formally: given an agent that proposes action A with intended postcondition P, and a tool that executes A and returns result R, how does the agent verify that P actually holds? Current systems treat R as sufficient evidence for P. We argue that this conflation is the root cause of a broad class of agent failures and that it requires a structural solution.
Our contributions are as follows:
1. We formalize the Postcondition Problem and distinguish it from related issues such as tool selection errors and parameter construction failures.
2. We introduce receipt-based verification as a design pattern in which every tool call produces an inspectable receipt object that can be matched against expected postconditions.
3. We present a taxonomy of five categories of tool grounding failures, each requiring different detection and recovery strategies.
4. We define an evaluation protocol for measuring tool grounding reliability in agentic systems.
5. We discuss design implications for tool schema specification, postcondition typing, and receipt-first architectures.
Claims Not Made. We do not claim that receipt-based verification eliminates tool failures. We do not claim that LLMs can reliably generate correct postcondition specifications without supervision. We do not claim to solve the general problem of verifying arbitrary side effects in distributed systems. Our scope is narrower: we identify a structural gap in current tool-use architectures and propose a mechanism that makes failures visible and recoverable rather than silent and compounding.
The integration of external tools into LLM-based systems has progressed rapidly. Toolformer [2] demonstrated that language models can learn to invoke APIs autonomously by training on augmented corpora where tool calls are interleaved with text. The model learns when a tool call is beneficial and generates both the call and its result as part of the text stream. Gorilla [3] extended this approach by training on a large corpus of API documentation, improving the model's ability to select and invoke real-world APIs correctly. ToolBench [4] provided a benchmark suite for evaluating tool-use capabilities across thousands of real APIs, revealing that even strong models frequently select wrong tools or construct malformed parameters.
More recent work has focused on agentic frameworks where tool use is embedded in a planning loop. ReAct [5] showed that interleaving reasoning traces with actions improves performance on complex tasks. Chain-of-thought prompting [6] provides the reasoning substrate, while tool calls provide the action substrate. Systems built on these patterns, including LangChain [7] and AutoGPT [1], compose multiple tool calls into multi-step trajectories where later steps depend on earlier results.
OpenAI's function calling interface [8] and similar mechanisms in other model providers [9] allow models to emit structured tool calls rather than free-text API invocations. These interfaces typically accept a JSON schema describing available functions and return a structured object containing the function name and arguments. The function is then executed externally, and the result is fed back to the model.
This architecture introduces a clear boundary between the agent (the model plus its planning logic) and the environment (the tools and the systems they interact with). The agent's only interface with the environment is the return value of each tool call. This boundary is where the Postcondition Problem arises: the return value is a message from the environment, but it is not the same as the postcondition itself.
The term grounding has been used in multiple senses. In linguistics, it refers to the relationship between words and their referents [10]. In robotics, it refers to connecting abstract plans to physical actions [11]. In this paper, we use tool grounding to mean the relationship between a tool call's intended effect and its actual effect in the environment. A tool call is grounded when the agent's belief about its effect matches what actually occurred. It is ungrounded when there is a divergence.
We now formalize the problem. Let A be an agentic system that interacts with an environment E through a set of tools T = {t_1, t_2, ..., t_n}. Each tool t_i accepts parameters p and produces a return value r. The agent maintains an internal state S that represents its beliefs about the environment.
Definition 1 (Tool Call). A tool call is a tuple c = (t, p, r) where t in T is a tool, p is a parameter vector, and r is the return value produced by executing t(p) in the environment E.
Definition 2 (Intended Postcondition). For a tool call c = (t, p, r), the intended postcondition P(c) is the proposition that the agent expects to hold in the environment after c is executed. P(c) is part of the agent's internal representation and is not directly observable.
Definition 3 (Actual Postcondition). For a tool call c = (t, p, r), the actual postcondition Q(c) is the proposition that actually holds in the environment after c is executed. Q(c) is a property of the world, not of the agent's beliefs.
The Postcondition Problem: Given a tool call c = (t, p, r), how does the agent determine whether P(c) = Q(c), that is, whether the intended postcondition matches the actual postcondition?
In current systems, the agent uses r as a proxy for Q(c). If r indicates success, the agent assumes P(c) holds. This assumption is encoded in the agent's state update:
S' = Update(S, P(c)) if r indicates success S' = S if r indicates failure
The problem is that r may not be a reliable indicator of Q(c). There are several modes of divergence:
(1) r indicates success, but Q(c) does not hold (false success). (2) r indicates failure, but Q(c) does hold (false failure). (3) Q(c) partially holds, but r does not indicate the extent of partial success. (4) Q(c) holds in a different sense than P(c) (semantic mismatch).
Mode (1) is the most dangerous because the agent proceeds on a false belief that compounds across subsequent actions. Mode (3) is common in systems where tools interact with partially-available services or eventually-consistent stores.
Proposition 1. In a multi-step agent trajectory where each step depends on the postcondition of the previous step, a single false success can cause the entire trajectory to produce an incorrect final result, even if all subsequent tool calls execute correctly.
Proof sketch. Let c_1, c_2, ..., c_k be a sequence of tool calls where P(c_{i+1}) depends on Q(c_i). If r_1 indicates success but Q(c_1) does not hold, then the agent's state S_1' encodes P(c_1) as true. The agent constructs c_2 under the assumption that P(c_1) holds. Even if c_2 executes correctly with respect to its parameters, those parameters were constructed under a false premise, so Q(c_2) may not satisfy the intended goal. The error propagates forward without bound.
The most insidious class of tool grounding failures are those in which the tool returns a success signal but did not actually produce the intended effect. We call these silent failures because, from the agent's perspective, nothing went wrong.
1) Wrapper Swallowing. When tools are wrapped in middleware (error handlers, retry logic, logging layers), exceptions from the underlying system may be caught and replaced with default success responses. This is a common pattern in production API wrappers where the goal is to prevent crashes, but it has the side effect of hiding failures from the caller.
2) Partial Execution. Some tools perform multi-step operations internally. A file copy operation, for example, may read the source file, create the destination file, write the contents, and set permissions. If the write succeeds but the permission set fails, the tool may report success because the primary operation (copy) completed, even though the file is not accessible in the intended way.
3) Stale State. Tools that interact with eventually-consistent systems may return success based on a write acknowledgment from one node, while the data has not yet propagated to other nodes. The agent reads the success signal and proceeds, but a subsequent read from a different node may not find the data.
4) Semantic Mismatch. The tool's definition of success may differ from the agent's definition. A database tool may consider an INSERT successful if the query executes without error, even if the inserted row violates an application-level constraint that the database does not enforce. The tool's postcondition (query executed) diverges from the agent's postcondition (data is correctly stored and accessible).
Silent failures are dangerous individually but catastrophic in sequence. Consider an agent that must: (1) create a database record, (2) generate a file referencing that record, (3) upload the file to a storage service, and (4) send a notification containing a link to the uploaded file. If step (1) silently fails, the agent proceeds to step (2) with a non-existent record ID. Step (2) may succeed (creating a file with an invalid reference), step (3) may succeed (uploading the file), and step (4) may succeed (sending the notification). The agent reports success. The user receives a notification with a link to a file that references a non-existent record. Every step after the silent failure is wasted work, and the final state is inconsistent.
This compounding effect is analogous to the cascade failure pattern in distributed systems [12], but with an important difference: in distributed systems, cascade failures typically produce error signals that propagate backward through the dependency chain. In agentic systems, the failure is silent, so there is no error signal to propagate. The agent's belief state diverges from reality and never self-corrects.
We propose receipt-based verification as a structural mechanism for closing the verification gap. The core idea is simple: every tool call produces not just a return value but a receipt object that encodes what the tool actually did, which the agent (or an auditor) can inspect, compare against expected postconditions, and use to detect failures.
Definition 4 (Receipt). A receipt for a tool call c = (t, p, r) is a structured object R(c) that includes: - r_id: a unique identifier for the call - t_id: the tool identifier - p: the parameters that were actually passed (which may differ from those constructed by the agent due to middleware transformation) - r: the raw return value - effects: a structured description of the effects the tool actually produced - timestamp: when the call was executed - environment: identifying information about the execution context (version, endpoint, region, etc.) - preconditions_checked: which preconditions the tool verified before execution - partial: a boolean indicating whether execution was partial
Definition 5 (Postcondition Specification). A postcondition specification S(P) for an intended postcondition P is a predicate over receipt objects: S(P)(R) returns true if the receipt R is consistent with P holding.
Definition 6 (Receipt Verification). Given a tool call c with intended postcondition P and receipt R(c), the verification step computes:
verified = S(P)(R(c))
If verified is true, the agent updates its state to include P. If verified is false, the agent enters a recovery path (retry, alternative tool, human escalation).
We define the receipt-based verification protocol as follows:
Protocol 1 (Receipt-Verified Tool Call).
Step 1: The agent constructs intended postcondition P for the planned tool call. Step 2: The agent constructs postcondition specification S(P). Step 3: The agent invokes tool t with parameters p. Step 4: The tool executes and produces return value r and receipt R. Step 5: The agent evaluates S(P)(R). Step 6: If verified, update state. If not, invoke recovery procedure.
The overhead of this protocol is one additional postcondition evaluation per tool call. The cost of the evaluation depends on the complexity of S(P), but for many common tool operations (create, update, delete, read), S(P) can be expressed as a simple predicate over the receipt's effects field.
We identify three design principles for effective receipts:
Principle 1 (Completeness). The receipt must encode all effects of the tool call, not just the primary effect. A database INSERT receipt should include the table, the generated ID, the row data, and any triggers that fired, not just a success flag.
Principle 2 (Fidelity). The receipt must reflect what actually happened, not what was intended. If a tool was asked to write to table A but actually wrote to table B due to an alias resolution, the receipt should record table B.
Principle 3 (Immutability). Once produced, a receipt should not be modifiable. This ensures that receipts can serve as audit records and that postcondition verification is based on ground truth rather than a mutable artifact.
Theorem 1 (Detection Soundness). If the postcondition specification S(P) is correct and the receipt R is faithful, then S(P)(R) = true implies P holds with high probability.
Proof sketch. If S(P) correctly characterizes the set of receipts consistent with P, and R faithfully encodes the actual effects of the tool call, then a positive verification implies the actual effects are consistent with P. The "high probability" qualification accounts for the possibility that the receipt captures the tool's reported effects but not the full state of the environment (e.g., a concurrent modification between the tool call and the verification).
Theorem 2 (Detection Completeness). If P does not hold and the receipt R faithfully encodes the actual effects, then S(P)(R) = false, provided S(P) is correct.
This means that receipt-based verification does not produce false negatives when the receipt is faithful and the specification is correct. In practice, both conditions may be violated, which we address in the Limitations section.
We organize tool grounding failures into five categories based on where in the call chain the failure occurs.
Category 1: Wrong Tool Selection. The agent selects a tool t_i when tool t_j was appropriate. This is a planning failure that occurs before execution. Receipt verification cannot detect this directly, but postcondition verification can: if the agent specifies P(c) and the receipt shows that t_i's effects are inconsistent with P(c), the mismatch is detected.
Category 2: Wrong Parameter Construction. The agent selects the correct tool but constructs incorrect parameters. This may be due to hallucinated field names, wrong data types, or incorrect values. Typed tool schemas (see Section VIII) can prevent some of these errors, and receipt verification can detect others by comparing the actual parameters recorded in the receipt against the intended parameters.
Category 3: Silent Partial Failure. The tool executes but only partially completes its intended operation. The receipt's partial field and effects description allow the agent to detect that the intended postcondition only partially holds and to decide whether to retry, accept the partial result, or escalate.
Category 4: Success Signal Without Effect. The tool returns a success code but did not produce the intended effect. This is the classic silent failure. Receipt verification detects this when the effects field does not contain evidence of the intended postcondition.
Category 5: Effect Without Verification. The tool produces the intended effect, but the agent does not verify it. This is not a tool failure but an agent architecture failure: the system lacks a verification step. In current tool-use frameworks, this is the default behavior. Receipt-based verification is specifically designed to address this category by making verification a structural part of the tool-call protocol.
Table I summarizes the taxonomy:
Category | Failure Point | Receipt Detectable | Recovery Strategy ---------|---------------------|--------------------|-------------------------- 1 | Tool selection | Yes (via effects) | Re-plan with feedback 2 | Parameter construction| Yes (via params) | Correct and retry 3 | Partial execution | Yes (via partial) | Retry or accept partial 4 | Silent failure | Yes (via effects) | Retry or escalate 5 | No verification step | N/A (structural) | Add verification to arch
Measuring tool grounding reliability requires a protocol that goes beyond simple success/failure rates. We propose a multi-dimensional evaluation framework.
Metric 1 (Grounding Accuracy). The fraction of tool calls where the agent's belief about the postcondition matches the actual postcondition. This requires ground truth about the actual state of the environment, which can be obtained through independent state probes.
Metric 2 (Silent Failure Rate). The fraction of tool calls where the return value indicates success but the postcondition does not hold. This is a subset of grounding inaccuracy but is singled out because it is the most dangerous failure mode.
Metric 3 (Receipt Verification Precision). The fraction of receipt verifications that correctly identify whether the postcondition holds. This measures the quality of the postcondition specifications.
Metric 4 (Receipt Verification Recall). The fraction of actual postcondition failures that are detected by receipt verification. High recall means few silent failures go undetected.
Metric 5 (Recovery Rate). The fraction of detected failures that are successfully recovered from through retry, re-planning, or escalation.
Protocol 2 (Tool Grounding Evaluation).
Step 1: Construct a benchmark of tasks requiring multi-step tool use, with known postconditions for each step. Step 2: Execute each task with the agent under evaluation. Step 3: After each tool call, probe the environment to determine the actual postcondition (ground truth). Step 4: Compare the agent's beliefs (from its state) against ground truth. Step 5: Compute Metrics 1-5. Step 6: Repeat with receipt-based verification enabled and compare.
The delta between the non-receipt and receipt-enabled runs measures the value of the verification mechanism. We expect the delta to be largest for Metric 2 (Silent Failure Rate), since that is the primary target of receipt-based verification.
A suitable benchmark should include:
- Simple tasks (single tool call with clear postcondition) - Compound tasks (multi-step, each step depending on previous postconditions) - Adversarial tasks (tools that sometimes return false success signals) - Partial tasks (tools that sometimes partially fail) - Cross-system tasks (tools that interact with multiple backends)
Each task should have a ground-truth specification that can be verified independently of the agent's execution. This is analogous to the test oracle problem in software testing [13], and the same techniques (reference implementations, property-based checks, independent re-execution) apply.