LeanGuard: A Lean-verified guardrail for tool-calling agents

LeanGuard is a runtime guardrail that validates each tool call with policies written in Lean4 before it reaches the environment, evaluates in a fail-closed manner, and proves the decision process equivalent to LeanLTL semantics. Policies combine state predicates with scoped past-time temporal operators acting on execution history. When testing five Qwen models (0.8B-27B) on Tau-Bench, agents without the guardrail executed at least 33 policy-forbidden calls, while LeanGuard executed none, and task success rate did not change significantly with feedback. On DTap, LeanGuard reduced the direct prompt injection success rate from 57.9% to 5.9%. Rejected calls can be corrected by returning the violated rule and a hint to the agent, or by using Lean metaprogramming to search for and prove a neighboring call that preserves user intent without going through the model; the authors state that feedback reduced repeated rejected calls and improved task success rate over rejection alone on four of the five models.