LLM 智能体（agent）会生成并执行多步计划，计划中会调用外部工具；这些工具既可访问私有数据，也可执行命令。在此场景下，安全性并非某个单一步骤的属性，而是由计划所形成的整个执行过程的属性；计划本身就是关键工件，记录了工具调用、控制流与数据依赖关系。论文提出 CaMeLoT，作为已有防御方案 CaMeL（面向工具型 LLM 智能体的提示注入防御）的补充。CaMeLoT 在 CaMeL 基础上增加一个静态验证层，在调用任何工具之前对智能体计划进行检查。其核心方法为：把生成的计划翻译成有限状态迁移系统，用工具调用、provenance（数据来源）与污点信息对该系统进行标注，再使用 CTL（计算树逻辑）表达时序安全策略，并借助 nuXmv 模型检验器进行验证。由于验证发生在执行之前，不安全的计划会被直接拒绝，无需调用 LLM 或执行工具，从而节省运行时本会消耗的 token，也避免了回滚已发生的变更或拆除临时沙箱的成本。当验证失败时，模型检验器会返回反例，用于向智能体提供反馈以修复计划。评估方面，作者在来自 AgentDojo 基准、SOC 工作流和提示抽取（prompt-extraction）实验的策略集上对 CaMeLoT 进行了测试，结果表明它能够在执行前验证广泛的时序属性，同时保留 CaMeL 原有可运行时检查的覆盖范围。该工作属于形式化方法与 LLM 智能体安全的交叉方向，适合智能体安全、安全编排与形式化验证方向的研究者和工程师阅读。