CaMeLoT：用 CTL 时序逻辑在执行前静态验证 Agent 计划
CaMeLoT: CaMeL orchestrated with Temporal logic for static verification and liveness
AI 导读
CaMeLoT 是面向工具调用型 LLM Agent 的提示注入防御方案，作为已有防御 CaMeL 的补充，在调用任何工具之前对 Agent 生成的计划做静态验证。它把计划转换为有限状态迁移系统，标注工具调用、来源与污点信息，再用 nuXmv 模型检查器对照以 CTL 表达的时序策略进行检验。由于验证发生在执行之前，不安全的计划会被直接拒绝，无需消耗 LLM 调用和工具调用，也省去了回滚改动或拆除临时沙箱的开销。验证失败时模型检查器会返回反例，供 Agent 据此修复计划。