VeriGuard：通过可验证代码生成提升 LLM Agent 安全性

论文提出 VeriGuard，用离线形式化验证与在线监控为 LLM Agent 提供可证明的安全约束。其架构分两阶段，离线阶段把用户的安全约束澄清为形式化规格，合成行为策略并反复测试与形式化验证直至可证明合规；在线阶段以轻量监控器在每次动作执行前对照已验证策略校验，不合规则拦截。该方法的保证仅限规格覆盖的行为，规格不完整时仍可能出现规格博弈；它只校验提议动作而非内部推理，内部谋划有害行为但表面合规的 Agent 会通过监控。文章还提出如何把形式化验证扩展到连续、物理的动作空间这一开放问题。