LeanGuard Adds Lean4-Verified Guardrails to Tool-Using Agents

Introduction

Once a language-model agent can query systems, change records, or trigger external actions, safety depends on more than the text it produces. The important question is whether the action eventually reaches the environment. A model may understand a broad task correctly and still issue a forbidden call because of a misleading instruction, a prompt injection, or an unsafe argument. LeanGuard addresses this point in the execution path: every proposed tool call is checked before it is released to the environment.

Key points

• Policies cover state and history. LeanGuard policies are written in Lean4. They combine predicates over the current state with scoped past-time temporal operators, allowing a policy to describe both the present call and relevant events that happened earlier in the trajectory.
• The default is fail-closed. If compliance cannot be established, the call is denied rather than treated as acceptable. The authors also prove that the decision procedure corresponds to a LeanLTL semantics, giving the runtime check a formal foundation.
• A denial can lead to correction. In feedback mode, the agent receives the violated rule and a hint. In proof-guided repair, Lean metaprogramming searches for a nearby alternative call, then proves that the alternative is admitted by the policy while preserving the user’s intent. The repair process does not require the model to invent the correction itself.
• The guard blocks forbidden execution. Across five Qwen models ranging from 0.8B to 27B parameters on Tau-Bench, unguarded agents made at least 33 calls forbidden by the Lean policy, while LeanGuard allowed none of those calls. Feedback did not significantly change overall task success and reduced repeated blocked attempts.
• Prompt-injection results are notable. On DTap, direct prompt-injection success fell from 57.9% to 5.9%. In the telecom setting, where benign tasks did not require writes, benign success remained unchanged. In replayed denials caused by argument values, proof-guided repair found an admissible edit for 88 of 252 cases, with a reported median time of 2 ms.

Why it matters

LeanGuard does not try to make the model infallible. Instead, it separates flexible language-based planning from the authority to perform high-impact actions. The model can interpret the request and propose a call, while a formally specified policy decides whether that call is allowed under the current state and execution history. This division is particularly relevant to account changes, data writes, and other operations where a mistaken action is more costly than a mistaken sentence.

The approach also has clear boundaries. Formal verification can establish that an implementation follows a policy; it cannot by itself show that the policy fully captures an organization’s intent. Policy maintenance, tool-schema changes, evaluation latency, and the cost of repeated denials remain deployment concerns. The reported experiments establish the value of pre-execution verification, but they do not remove the need to review policy coverage and operational behavior as systems evolve.

The broader lesson is that agent safety can be enforced at the action boundary rather than left entirely to prompts or post-hoc audits. LeanGuard offers a concrete model for combining probabilistic planning with a conservative, auditable, and formally grounded execution layer.

Source: Hugging Face Daily Papers