$ cat wiki/papers/2026/2611.02332-leanguard.md
LeanGuard — checking policy before tool execution
TL;DR
LeanGuard checks proposed tool calls against a Lean4 policy before execution. The authors report fewer prohibited actions and lower direct prompt-injection success in tested environments; this does not prove that a policy captures every safety requirement. (source)
Authors & Org
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. Affiliations are not established by the captured abstract record. First submitted 2026-11-02. (source)
Method
Policies combine state predicates with scoped past-time temporal operators over execution history. Evaluation fails closed, and the decision procedure is proved equivalent to a LeanLTL semantics. (source)
After denial, feedback supplies the violated rule and a hint. Alternatively, proof-guided repair uses Lean metaprogramming to search for a nearby call that preserves user intent and proves policy admissibility, without the language model. (source)
Results
On Tau-Bench with five Qwen models (0.8B–27B), unguarded agents execute at least 33 policy-forbidden calls; LeanGuard executes none. With feedback, task success does not change significantly. These counts concern calls forbidden by the encoded policy. (source)
On DTap, direct prompt-injection success falls from 57.9% to 5.9%. Benign success is unchanged in telecom, where benign tasks need no writes. Feedback improves task success for four of five models relative to bare denial and reduces repeated blocked calls. (source)
On replayed argument-value denials, repair proves an admissible edit for 88 of 252 denials. The abstract reports median repair time as 2,ms; that malformed unit string is preserved rather than silently interpreted. (source)
Significance
For Agent Runtime Containment and Agents (LLM Agents), this is an explicit enforcement point between a proposed action and execution. Interpretation: a proof about policy evaluation and evidence about task success answer different questions; both are needed to assess a practical guardrail. (source)
Open Questions
The abstract does not establish policy completeness, robustness to compromised tools, or safety outside the evaluated domains. Repair coverage is limited to a subset of replayed denials, and total operational overhead is not established here. Full paper and code were not reviewed. (source)