Sreehari Sankar, Debargha Ganguly, Vikash Singh, Mohsen Hariri, Weicong Chen, Yangyan Zhang, Shouren Wang, Wang Yang, Chaoda Song, Alexander Nemecek, Osama Zafar, Idan Davidovich, Yuting Shao, Kai Ye, Biyao Zhang, Xinpeng Li, Joe Stubbs, Erman Ayday, Jing Ma, Vipin Chaudhary
7 min
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.
Alex: Ownership is a current fact. But some policies say you must look something up before changing it. How does LeanGuard handle that?
Sam: It uses temporal policies: rules that depend on earlier events. The monitor keeps a history, so it can require a prior resource lookup or authentication. Those checks can be scoped to the relevant customer or order, rather than whatever happened most recently.
Alex: And if a payment times out, the history has to distinguish an unknown outcome from permission to try again.
Sam: The system records a reservation before dispatching an admitted call. A single-use operation stays unavailable while its outcome is unknown. Missing or malformed evidence also causes denial, rather than becoming a loophole in the rules.
Alex: Now the proof. Does it establish that the agent cannot do anything unsafe?
Sam: No. It establishes that an allowed call satisfies the formal policy’s independently defined meaning. The proofs are checked when the policy is built, not constructed for every ordinary call. The execution guarantee assumes faithful backend evidence and that every consequential call passes through the monitor.
Alex: That makes policy authoring part of the safety boundary. A perfectly checked rule can still leave something important out.
Sam: The authors explicitly say so. They formalize only the tool-enforceable subset of the benchmark policies. An automated aid drafts rules, but humans review and correct them. The proofs cannot catch omissions or mistakes in that translation.
Alex: With that boundary clear, what did they actually test?
Sam: They used retail, airline, and telecom tasks from tau-squared bench, a benchmark with stateful tools and simulated customers. Each evaluated Qwen model attempted 278 tasks per experimental arm. They compared unguarded execution, a bare denial, and denial with explanatory feedback.
Alex: What is the clearest evidence that enforcement worked?
Sam: Unguarded agents executed at least 33 calls that changed state despite violating the Lean policy. Under LeanGuard, the count was zero. That is the boundary working as designed, not evidence that the models stopped proposing bad actions.
Alex: And the usefulness question from the start: could guarded agents still finish the tasks?
Sam: With feedback, success was about 71 percent, compared with about 73 percent unguarded. The difference was not statistically significant in that main comparison. But that does not establish equivalence, and the effects varied across models and domains.
Alex: Is there a particular reason not to flatten those differences into “no cost”?
Sam: Retail success fell, while airline and telecom improved in the pooled feedback results. A separate run on the official test split also showed an overall decline. All experiments used one model family, English-language tasks, and simulated users.
Alex: The paper also tests malicious instructions. Does the same protection survive when someone deliberately tries to redirect the agent?
Sam: On DTap, a prompt-injection benchmark, direct attack success dropped from about 58 percent to about six percent. But this deployment was read-only: it supplied permission to read records, not to make changes. That restriction also blocked legitimate tasks needing writes.
Alex: Then the attack reduction comes partly from withholding capabilities the benign task might need.
Sam: The authors acknowledge that. Benign success fell sharply overall, though it stayed essentially unchanged in telecom, where benign tasks rarely needed writes. And successful attacks remained when the harm was in the response itself, such as manipulated medical advice or false claims.
Alex: What about recovery? Does explaining a denial do more than make the refusal easier to understand?
Sam: Compared with bare denial, feedback reduced repeated blocked calls and increased later recovery of denied actions. Task success improved for most evaluated models, though the overall improvement was not statistically significant. The natural-language hint itself is not verified; the failed-rule record comes from the policy.
Alex: And the proved corrections are still a separate result, rather than something those agents received?
Sam: Yes. Offline search repaired about a third of denials caused by argument values. Common fixes restored the original refund payment method or changed how a flight change was paid for. It could not manufacture missing customer approval, and any repaired call would still need fresh admission.
Alex: Who should read the full document, and where should they start?
Sam: Researchers building agent infrastructure or combining formal methods with language models should read the admission guarantee beside the Limitations. Then examine the enforcement results, especially the read-only attack setting. Read proof-guided repair for the proposed next step, remembering that its effect on live task completion remains untested.
Alex: And what should everyone else carry away?
Sam: A verified action boundary is not a verified agent. LeanGuard shows how to enforce the rules you encoded, not how to prove you encoded every rule that matters.
Alex: Thanks for listening.