LeanGuard: Lean 4-verified runtime blocks prompt-injection tool calls by agents
CWRU · hf · 2026-11-03
Researchers at Case Western Reserve University and UT Austin present LEANGUARD (arXiv, Nov 2), a verified runtime that checks every proposed tool call against a policy written in Lean 4 before it reaches the environment. Policies combine state predicates with scoped past-time temporal operators over the execution history; evaluation is fail-closed and the decision procedure is proven equivalent to a LeanLTL semantics. Denied calls can be auto-repaired via proof-guided search. The system substantially reduces unauthorized executions and prompt-injection success (the paper demos the classic 'swap my last bookshelf order for a camera' gift-card scam) without harming benign task performance.
More from Safety
- AI Finds Bug Enabling Infinite XRP Minting, Earning $250K Bounty — massimosgrelli · 2026-11-03
- Frontier AI Safety and Governance 2026 report released at Wuzhen Summit — S_OhEigeartaigh · 2026-11-03
- CrowdStrike to acquire AI security testing startup Dreadnode — joshua_saxe · 2026-11-03
- Harvard breach: 850.5k alumni emails now searchable on Have I Been Pwned — 0xkarasy · 2026-11-03
- Pliny: frontier labs' 'safety and alignment' rhetoric is like taking health advice from Big Tobacco — davidmanheim · 2026-11-03
- Ballistic Ventures' Insider Risk Maturity Model targets human and AI agent threats — philvenables · 2026-11-03