LeanGuard blocks forbidden tool calls before they run: direct prompt-injection success on DTap falls from 57.9% to 5.9%
Synopsis
Tool-using language-model agents often execute actions their domain policies forbid, and LeanGuard places policies written in Lean 4 between the model and its tools so that only admitted calls execute. On τ 2-bench, unguarded runs of five Qwen models executed at least 33 calls the Lean policy forbids, while LeanGuard executed none; on DTap, direct prompt-injection success fell from 57.9% to 5.9% and indirect success from 22.3% to 3.8%. Denials with feedback did not significantly change task success, and the read-only deployment blocks many benign writes.
Interpretation
LeanGuard checks every proposed tool call against a Lean 4 policy before the call reaches the environment, so a denied call never executes and the agent cannot cause a state transition the policy forbids. Earlier agent guardrails constrain calls at runtime through symbolic constraints, domain-specific languages or learned checkers; LeanGuard differs by proving its admission procedure equivalent to an independent temporal-logic semantics and by returning the violated rule to the agent. On τ 2-bench, replaying unguarded episodes found at least 33 calls that executed and changed state while failing the Lean policy, across 28 episodes; with LeanGuard, none of the 1,702 stopped calls executed. On DTap, direct injection success fell from 57.9% to 5.9% and indirect from 22.3% to 3.8%.
Policies combine state predicates with three past-time operators, which express obligations such as reading before writing or modifying an order at most once. Checks over the current state alone cannot express these ordering and counting constraints, so LeanGuard uses PREVIOUS, ONCE and SINCE, each restrictable to a time window and evaluable over events sharing a principal, conversation or resource. The retail, airline and telecom domains of τ 2-bench were formalized as 45 rules over 43 agent tools in 583 lines of Lean; evaluation used 278 tasks, with each model run once per arm.
A denied call can be corrected in two ways: the failed rules and a natural-language hint go back to the model, or Lean metaprogramming searches for a nearby call that preserves the user's intent and returns a kernel-checked proof of admissibility. A bare denial that only says the call was not executed leads agents to retry the same call; feedback cut blocked calls from 983 to 719 and raised recovered denied actions from 34 to 48. On replayed τ 2-bench denials, proof-guided repair proved an admissible edit for 88 of the 252 denials caused by argument values, in a median of 2 ms; the search ran offline after the episodes, so agents never received these repairs.
Perspective
The demonstrated scope is the retail, airline and telecom domains of τ 2-bench and seven DTap domains, with all experiments using one model family (Qwen), English-language tasks and simulated users; the guarantee holds relative to the reviewed formal specification and trusted inputs and covers only the tool-call execution boundary.
The formalization covers only the tool-enforceable subset of each natural-language policy and was drafted with a language-model authoring aid and corrected by hand, so errors in that step are not caught by the proofs; the read-only DTap deployment blocks benign writes, making its attack success an upper bound on protection; proof-guided repair was evaluated offline on replayed denials and the runtime does not yet call it; τ 2-bench violation rates come from an LLM judge that is itself one of the evaluated models.