LEANGUARD introduces a runtime guardrail system for tool-using language-model agents that enforces domain policies written in Lean4 before tool calls reach the environment. Policies combine state predicates with scoped past-time temporal operators over execution history, and evaluation follows a fail-closed decision procedure proved equivalent to a LeanLTL semantics. When a call is denied, LEANGUARD offers two correction mechanisms: feedback, which returns the violated rule and a hint to the agent, and proof-guided repair, which uses Lean metaprogramming to search for a nearby admissible call that preserves user intent and proves policy compliance without model involvement. Evaluated on Tau-Bench with five Qwen models (0.8B–27B), unguarded agents executed at least 33 policy-forbidden calls while LEANGUARD executed none; task success with feedback did not change significantly. On DTap, direct prompt-injection success dropped from 57.9% to 5.9%, and in telecom benchmarks where benign tasks require no writes, benign success remained unchanged. Feedback reduced repeated blocked calls and improved task success for four of five models over bare denial. On replayed denials caused by argument values, proof-guided repair produced a verified admissible edit for 88 of 252 cases with a median latency of 2 ms.