Lean-checked guardrail cuts direct prompt-injection success from 57.9% to 5.9%
LeanGuard checks every tool call an agent proposes against a policy written in Lean4, a language for machine-checked proofs, and blocks the call before it reaches the environment if the policy forbids it. On Tau-Bench with five Qwen models, unguarded agents executed at least 33 forbidden calls and LeanGuard none, with no significant change in task success when agents get feedback. On DTap it cut direct prompt-injection success from 57.9% to 5.9%.