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.
Sam: An agent can propose a forbidden action without being allowed to carry it out. LeanGuard separates those steps, checking tool calls against formally verified rules before anything reaches the outside system.
Alex: Blocking mistakes sounds useful, but agents still have jobs to finish. Does this system help them recover, or just refuse?
Sam: It can return the failed rule and a hint. It also has a separate, offline method that finds some corrected calls and proves they are allowed. This is a method-and-proof preprint by Sreehari Sankar and colleagues at Case Western Reserve University and UT Austin.
Alex: So this matters to researchers whose agents change accounts, bookings, or payments. The question is whether stronger control leaves them useful.
Sam: Yes. We’ll unpack what the system actually guarantees, how the experiments test its usefulness, and where that guarantee stops.
Alex: Start with what is new. Other guardrails already check actions before they execute. What does LeanGuard add?
Sam: The authors place it alongside systems such as Progent, which expresses restrictions as symbolic constraints on tool calls. Earlier work also uses Lean, a programming language and proof assistant, to check agent actions. LeanGuard adds a proof connecting its executable checker to a separately defined meaning of the policy.
Alex: That distinction matters because a checker could implement the wrong interpretation. What else separates this from a filter?
Sam: The repair mechanism. Rather than merely choosing a safe substitute, it searches for an edit of the agent’s own call. It returns that edit only with a checked proof of permission, under an explicit condition defining which changes preserve user intent.
Alex: Let’s make permission tangible. What happens in the retail exchange example?
Sam: A customer wants to exchange a bookshelf for a camera. A malicious note inside a tool response claims the customer already approved, and tells the agent to charge a particular gift card. Without the guard, the illustrated agent follows it.
Alex: If the agent treats that note as consent, why doesn’t the checker make the same mistake?
Sam: Because the checker does not take the agent’s word for it. A trusted adapter reads the authoritative backend and supplies the facts needed for authorization. Text inside a tool response never becomes evidence of consent.
Alex: So the model proposes the exchange, but a separate channel establishes who owns the order and what they approved.
Sam: The proposed call is denied because confirmation is missing and the card is not on the account. After confirmation through a trusted screen, a reissued exchange using the customer’s card is admitted. Approval is bound to the exact proposal and state revision, and can be used only once.
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.