# LEANGUARD

Tool-using language-model agents often execute actions their domain policies forbid, and LeanGuard places policies written in Lean 4 between the model and its tools so that only admitted calls execute. On τ 2-bench, unguarded runs of five Qwen models executed at least 33 calls the Lean policy forbids, while LeanGuard executed none; on DTap, direct prompt-injection success fell from 57.9% to 5.9% and indirect success from 22.3% to 3.8%. Denials with feedback did not significantly change task success, and the read-only deployment blocks many benign writes.

Tool-using language-model agents often execute actions their domain policies forbid, and LeanGuard places policies written in Lean 4 between the model and its tools so that only admitted calls execute. On τ 2-bench, unguarded runs of five Qwen models executed at least 33 calls the Lean policy forbids, while LeanGuard executed none; on DTap, direct prompt-injection success fell from 57.9% to 5.9% and indirect success from 22.3% to 3.8%. Denials with feedback did not significantly change task success, and the read-only deployment blocks many benign writes.