本文研究智能体（Agent）运行时环境中一种被称为“执行编辑”（execution edits）的操作安全性问题。执行编辑包括 Checkpoint（记录当前执行状态）、Fork（分支）、Restore（恢复某个检查点）和 Merge（合并分支），这些操作允许在不重启任务的情况下改变智能体的后续执行路径。然而，执行编辑无法撤销先前的授权或已经发出的工具请求，因此不安全的编辑可能导致同一工具动作被重复授权、丢弃任务仍需要的结果，或与编辑前已开始的调用产生冲突。由于智能体本身不可信，运行时必须依据其执行记录来确定每次编辑需要兼顾哪些过去的动作、必须保留哪些关键结果，才能确保后续执行安全。现有智能体系统却并未从实际运行中推导出每次编辑必须保留的内容，而是将这一需求作为输入条件，导致安全性缺乏严格保障。本文提出了一种算法，能够精确判定一次编辑是否安全，并返回所有安全的继续执行方式，或者证明不存在安全方式。该算法枚举任务在不违反策略的前提下可能完成的所有路径，移除那些可能导致后续无法完成关键结果的路径，若剩余路径为空则返回可验证的证明，表明不存在安全实现；否则，剩余路径精确描述了运行时可以允许的行为。形式化结果覆盖了 Checkpoint 以及 Fork、Restore、Merge 的六种形式，并扩展到原子强制实施以及精确检查器所需的信息。研究使用 Lean 定理证明器对有限检查器和运行时不变式进行了机械化验证，并通过测试验证了所有六种编辑形式。源代码、Lean 证明和可执行测试均公开在 GitHub 仓库中。该工作为智能体运行时的安全控制提供了理论基础和可验证的实现方法，适合系统安全、形式化验证和智能体架构研究者阅读。

该论文对当前人工智能安全的主流范式提出结构性批评，认为仅靠训练阶段的对齐方法（如RLHF、DPO、Constitutional AI）无法充分保障自主智能体的安全。作者主张，智能体安全应被设计为一种由执行环境（harness）强制实施的“运行时契约”，并包含两个互补的维度：预防性维度通过沙箱、权限门、输出过滤器和轨迹监视器在危险行为发生前予以阻断；证据性维度则要求对“良好行为确实发生”提供可验证的证明，例如测试运行、日志捕获、文件差异和引用溯源，并将这些证据作为任务提交的先决条件。为了支撑这一立场，论文提供了四条公开证据线：对52起已记录AI智能体/LLM安全事件的分析；对31个非争议核心案例及1个争议性说明案例的虚假完成审计；对12个公开智能体系统和执行框架的轨迹模式审计；以及对NeurIPS、ICML、ICLR 2023-2025年全部28560篇论文的标题级审计，显示训练时与部署时相关出版物的数量存在8-12倍的失衡。论文还借鉴了计算机安全和实验科学两个领域如何通过包含预防与证据元素的运行时契约来确保安全，指出智能体AI正面临同样的压力。作者形式化定义了“智能体轨迹模式”和“证据链”，提出了基于标准监视器组合的可组合门控命题，并勾勒了后续研究议程。核心结论是：智能体AI的安全单元应是“带可验证证据的轨迹”，而非模型本身。该研究面向AI安全研究者、智能体框架开发者以及安全运营人员，为将安全从训练阶段扩展到运行时执行提供了系统性的论证和初步设计框架。

该论文研究使用工具（tool-using）的智能体在运行时安全领域的可执行性（enforceability）理论。现有运行时防护栏（runtime guardrails）在不可逆的工具调用前进行干预，但它们的保证取决于可表示的策略状态、裁判（judge）的观测能力以及干预是否改变未来行为。本文分离出三个核心问题：第一，相对于固定的预言谓词（oracle predicates），确定性门控（deterministic gate）恰好能执行那些其寄存器模型能够识别的良好前缀（good prefixes）的非空安全策略；当使用两个可递减计数器时，策略非平凡性（nontriviality）不可判定，但对于可分离的单调片段（separable monotone fragment）则属于PSPACE。第二，在固定的外生规律（exogenous law）下，Neyman-Pearson引理给出了精确的误拦截/漏报前沿（false-block/miss frontier），而共形校准（conformal calibration）给出了有限样本的边际保证（finite-sample marginal certificate），可能需要通过全拦截（block-all）实现。第三，一旦拦截改变了未来的提议，静态分数与非门控轨迹（ungated trajectories）无法识别闭环前沿；一个指定的有限控制模型（finite controlled model）可以产生占用程序（occupancy program）。有界表示攻击（bounded representation attacks）引入了鲁棒性裕度，因此仅凭良性校准（benign calibration）无法迁移。实验通过静态诊断、控制模型枚举、表示重写以及配对的闭环重运行来区分这些不同方面。该论文为智能体运行时安全提供了形式化理论基础，适合安全研究者、形式化方法学者以及AI安全工程师阅读。