如果你用过任何一款 AI 编程 agent——那种能自己调工具、写代码、再读回结果的程序——你大概率会反复按一个按钮：回退到上一步。这听起来人畜无害，但最近一组研究者用 Lean 机械化证明告诉我们一件反直觉的事——回退到上一步，即使操作本身完全合法，也可能让同一次工具调用被悄悄授权了两次，或者反过来，让你原本拿到的结果凭空消失。换句话说，”撤销”在 agent runtime 里不是免费的，agent 的 checkpoint、fork、restore、merge 这四种”执行编辑”操作里，藏着三类我们之前看不见的事故。
一、为什么”撤销”在 agent 时代不再是无害动作
过去的”撤销”操作面对的是一段确定的文本或文件：你按 Ctrl+Z，文档回到上一个状态，前一个状态被丢掉，两边互不影响。Agent runtime 完全不是这样。一个 agent 的执行轨迹里有几类东西：已经被授权但还没真正发出去的工具调用、已经发出去但 agent 还没收到回应的请求、已经收到的工具结果、还有那些 agent 已经拿来做下一步推理的”事实”。当用户在 agent 里点了”回到上一步”，runtime 要做的不是简单地把文字回滚，而是要在这一长串半成品动作里，挑出哪些被”撤销”，哪些保留。
问题在于，这个”挑”的动作不是人做的，是 runtime 自己推断的。而 runtime 能看到的”授权”，是上一轮执行时给的。runtime 没有能力反悔一个已经被授权的工具调用——授权一旦发生就发生，它不能追回；runtime 也没办法把已经发出但还没回响的请求”撤回来”，那条消息已经离开本机了。结果就是，看似无害的 fork、restore、merge 操作里，藏着三种实际会发生的不一致：
第一种，双重授权。runtime 觉得”上一轮已经授权过一次工具调用了，这次回退回去之前，那个授权算继续生效”。但用户在界面上看到的，是”我刚才明明退回去了，怎么这个工具又跑了一次”。
第二种，结果失踪。runtime 把执行轨迹回滚到某个 checkpoint，丢掉了 checkpoint 之后才出现的某个工具结果。用户的视角是”我明明让它查过这个东西，怎么再问一遍就完全没那段记忆了”。
第三种，在途冲突。runtime 正在 fork 的同时，另一条并行的执行轨迹正在用相同的参数调用同一个工具。两边都跑了一遍，最后留下的两个结果里，只有一个会被 agent 看见，另一个就此失踪。
二、研究者的解法：把”能不能安全执行”做成可判定算法
这组研究者没有止步于”发现了 bug”。他们直接把”在某个执行轨迹上做 fork/restore/merge 操作到底安不安全”这件事，做成了一个形式化可判定的问题。给定一段具体的执行轨迹，算法要么返回”这是所有可以安全继续执行的方式”，要么给出”在当前轨迹下，不存在任何一种安全的实现方式”——而且后者是带机器可验证证明的。
为了让这件事不只停留在纸面，他们用 Lean 把整套逻辑机械化了一遍。换句话说，这不是一个”理论上应该对”的论证，而是一个可以在证明助手里跑出来的真东西。这种风格的论文，过去更常出现在编译器正确性、共识协议、密码学证明里，把它用在 agent runtime 的”撤销”操作上，本身就说明这件事的复杂度已经被低估很久了。
更有意思的是，他们的算法不是”给 agent 加一条新约束”。agent 是不可信的——它可能乱发工具调用、可能跳过 runtime 的检查、可能用一些 runtime 看不到的副作用去影响下一步执行。整套安全保证建立在 runtime 自己手里的”执行轨迹”之上：runtime 不相信 agent 接下来要做什么，只看它已经做过什么，再决定这次 fork/restore/merge 能不能继续。这种”不信任执行者，只信任日志”的思路，跟数据库事务和分布式系统的两阶段提交是同源的。
三、它意味着什么：每次按”撤销”之前，先想想这四件事
这篇论文对普通 AI 编程用户的直接意义，是让我们重新认识”撤销”按钮的代价。它不是一个无副作用的 UI 操作，它是一次会改变授权状态、改变 agent 记忆、改变并发结果的事务。你按下去之前，最好在心里过一遍：
1. 这次回退的 checkpoint 之前，有没有已经发出但还没回应的工具调用？那些调用要么会带着旧授权跑完，要么会因为结果对不上而让你下次推理时多出一个”幽灵事实”。
2. 你和 agent 之间的对话里，有没有某段信息是在这个 checkpoint 之后才拿到的？如果有，那段信息大概率会被一起丢掉，agent 接下来会表现得像失忆。
3. 你是不是在 agent 还在调用外部 API 的时候按了撤销？如果是，那条 API 调用已经离开本机，撤销并不能把它召回来，只能决定它回来的结果还算不算数。
4. 你会不会在几秒钟后再按一次 forward？forward 不是 fork 的逆操作——它会把上面那三类不一致原封不动地带回来，甚至放大。
“Execution edits cannot undo an earlier authorization or a tool request already sent. An unsafe edit can therefore authorize the same tool action twice, discard a result the task still requires, or conflict with a call that began before the edit.”——研究者论文原文给出的三类失败模式总结
形式化证明帮我们确认了一件事：在 agent runtime 上，撤销是一个有真正成本的操作。这个成本之前一直被 UI 上的”无副作用”假象藏着。今天起，每一次按”撤销”按钮，都值得你先停一秒，问一句”那条已经发出去的请求，会不会让我等下重复执行一次”。
本站编辑整理，资料来源公开网络。如有错误欢迎指正。