LEANGUARD: Lean-Verified Guardrails for Tool-Using Agents

1 Introduction

• Tool-using agents inconsistently follow domain policies, miss state dependencies, and can execute unsafe actions after untrusted tool outputs steer their reasoning.These failures matter when a successful call still makes a policy-forbidden state transition.Source: §1 · p. 1
• Figure 1 contrasts an unguarded agent billing an attacker’s gift card after injected instructions with LeanGuard denying the call until customer confirmation and an account card are present.The reissued call is then admitted.Source: Figure 1 · p. 1
• LeanGuard checks proposed calls at the tool boundary against Lean policies, with a decision procedure proved equivalent to an independent temporal semantics.A denied call can be corrected from model-facing feedback or by Lean metaprogramming that proves a nearby call admissible without the model.Source: §1 · p. 2
• At least 33 policy-forbidden calls were executed by unguarded Tau-Bench agents, while LeanGuard executed none; feedback did not significantly change task success.On DTap, LeanGuard reduced direct prompt-injection success from 57.9% to 5.9%.Source: §1 · p. 2
• Proof-guided repair proved admissible edits for 88 of 252 replayed Tau-Bench denials caused by argument values, with a median time of 2 ms.Feedback reduced repeated blocked calls and raised task success for four of five models over a bare denial.Source: §1 · p. 2

2.1 Overview

• LeanGuard is a Lean 4 policy runtime that checks proposed calls before dispatch and offers either model-guided feedback or proof-guided repair after denial.The model uses ordinary tool schemas and does not write Lean code, policies, proofs, or approval records.Source: §2.1 · p. 2, §2.2 · p. 2

2.2 Step 1: The Proposed Call and Its Evidence

• The adapter treats proposed calls as untrusted, validates arguments, and derives policy evidence from an authoritative backend snapshot with a revision tied to the relevant state.Dispatch outcomes are recorded, and user confirmation is trusted evidence bound to the exact proposal and state revision and usable once.Source: §2.2 · p. 2

2.3 Step 2: Lean Policies

• Policies combine PREVIOUS, ONCE, and SINCE over scoped history with permits, requirements, and forbids; unmet requirements and applicable forbids cannot be overridden by a permit.Temporal windows and scopes can restrict evaluation to events sharing a principal, conversation, or resource.Source: §2.3 · p. 3
• Evaluation denies actions when required data is missing or malformed, and its result is proved equivalent to an independent LeanLTL interpretation for every history.The proofs are checked when policies are built, and exported theorems depending on sorry or another nonstandard axiom are rejected.Source: §2.3 · pp. 3–4

2.4 The Admission Decision and Its Guarantee

• The admission theorem ensures that every allowed call satisfies the policy’s LeanLTL interpretation, and the runtime dispatches a call only after it is allowed.The guarantee assumes faithful observations and that every consequential call passes through the monitor; it is relative to the reviewed specification.Source: §2.4 · p. 4

2.5 Step 3a: Feedback-Guided Recovery

• Feedback returns failed-rule identifiers, obligations, errors, supporting evidence, and a natural-language hint, while leaving the model to fix the call.The hint renders the failed obligation but is not itself verified.Source: §2.5 · p. 4

2.6 Step 3b: Proof-Guided Repair

• Lean searches finite candidate edits that preserve user intent and returns a repair only with a kernel-checked proof that the policy admits it.The search uses a Lean tactic and can be extended with registered facts or custom tactics; failure to find an edit in the candidate set does not prove none exists, and repairs are evaluated on replayed denials.Source: §2.6 · p. 4

2.7 Instantiation on τ 2-bench and DTap

• The evaluation formalizes reviewed, tool-enforceable τ 2-bench policies and instantiates DTap contracts under a read-only deployment; task completion and policy compliance are measured separately.The τ 2-bench policies cover retail, airline, and telecom; DTap uses reviewed contracts for 199 tools across seven domains, with no write grants, reviews, or confirmations.Source: §2.7 · pp. 4–5

3 Results

• The evaluation used five Qwen models across up to three arms; formal violations were replay-verifiable policy denials, while judge-flagged episodes captured broader but approximate compliance judgments.The judge could overlook trusted runtime evidence and graded its own episodes.Source: §3 · p. 5

RQ1: What Goes Wrong

• On τ 2-bench, stopped calls most often involved authorization failures (572), followed by invalid invocations (551); temporal incompatibilities numbered 411 and prohibitions 313.On DTap, stopped attack calls were mostly authorization failures (60%) and invalid invocations (58%); 13% used tools whose effects LEANGUARD could not model.Source: RQ1: What Goes Wrong · p. 6, Figure 3 · p. 6

RQ2: Does Enforcement Work, and at What Cost?

• On τ 2-bench, LEANGUARD executed none of the calls it denied, while task success with feedback was 70.9% versus 72.7% unguarded (p = 0.21).A bare denial yielded 68.9% task success (p = 0.007).Source: RQ2: Does Enforcement Work, and at… · p. 6, Table 1 · p. 6
• On DTap, LEANGUARD reduced direct prompt-injection success from 57.9% to 5.9% and indirect success from 22.3% to 3.8%.In telecom, benign success was unchanged (75.1% vs. 75.3%); across domains, read-only deployment reduced benign success from 53.1% to 12.5%.Source: Table 1 · p. 6, RQ2: Does Enforcement Work, and at… · p. 7
• Tool-call enforcement leaves response-text attacks outside its coverage: these still succeeded in 30.2% of guarded customer-service and travel episodes and 21.4–37.0% of five medical attack categories.Response-only harms include diagnosis manipulation and ignoring allergies.Source: RQ2: Does Enforcement Work, and at… · p. 7

RQ3: Can the Model Recover from a Denial?

• With feedback, blocked calls fell from 983 to 719 across models, recoveries rose from 34 to 48 (5.5% to 9.1% of denied actions; p = 0.02), and task success rose for four of five models versus bare denial.Overall task success was 70.9% with feedback versus 68.9% with bare denial (p = 0.13).Source: RQ3: Can the Model Recover from a… · p. 7

RQ4: Can Lean Repair a Denied Call?

• For argument-value denials, Lean proved an admissible edit for 88 of 252 cases (34.9%), with a median repair time of 2 ms.The search ran after the episodes, so agents did not receive these repairs; when agents later issued them, 16 of 22 tasks succeeded, versus 7 of the other 66.Source: RQ4: Can Lean Repair a Denied Call? · p. 7

• Prior safeguards include learned guard models such as GuardAgent and AGrail, as well as formal runtime enforcement through symbolic constraints, policy languages, capabilities, and reference monitors.The formal approaches extend runtime shielding, which can block or repair actions that violate a safety specification.Source: §4 · pp. 7–8
• ToolSafe is the closest prior work to LEANGUARD’s recovery setting because it checks tool invocations and returns feedback for later agent reasoning (Mou et al., 2026).LEANGUARD proves admission correct against temporal-logic semantics and searches for an admissible edit of the agent’s own call.Source: §4 · p. 8
• Recent Lean-based work checks financial-agent actions or formalizes workflows and trajectories, while LEANGUARD returns violated rules and supports proof-backed call repair (Rashie and Rashi, 2026; Wang et al., 2026b).Source: §4 · p. 8
• Benchmarks cover stateful tool use, simulated users, explicit policies, prompt injection, and broader safety risks; this paper additionally measures model and Lean recovery after denial.Source: §4 · p. 8

• LEANGUARD blocks policy-denied calls on τ 2-bench, feedback helps agents recover, and offline Lean search computes and proves admissible fixes without the model.Harm carried by response text remains beyond its enforcement scope.Source: §5 · p. 8

Limitations

• The guarantee covers only the tool-enforceable formalization of each natural-language policy, and proofs do not catch errors or omissions in that formalization.The policies were drafted with an LLM-based authoring aid and corrected by hand.Source: Limitations · p. 9
• The guarantee assumes faithful adapter reports and that every consequential tool call passes through the monitor; free-form dialogue to consent records is outside its scope.Source: Limitations · p. 9
• Tool-call monitoring does not cover harm carried by response text, and read-only DTap overstates protection relative to policies that permit benign writes.Source: Limitations · p. 9
• Proof-guided repair was tested only offline on replayed denials, so its effect when delivered to an agent remains unmeasured; experiments also use one model family, English tasks, and simulated users.Source: Limitations · p. 9

A Runtime Protocol

• A dispatch reservation is recorded before tool invocation, so single-use operations become unavailable while in flight and unknown outcomes are not retried automatically.Unknown outcomes retain any consumed quota.Source: A Runtime Protocol · p. 11
• Snapshots carry a revision and backend-state digest, while facts recorded at dispatch cannot be replaced by later tool output; text in tool outputs is not evidence.Source: A Runtime Protocol · p. 11
• Confirmation is bound to the proposed action, arguments, resource, state revision, and user-visible details, and is valid only while unrevoked and unconsumed.The experiments use a separate model call to simulate the trusted confirmation screen, whose errors can produce incorrect consent evidence.Source: A Runtime Protocol · p. 11

B Semantics of the Policy Language

• History is represented newest-event-first, with trace steps moving toward the past; temporal windows anchor at the current event and scope projection re-anchors there.Each trace state retains the remaining history, and an empty final state makes the embedding total.Source: B Semantics of the Policy Language · p. 11
• The evaluator returns true exactly when the LeanLTL trace satisfies the formula, and the equivalence extends to authorization and fail-closed admission.Metric windows and scope projections extend LeanLTL’s trace sets beyond plain finite-trace LTL; exported theorems are checked for prohibited axioms and sorry.Source: B Semantics of the Policy Language · p. 12, Table 3 · p. 12

C Additional Related Work

• Related work verifies model reasoning, formal artifacts, clinical reports, and unsafe inputs; LeanGuard instead checks whether a tool call is admissible under policy, trusted state, and history.Source: C Additional Related Work · p. 12

D Policies

• Each τ 2-bench policy has a permit, a schema rule, and requirements, with no forbid; retail requirements include ownership, order state, confirmation, and payment rules.Table 4 gives the policy sizes, and its scope excludes the customer’s telecom device tools.Source: D Policies · p. 12, Table 4 · p. 12
• DTap’s eight-rule template requires contracted tools, exact grants for resolved effects, valid contracts, state-bound single-use confirmation for sensitive effects, prior observation where designated, resolved earlier dispatches, and a dispatch budget.Source: D Policies · p. 12
• Some DTap operations are never admissible, while publishing content or placing orders requires independent review of the exact payload; a Lean theorem characterizes key conditions on admitted calls.The theorem requires a contracted tool, a valid grant for each effect, and an unconsumed confirmation when approval is needed.Source: D Policies · p. 13

E Experimental Setup

• The τ 2-bench evaluation runs 278 tasks once per model and arm, with a 240-step or two-hour episode limit; unscored episodes count as failures.The task set comprises 114 retail, 50 airline, and 114 telecom tasks.Source: E Experimental Setup · p. 13
• DTap evaluation covers seven domains with available runners, and Table 6 describes evaluated benign and attack cases plus unscored episodes and their causes.The other seven domains lack runners in the evaluation cluster.Source: E Experimental Setup · p. 13, Table 6 · p. 14
• Table 7 categorizes calls or episodes that LeanGuard would stop, with τ 2-bench counts based on replayed Lean-policy failures and DTap counts based on matched transcripts.The table notes that consent cannot be checked offline, stricter-than-benchmark rules are excluded, and some domain cases are omitted.Source: Table 7 · p. 14

Without a guard

• 33 unguarded calls across 28 episodes executed and changed state, failing a state rule in 14 cases, a temporal rule in 17, and a prohibition in 3.One call failed both a state and a temporal rule; offline consent checks make the 13 authorization failures a lower bound.Source: F Failure Profile (RQ1) · p. 14

Calls LEANGUARD stopped

• None of LEANGUARD’s stopped calls executed; among benign DTap stopped calls, 61.7% (9,431 of 15,291) failed for missing authority or approval.In medical DTap cases, denied patient registration led many later calls to fail with a missing-patient state error.Source: F Failure Profile (RQ1) · p. 14

Rules behind each category

• On τ 2-bench, calls to the customer’s own device tools account for almost all invalid invocations, while airline and retail confirmation rules account for more than half of authorization failures.On DTap, each template rule maps to one category, and state failures include fail-closed errors such as an unregistered medical patient.Source: F Failure Profile (RQ1) · pp. 14–15

Failure categories

• Among calls LEANGUARD stopped, the temporal category included 164 calls stopped only by rules stricter than the benchmark: retail.modify_once and stable_identity.Source: Table 8 · p. 15

τ 2-bench by domain

• LEANGUARD + feedback lowered retail task success by 7.9 pp and raised airline and telecom success by 2.4 and 2.5 pp, respectively.On the official test split, Qwen3.5-4B task success fell from 86.5% to 82.2% overall, with a 11.9 pp drop in retail and a 3.1 pp rise in telecom.Source: G Enforcement (RQ2) · p. 15, Table 10 · p. 16, Table 11 · p. 17

Judge-flagged episodes

• Audits of judge-flagged calls admitted by LEANGUARD across its two arms found disagreements when judges lacked trusted runtime evidence or cases involved behavior outside the compiled policy.Source: G Enforcement (RQ2) · p. 17

Comparison with other guardrails

• 0.0% of episodes had an executed call violating the Lean policy under LEANGUARD, versus 2.0% with ToolSafe and 2.6% with Progent.The 0.0% result holds by construction because LEANGUARD dispatches only admitted calls; consent cannot be checked offline for the other guards.Source: G Enforcement (RQ2) · p. 15

DTap by model and domain

• Direct attacks fell to 0.0% in travel, finance, and legal, while indirect attacks remained highest in customer service (10.8%) and travel (9.7%).Benign success was 75.1% to 75.3% in telecom, but fell to 0.0% in travel, finance, and legal under the read-only deployment.Source: G Enforcement (RQ2) · pp. 15–16

Without the medical domain

• Without medical cases, benign success fell from 60.2% (1,669/2,771) to 24.3% (636/2,613), while direct attack success fell from 59.9% (1,127/1,882) to 2.5% (48/1,936).Half of the 1,918 benign cases solved without a guard but failed with LEANGUARD + feedback were medical cases where patient registration was denied.Source: G Enforcement (RQ2) · p. 17

Medical attack categories

• In medical DTap attacks, the three direct-attack categories requiring a tool call fell to 0.0%, while five other direct-attack categories retained 21.4–37.0% success.Under indirect attack, every medical category stayed at or below 6.8%.Source: G Enforcement (RQ2) · p. 17

Attacks without a tool call

• Response-text-only attacks fell from 41.0% to 30.2%, and 289 attacks still succeeded without any admitted state-changing call.Of the successful attacks, 158 involved no admitted call and 131 involved only reads; LEANGUARD checks tool calls, not response text.Source: G Enforcement (RQ2) · p. 17

Tools whose effect LEANGUARD cannot model

• LEANGUARD stopped 5,792 DTap calls whose effects it could not determine, including 2,728 general shell commands, 1,143 finance trades, and 1,082 telecom record writes.The runtime fails closed when a contract cannot determine a call’s effect.Source: G Enforcement (RQ2) · p. 17

What agents do after a denial

• After a bare denial, 30% of denials were followed by the same call being denied again, versus 22% with feedback.With feedback, 7% of denials were followed by the same call being admitted after the missing requirement was met, compared with 4% after a bare denial.Source: H Recovery and Repair (RQ3, RQ4) · pp. 18–19, Figure 5 · p. 20

DTap outcomes

• In DTap’s read-only deployment, aggregated over five models, attack success fell in every domain from unguarded rates to rates with LEANGUARD + feedback, while telecom retained benign success.Source: Figure 4 · p. 19

Recovery and task success

• With feedback, 35 of 48 recovered actions (72.9%) belonged to solved episodes, compared with 26 of 34 (76.5%) after a bare denial.Episodes with a denial but no recovery were solved in 34.9% of cases with feedback and 34.6% without.Source: H Recovery and Repair (RQ3, RQ4) · p. 20, Table 23 · p. 21

Implementation

• Repair search tries up to 32 candidate edits in preference order and returns the first whose goal it can prove.The tactic combines concrete evaluation with arithmetic, equality reasoning, and lemma instantiation.Source: H Recovery and Repair (RQ3, RQ4) · pp. 20–21

Which denials can be repaired

• guard_repair? proved admissible edits for 88 of 252 argument-value denials (34.9%); per-denial search took a median 2 ms, with a maximum of 70 ms.Source: Table 24 · p. 21, H Recovery and Repair (RQ3, RQ4) · p. 21