LEANGUARD: Lean-Verified Guardrails for Tool-Using Agents

LEANGUARD. Lean-Verified Guardrails for Tool-Using Agents. By Sreehari Sankar and nineteen others, from Case Western Reserve University and the University of Texas at Austin. Published on the second of November.

Tool-using language-model agents often execute actions that their domain policies forbid. The rule exists, the agent breaks it anyway, and the call reaches the environment. Whatever the policy says, nothing in that picture stands between the decision to call a tool and the call itself.

LeanGuard is a runtime placed exactly there. Every proposed tool call is checked against a policy written in Lean4 before the call reaches the environment. The policy stops being guidance the agent may or may not follow, and becomes a formal check that each call has to pass.

Policies combine state predicates with scoped past-time temporal operators over the execution history, so a rule can depend both on the current state and on what has already happened. Evaluation is fail-closed. And the decision procedure itself is proved equivalent to a LeanLTL semantics, so the checker provably does what the formal policy says.

A denied call can be corrected in two ways. With feedback, the agent receives the violated rule along with 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. That repair runs without the model. The first route hands the problem back to the agent with an explanation; the second fixes the call directly, and comes with a proof that the fix is allowed.

On Tau-Bench, with five Qwen models ranging from zero point eight billion to twenty-seven billion parameters, unguarded agents execute at least thirty-three calls that the Lean policy forbids. LeanGuard executes none. With feedback, task success does not change significantly. On DTap, LeanGuard cuts direct prompt-injection success from fifty-seven point nine percent to five point nine percent. In the telecom domain, where benign tasks need no writes, benign success is unchanged.

Feedback also reduces repeated blocked calls, and raises task success for four of the five models compared with a bare denial. Repair was tested on replayed denials. Among two hundred and fifty-two denials caused by argument values, repair proves an admissible edit for eighty-eight, in a median of about two milliseconds.

Two things sit side by side here. One is the guarantee: no forbidden call reaches the environment, and the decision procedure behind that is proved against a formal semantics. The other is recovery. A denied call need not end the task, since feedback or proof-guided repair can turn it into one the policy admits.