Tool-using agents safely blocked from forbidden actions with leanverified guardrails
LEANGUARD: Lean-Verified Guardrails for Tool-Using Agents
Artificial IntelligenceComputation and Language
Summary
Sometimes language AI agents use tools but try to do things they're not allowed to do. The authors developed LeanGuard, a system that checks every tool action against strict rules written in a mathematical language called Lean4 before the action happens. If an action is blocked, the system can tell the AI why and even suggest a better, allowed action. Their tests showed that LeanGuard stopped all forbidden actions and reduced harmful prompt injections without hurting successes on normal tasks.
What this means in practice
- •For ai developers: Prevent AI agents from executing disallowed tool actions by enforcing verified policies during runtime.
- •For security teams: Reduce prompt-injection attacks on AI systems by automatically blocking unauthorized commands in real time.
Authors
Sreehari Sankar, Debargha Ganguly, Vikash Singh, Mohsen Hariri, Weicong Chen, Yanyan 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
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.