Anthropic 发布过多份安全研究：其中一些会先演示模型可能被怎样攻破，再讨论如何缓解。
越安全的系统，越需要说清楚自己在哪里会失守。安全声明的可信度，不来自”我什么都能防住”，而来自”我知道自己防不住什么”。
DeepSeek 随 Harness 一起发布的那篇近百页论文，讨论的正是一个叫 Cordis 的运行时框架：它不负责让模型更会回答问题，而是负责管理 Agent 系统里的插件、服务、依赖和卸载。
这篇论文给出了一组数学证明。读这组证明的正确姿势，恰恰是上面这种：先看它不保证什么。
它证明的不是”用了 Cordis 就不会出 bug”。更准确的说法是：在论文定义的模型和条件下，一组常见运行时错误被收进了框架边界——加载顺序、卸载清理、依赖失效、中间状态和最终一致性，不再完全交给每个插件作者临场处理。
这篇文章只看一个问题：这些证明在工程上到底买到了什么？
一、三条核心保证，每条都带条件
先把边界讲清楚。论文一共证明了五条性质，都是”模型内、有条件”的保证。其中三条对工程判断最有用。
第一条，时间可组合性：边界内的可逆副作用可以被恢复。
注意是边界内、通过上下文介导、并且提供了正确 inverse（逆操作，也就是撤销办法）的副作用，不是现实世界所有外部影响都能自动撤销。写出去的网络包、已经发出的消息、被外部进程改过的文件，都需要额外边界或补偿逻辑。
第二条，空间可组合性：依赖变化可以被生命周期规则吸收。
依赖没准备好时，消费者不该先运行；提供者退出时，消费者要先完成自己的清理，不能在清理阶段发现依赖已经被抽走。
第三条，合流性：在一组条件下，不同执行顺序最终可以收敛到等价状态。
条件同样重要：论文排除了失败组件，要求步骤相互独立、组件提供项完整，并且比较的是同一组编排输入下的静止状态。它不是说任意历史、任意外部副作用都无差别。
另外两条——状态转换不破坏结构约束（preservation，保持性）、系统不会永久卡在可推进的中间态（progress，进展性）——是这三条的结构地基，这里不展开。
所以，这篇论文真正给工程买到的不是”永不出错”，而是更清楚的边界：哪些错误应该由框架结构排除，哪些错误仍然属于外部世界、组件作者或产品实现。
二、HMR（热模块替换）的关键不是热，是复用已有生命周期边界
很多前端开发者熟悉 HMR：改一个模块，不重启整个应用，只替换受影响部分。Vite 官方文档会把能接受热更新的模块称为 HMR boundary（热替换边界）；Webpack 也要求开发者显式声明哪些模块可以接受热更新。它们都在解决同一个问题：变更传播到哪里可以停。
Cordis 论文在 HMR 上的重点不是”也能热更新”，而是：组件本身已经带着 effect 和 coeffect 边界，所以 Cordis HMR 可以复用组件生命周期边界，不要求开发者再额外标一个 acceptance boundary（接受边界）。
原因很简单。
一个组件的 Fiber——Cordis 里承载组件运行状态的最小单元——已经记录了它安装过哪些副作用，也记录了它依赖哪些上下文能力。
替换模块时，旧 Fiber 先卸载，撤回它通过上下文安装的 effect；新模块重新导入后，再用新 Fiber 安装一遍。影响范围由模块依赖图和组件条目共同计算，而不是靠开发者在业务代码里额外维护一套热更新边界。
论文把 Cordis HMR 写成三步：
- 模块分类：把变更模块和依赖图里的模块分成可热替换与需要重启的部分；
- 过期条目检测：找出哪些组件条目的依赖树碰到了已变更模块；
- 事务性重载：清缓存、重新导入、替换 Fiber；如果导入失败，就恢复缓存并用旧组件重建。
这三步带来的工程效果是：在论文描述的事务流程内，要么新代码完整生效，要么旧代码恢复，目标是不停在”半个模块新、半个模块旧”的状态。
这里仍然要降调：这是论文对 Cordis HMR 机制的描述，不等于所有应用状态都能被魔法保留。通过上下文注册、并且带有正确清理逻辑的 effect，可以按框架规则撤回；外部系统已经接收的输出、组件作者没有纳入上下文边界的状态，仍然要另行处理。
三、访问控制来自依赖声明，但沙箱仍需要外部边界
第二个工程收益，是权限视野变窄。
在 Cordis 里，组件不能直接从环境里抓能力：要访问什么，先声明依赖；没有声明的 key，组件在运行时是拿不到的，会直接报错。这在结构上接近 capability-based access control（基于能力的访问控制）：能力不是随手可拿的全局变量，而是通过声明和上下文中介拿到的引用。
但这里也不能写过头。
论文自己说得很清楚：Cordis 可以通过依赖声明和拦截（interception）约束组件访问什么；但对不可信代码，语言层面的访问控制不够，仍然需要外部沙箱，例如独立进程、独立运行时、容器或 WebAssembly。
也就是说，Cordis 不是替代沙箱，而是给沙箱提供一致的依赖入口：不可信组件跑在外部边界里，通过 bridge（桥接通道，负责在隔离边界两侧传递调用和数据）访问宿主提供的能力；宿主侧仍然可以用依赖声明和 interception 收窄它看到的能力。
这对 Agent Harness 很重要。工具、文件系统、模型适配器、子代理都不是普通函数调用，而是能力。能力越多，越需要先问清楚：这个组件声明了什么？运行时给了什么？访问时有没有被拦截？不可信代码是否在真正的隔离边界里？
一句话：框架管好框架内的事，组件作者管好自己声明的事，真实世界的事另找边界。
四、Koishi 案例说明的是“存在性”，不是排行榜
论文把 Koishi 作为案例研究：Koishi 是基于 Cordis 的开源聊天机器人框架。论文使用的口径是四年发展中积累了 4000 多个社区贡献插件。
发布前复核时，Koishi 官方 README 仍写”超过 3000 个官方和社区插件”；但官网插件市场索引已经能支撑 4000+ 这个量级。不同入口的统计口径不完全一样，但不影响”存在性案例”这个判断。
对读者更有用的读法是：论文用 Koishi 说明，Cordis 这套模型已经支撑过一个真实的开放插件生态，而不是只停在玩具原型。
论文自己也给了限制：这是单一生态、单一宿主语言里的观察性证据，不是和另一种架构做的受控实验。它说明的是 existence-and-adoption（存在且被采用）：这个模型至少可以在一个真实生态里被采用和运转；它没有量化证明开发效率提升多少，也没有证明所有场景都优于替代架构。
这个边界反而让文章更可信。
Koishi 案例里最值得保留的观察只有两个：
- 插件作者把副作用通过上下文介导的 effect 注册，并提供正确清理逻辑后，可以获得有序清理，不必再为这类 effect 额外手写一套分散的卸载路径；
- 独立作者写出来的插件，可以靠 coeffect 形成真实依赖拓扑；服务不可用或依赖变化时，由生命周期规则决定谁先停、谁后退、谁恢复。
这已经足够支撑本文判断：形式化保证的价值，不是让每个插件作者都懂形式化方法，而是把一类重复的生命周期胶水收进框架。
五、对 Agent Harness 的真正启发
读到这里，你可能有一个最直接的反应：我的 Agent 跑完一个任务就退出了，谁没事干把每个组件都拆下来换个更炫的型号再装回去？
如果你的 Agent 确实只跑一次就走，这篇论文对你没什么用。手写一个循环就够了。
但越来越多的 Agent Harness 正在变成长期运行的系统：持续管理工具、会话、权限、沙箱、子代理、模型适配器和 UI，甚至在运行中合成新工具、替换组件、调整自己的工作流——论文把这种 self-evolving（自我演化）的 Harness 写进了动机，因为这个方向会持续制造动态组合问题。
发布前复核 DSH 主仓时，也能看到这个方向已经不是几个示例插件的规模：按工作区包口径，它已经是 200 多个包的工程，其中近 50 个包带 DSH 自己的插件 / 组合声明。不过这个数字只说明产品内部已经高度插件化，不等同于 Koishi 那种开放社区插件市场规模。
一旦 Agent 需要在不停机的情况下换件，“拆得更碎”就不是过度工程，而是前提。
- 如果没有时间可组合性，每次换件都要担心清理遗漏。
- 如果没有空间可组合性，每次依赖变化都要手写通知和重试。
- 如果没有合流性这类条件性收敛结论，不同更新顺序就可能留下不同残影。
但也不要把结论写成”应用层不需要安全逻辑”。更稳的说法是：
好的 Harness 不会替你消灭所有风险，但会把风险分层。框架能排除的，放进框架；组件作者必须负责的，写进组件边界；外部世界无法撤销的，交给事务、补偿、隔离或人工确认。
这就是那组证明在工程上真正买到的东西。
评价一个 Agent 产品时，它让你多看一层：不只问模型有多强、工具有多少，还要问这套 Harness 的账清不清楚——谁安装了什么，谁依赖什么，谁能看到什么，谁退出时先清理什么。
形式化证明买不到万能安全；它买到的，是每一类风险都有清楚的边界和责任人。