以下为上游提供的源文稿，可能存在识别错误。
乔木转写是基于源文稿的中文提炼，不是逐字翻译。请核对原文中的人名、数字与观点。
选一篇，慢慢读
从左侧挑一篇，正文会在这里排成书页。
Tool-using language-model agents often execute actions that their domain policies forbid. We present LeanGuard, a runtime that checks every proposed tool call against a policy written in Lean4 before the call reaches the environment. Policies combine state predicates with scoped past-time temporal operators over the ex
阅读原文 · Sreehari Sankar, Debargha Ganguly, Vikash Singh, Mohsen Hariri, Weicong Chen, Yanyan Zhang, Shouren Wang, Wang Yang, Chaoda Song, Alexander Nemecek, Osama Zafar, Idan Davidovich, Yuting Shao, Kai Ye, Biyao Zhang, Xinpeng Li, Joe Stubbs, Erman Ayday, Jing Ma, Vipin Chaudhary
向阳乔木 · opencode-go/deepseek-v4.1-flash
工具调用型 Agent 出事，多数时候不是模型不会用工具，是它用了不该用的方式。LeanGuard 想干的事很具体： 在工具调用真正落到环境之前，用 Lean4 写的策略把它拦下来，而且拦截过程本身是可证明的。 这篇论文值得看的地方在于它没有停在“加一层规则过滤”。规则谁都会写，难的是两件事：策略语义要说得清，判定过程要信得过。LeanGuard 把这两件事...