LEANGUARD: Lean-Verified Guardrails for Tool-Using Agents

AI summary

Overview

Research area: AI agent safety and runtime enforcement — specifically, formal verification of tool-calling language-model agents using the Lean 4 proof assistant.

Technical level: Advanced. The paper assumes familiarity with interactive theorem proving, linear temporal logic, and agentic tool-use benchmarks; the core artifact is a machine-checked Lean development rather than an empirical study alone.

Scope (one sentence): The paper presents LeanGuard, a Lean 4 runtime that intercepts every proposed tool call from a language-model agent, decides admissibility against a formally verified policy over state and execution history, and offers two mechanisms for correcting denied calls — model-side feedback and Lean-side proof-guided repair.

What This Paper Is About

Language-model agents that call tools can execute actions their domain policies forbid: cancelling a flight that already departed, refunding an order the customer does not own, or acting on instructions injected into a tool's output. The authors place a verified checkpoint between the model and its environment, so a tool call runs only if a policy written in Lean 4 admits it, and the admission procedure is proved correct against an independent temporal-logic semantics. The paper also asks what should happen after a denial: can the model fix its call from structured feedback, or can Lean itself search for a nearby admissible edit and return it with a kernel-checked proof?

Key Contributions

1. A verified admission procedure. LeanGuard is a Lean 4 runtime whose decision function is proved equivalent to an independent LeanLTL (linear temporal logic) interpretation of the policy, lifted from single temporal formulas to authorization and to the full fail-closed admission decision. A verification script rejects any exported theorem depending on sorry or a nonstandard axiom.

2. Proof-guided repair. A Lean metaprogramming tactic, guard_repair?, searches a finite set of candidate edits to a denied call and returns one together with a kernel-checked proof that the policy admits it — with no involvement from the model. The authors state that, to their knowledge, no existing agent guardrail produces proved repairs.

3. Feedback-guided recovery. Instead of a bare denial, LeanGuard returns the identifiers of the failed rules plus a natural-language hint. The paper measures how this changes retry behavior, recoveries, and task success relative to bare denial.

4. A taxonomy and measurement of policy-violating calls. Five categories — invalid invocation, state incompatibility, temporal incompatibility, authorization failure, and policy prohibition — each mapped to a specific part of LeanGuard, with counts of stopped calls on both benchmarks.

Main Findings

• No forbidden call executes under LeanGuard on τ²-bench. Replaying unguarded episodes finds at least 33 calls, across 28 episodes, that the Lean policy forbids and that executed and changed state; with LeanGuard none of the 1,702 stopped calls ran. The five models are Qwen3.5-0.8B, 2B, 4B, 9B, and Qwen3.8-27B.

• Task success is not significantly changed with feedback. τ²-bench task success is 72.7% unguarded, 70.9% with LeanGuard plus feedback (p = 0.21), and 68.9% with a bare denial (p = 0.007). Per-model effects range from a gain of 4.4 pp for Qwen3.5-2B to a loss of 6.5 pp for Qwen3.8-27B.

• Prompt-injection success drops sharply on DTap. Direct attack success falls from 57.9% to 5.9%, and indirect attack success from 22.3% to 3.8%.

• Protection need not cost utility where benign tasks need no writes. In telecom, benign success is essentially unchanged (75.1% vs. 75.3%) while direct attack success falls from 55.1% to 2.4%.

• The read-only DTap deployment overstates protection. Because the session holds no write grants, reviews, or confirmations, benign success falls overall from 53.1% to 12.5%; tasks needing writes fail in travel, finance, and legal, and in medical the patient registration itself was denied. The authors call the 0.0% attack success in write-dependent domains an upper bound on protection under a read-only deployment.

• Judge-flagged episodes fall modestly. An LLM judge (Qwen3.8-27B) flags 9.7% of τ²-bench episodes unguarded, 5.6% under LeanGuard, and 6.5% with feedback (p = 0.002 for LeanGuard plus feedback). Flagged episodes under LeanGuard are not formal violations; an audit of 88 flagged episodes found judge errors such as ignoring trusted runtime evidence, including 18 roaming activations allowed because the line was abroad.

• Feedback reduces repeated blocked calls and raises recoveries. Blocked calls fall from 983 to 719 across all models; Qwen3.5-2B goes from 271 blocked calls for 141 distinct denied actions (about 1.9 per action) to 144 for 104 actions (1.4 per action). Recovered actions rise from 34 to 48, from 5.5% to 9.1% of denied actions (p = 0.02). Feedback raises task success for four of five models, by 2.2 to 5.8 pp, and from 68.9% to 70.9% overall (p = 0.13).

• Proof-guided repair succeeds on a third of argument-level denials. Of 252 denials caused by argument values, guard_repair? proves an admissible edit for 88 (34.9%), in a median of 2 ms per denial (at most 70 ms). Most repairs refund to the order's original payment method (64) or pay for a flight change by card instead of a travel certificate (18). All 7,720 admission decisions from the live runs were reproduced in the Lean replay, and each of the 1,613 denials was checked as a theorem.

• Proved repairs agree with what successful agents do. When the agent itself later issued the repaired call, the task succeeded in 16 of 22 cases, against 7 of the other 66. The search ran after the episodes, so agents never received these repairs.

• Authorization failures dominate stopped calls. On τ²-bench, authorization failures account for 572 calls (338 writes without the customer's confirmation, 268 acting on a resource the customer does not own), invalid invocations 551 (nearly all telecom agents calling the customer's own device tools), temporal incompatibility 411 (164 stopped only by the two stricter rules), and prohibitions 313 (mostly airline cancellation, change, booking, and compensation rules). On DTap, attacks lead mostly to authorization failures (60%) and invalid invocations (58%), and 13% of stopped calls use tools whose effect LeanGuard cannot model, such as general shell commands.

• Response-text harm is out of scope. Attacks whose harm lies in the response text still succeed in 30.2% of guarded customer-service and travel episodes (41.0% unguarded), and five medical attack categories keep 21.4–37.0% success under direct attack.

Methodology in Plain English

The model never sees anything new: it emits an ordinary structured tool call against the environment's ordinary schema. The host intercepts that call before it reaches the tool and treats the arguments, and any text inside tool outputs, as untrusted data. A domain adapter then snapshots the authoritative backend, validates the arguments, and derives the facts the policy needs; each snapshot carries a revision, so a policy cannot be satisfied by text asserting that the customer already approved something.

Policies are ordinary Lean 4 definitions combining state predicates with three past-time operators over the execution history: previous (held at the preceding relevant event), once (a matching event occurred earlier), and since (a condition has held continuously since a witnessing event). Each operator can be restricted to a time window and to a scope such as a principal, conversation, or resource, so "the previous observation of this order" means that order. Rules come in three kinds — permits, requirements, and forbids — and a broad permit cannot override an unmet requirement or an applicable forbid. Evaluation is fail-closed: missing or malformed data is distinguished from a predicate returning false, and an action is admitted only if every relevant component evaluates without error.

To show the evaluator actually matches the specification, the authors embed the history as a LeanLTL trace running newest event to oldest, interpret each policy constructor in that logic, and prove for every history that the executable evaluator returns true exactly when the trace satisfies the interpretation. Proofs are checked when the policy is built, not per tool call.

Admission fits into a monitored protocol: an admitted call records a dispatch reservation before the tool runs, so a single-use operation cannot be repeated while its outcome is unknown. User confirmation is bound to the exact proposal, arguments, resource, and state revision, and is single-use.

For repair, the authors define a repair as a witness that some candidate edit preserves the user's intent (EditOK) and is admitted by the policy. The guard_repair? tactic tries candidates in order and discharges each goal with guard_solve, which combines evaluating concrete predicates with the arithmetic, equality reasoning, and lemma instantiation of Lean's grind engine. Policy authors can register proved facts via a guard_rule attribute.

Empirically, the tool-enforceable subset of τ²-bench policies for retail, airline, and telecom was drafted by an authoring skill and corrected by hand, yielding 45 rules over 43 agent tools in 583 lines of Lean (retail 16 tools/17 rules/97 lines; airline 14/14/288; telecom 13/14/136; 62 shared lines). For DTap, one policy template with eight rules is instantiated per application with 199 reviewed tool contracts across seven of the benchmark's 14 domains (telecom 44, customer service 40, legal 37, travel 25, medical 22, OS-filesystem 18, finance 13). Evaluation uses 278 τ²-bench tasks at revision 672227c (114 retail, 50 airline, 114 telecom), seed 300, with three arms: Unguarded, LeanGuard, and LeanGuard + feedback. LeanGuard never consults the benchmark's reference solution or scoring assertions, so task completion and policy compliance are measured separately.

Why This Matters

The paper moves agent guardrailing from heuristic checking to machine-checked guarantees at the execution boundary, and it treats a denial as a problem to be solved rather than a dead end. It also makes a distinction the field often blurs: whether an action is well-formed is a different question from whether it is permitted, and the latter depends on state, history, and consent.

Real-world applications:

• Customer-service and retail agents that issue refunds, exchanges, and order modifications, where the policy requires ownership checks, prior reads, and single-use customer confirmation — the paper's running example is a retail exchange where an injected instruction would bill a price difference to an attacker's gift card.
• Airline and travel booking systems, where state preconditions (a flight has not departed) and prohibitions (non-refundable tickets) must hold before a mutation, and where payment-method substitutions are a common repairable error.
• Enterprise tooling with least-privilege requirements, where every effect must be covered by an exact grant naming principal, tenant, resource, operation, destination, clearance level, maximum amount, and validity window — with eight operations never admissible, including disabling security controls, exporting credentials, erasing audit logs, installing persistence, and escalating privileges.
• On-device or latency-sensitive assistants, where the authors motivate compact models running within tight latency, privacy, and compute budgets; policy proofs are compiled once at build time rather than checked per call.

Industry relevance: The dispatch-reservation and consent-binding protocol addresses concrete failure modes in production agents — retrying a payment after an ambiguous timeout, or reusing an approval for different arguments. The read-only DTap result is a direct warning to practitioners: a deployment that withholds all write grants will look very safe on attack metrics while breaking most benign tasks, so protection numbers must be reported alongside utility.

Future Directions

• Calling repair at runtime. The runtime does not yet invoke guard_repair?; it was evaluated only on replayed denials. Delivering a proved repair to the agent, and measuring whether it improves task success beyond feedback, is the most direct next step.

• Widening the verified boundary. The guarantee currently covers tool calls only. Harm carried in response text — which still succeeded in 30.2% of guarded customer-service and travel episodes, and in 21.4–37.0% of several medical attack categories — is outside it. Extending verification to generated content, and to the conversion of free-form dialogue into consent records, would close the largest stated gap.

• Reducing formalization dependence. The guarantee is relative to a hand-corrected, LLM-drafted formalization of the tool-enforceable policy subset, and proof checking cannot catch errors in that step. Better authoring, review, and reference-equivalence checking for formalized policies is an open problem, as is covering the remaining DTap domains (seven of 14 were evaluated).

• Broadening the evidence. All experiments use one model family (Qwen), English-language tasks, and simulated users; two τ²-bench rules (retail.modify_once and stable_identity) are stricter than the benchmark's own policy; and judge-flagged rates come from a model that is also one of the evaluated systems. Replication across model families, languages, and independent judges would test generality.

Target Audience

Researchers and engineers working on agent safety, runtime enforcement, and neurosymbolic verification will get the most from this paper, particularly those already comfortable with Lean or temporal logic and those building production tool-use systems that need auditable authorization. It is also relevant to benchmark designers interested in measuring what happens after a guardrail blocks an action, and to policy authors who need to know what a formal specification does and does not buy them. Readers without a formal-methods background can still extract the empirical results from Table 1 and Table 2, but the methodological core assumes familiarity with proof assistants.

Authors’ abstract

Tool-using language-model agents often execute actions that their domain policies forbid. We present LeanGuard, a runtime that checks every proposed tool call against a policy written in Lean4 before the call reaches the environment. Policies combine state predicates with scoped past-time temporal operators over the execution history, evaluation is fail-closed, and the decision procedure is proved equivalent to a LeanLTL semantics. A denied call can be corrected in two ways. With feedback, the agent receives the violated rule and a hint; with proof-guided repair, Lean metaprogramming searches for a nearby call that preserves the user's intent and proves that the policy admits it, without the model. On Tau-Bench with five Qwen models (0.8B-27B), unguarded agents execute at least 33 calls that the Lean policy forbids, while LeanGuard executes none; with feedback, task success does not change significantly. On DTap, LeanGuard reduces direct prompt-injection success from 57.9% to 5.9%, and in telecom, where benign tasks need no writes, benign success is unchanged. Feedback reduces repeated blocked calls and raises task success for four of five models over a bare denial. On replayed denials, repair proves an admissible edit for 88 of 252 denials caused by argument values, in a median of 2,ms.