§名词解释

插件（Component）是本文对论文中 Component 的称呼，用来定义依赖、供给和加载过程。
插件实例（Fiber）指插件进入运行时后产生的具体实例。
副作用（effect）指对共享环境的修改，本文沿用前端的译法，不译作“效应”。
撤销函数（inverse）比通常的清理函数（cleanup / disposer）多一层约定，执行后必须撤销对应操作对受管状态的修改。
上下文需求（coeffect）描述插件要求环境提供什么，例如文件系统或日志服务。

§它到底讲了什么

§我是不是看错论文了

前些日子 DeepSeek 发布了自己的 Agent Harness，社区里出现了很多介绍。我陆续看了一些，谈得最多的是它的核心理念 Everything is a Plugin，万物皆插件。模型、工具、记忆和会话都可以是插件，连 Agent Loop 本身也可以被替换。有些文章还深入源码，解释 DSH 怎样执行任务、调度工具。我最近也在学习 Agent Harness，很自然地想看看它的设计，以及它与 Claude Code、Pi 有什么不同。带着这个期待读完官方提供的论文，我的第一反应却是，我是不是看错论文了？

我想了解的任务规划、工具调度和上下文组织，在论文里都没有展开。读到这时才发现，我把社区对 DSH 整体架构的讨论，当成了论文要解释的内容。
DSH 是一个 Agent Harness，Cordis 是它底层的插件运行时，论文研究的是后者。它讨论的问题更为通用。一个允许插件动态安装、卸载和替换的系统，怎样才能在变化中保持正确？

这又让我有了一个疑问，为什么一个 Agent Harness 需要一篇讨论插件运行时的论文？

§自演化的 Harness 意味着什么

论文所说的“自演化 Harness”，究竟在演化什么？模型之外的工具、记忆、存储和调度，共同组成了 Agent 赖以工作的 Harness。模型可以在其中选择工具、读写记忆，但使用这些能力，与修改承载它们的系统，是两件事。

论文设想，未来的 Agent 能够修改自己的 Harness。要让这种修改成为可能，工具、模型服务乃至核心循环，都需要成为 Agent 可以识别和操作的对象。那么 Harness 首先得有一套表达自身结构的方式。
每个部分负责什么，提供哪些能力，又需要哪些支持，这些信息原本可能分散在代码各处。把它们纳入统一的运行时抽象，Harness 才能把自身交给程序管理，这样也才能变成 Agent 有可能修改的对象。
沿着这个要求，“万物皆插件”就容易理解了。DSH 用同一种插件模型描述工具、模型服务和核心循环，让修改 Harness 有了明确的操作单元。

§所谓“万物皆插件”

前端开发者对这个理念应该不陌生。Webpack 就是一个高度插件化的系统，官方文档把 Plugin 称为整个系统的骨架，它自身也建立在用户使用的那套插件系统之上。不过，高度插件化与运行中安全地改变插件组合，仍然是两件事。
Webpack 的插件把回调注册到 Hook 上，再在相应的编译阶段执行。常规配置下，同一个 Compiler 使用的插件集合通常保持稳定，执行时再由 Hook 调用相应回调。模型从已注册的工具中选择一项，也只是一次能力调用，未必改变 Harness 的结构。现有 Agent 也有动态扩展能力，例如 MCP 支持查询工具列表并通知列表变化。所以，只看“能否动态增加工具”，还不足以说明 Cordis 要解决的问题。

Cordis 关心的是插件组合在运行中变化时的正确性。插件可以进入、退出和被替换，运行时要管理系统里有哪些插件，以及它们之间怎样绑定依赖。“动态调用”与“动态组合”的区别就在这里，代码有没有提前加载进内存，并不能说明这种区别。

§“万物皆插件”之后

把能力都变成插件，系统便有了替换它们的操作单元，从程序系统的角度看，每一次自我修改都是一次动态组合。假设一个 Agent 原本通过本地文件系统插件读写工作区，现在准备改用远端 Code Server 环境提供的文件服务。新代码加载以后，旧插件仍可能持有文件句柄、目录监听器和本地缓存；远端实现则需要网络传输与鉴权服务，还要向上层提供相同的读写和监听接口。只把 Context 中的文件服务改指向新实现，正在使用旧实现的插件就可能陷入不一致状态。
系统需要知道旧插件改变过什么，并在它离开时按顺序撤销这些改变。系统也需要知道哪些插件依赖文件服务，它们当前绑定哪个实现，以及这次替换会影响谁。依赖出现、消失或换了提供方，相关插件就需要相应地退出和重新加载。
工程上常用重启来处理这类问题。例如，VS Code 的扩展管理文档说明，卸载、禁用或更新扩展后，会提示重启 Extension Host。进程结束时，操作系统回收它持有的内存、句柄等资源；重新启动后，依赖关系按配置建立。这种办法简单，却也意味着进程内未持久化的执行状态会丢失，需要保存和恢复。Cordis 要支持运行中的动态组合，就得让系统在不重启的情况下安全地更换服务。

论文要回答的，正是怎样完成一次局部替换，而不必让整个系统重新开始。

§从动态替换反推 Cordis

文件服务替换期间，我们希望会话继续运行，编辑、搜索和索引插件仍通过同一套文件接口工作。这要求旧实现的资源得到清理，相关使用方按顺序退出并重新绑定，无关插件则继续运行。已经完成的业务写入，也不应因为文件服务卸载而被一并回滚。
这些要求可以分成两个方向。时间可组合性（temporal composability）关心怎样撤回插件对受管状态的副作用；空间可组合性（spatial composability）关心依赖怎样组合、隔离，并在变化时协调。先看撤销。

§怎样只撤销旧插件

在“万物皆插件”的系统里，插件也是卸载和替换的单位。运行时要拿掉其中一个，就必须分清它和其他插件分别改变了什么。我们希望只撤销目标插件的修改，让其他插件保留当前状态；整个系统倒退到历史快照，显然不符合这个要求。
首先要明确修改的归属。那些不与外界交互、也不被外界持有的局部对象，随插件一起丢弃即可。需要单独处理的是越过插件边界的修改，例如注册目录监听、占用文件句柄，以及向 Context 提供服务。它们必须能归到对应的插件实例上。
知道“是谁做的”，还不等于可以安全地撤销。两个插件可能共同使用一个服务，如果 A 的清理会破坏 B 的结果，就不能把 A 当成独立的撤销单位。我们还需要独立性，让一方的执行和撤销不改变另一方的行为。确实有先后依赖的部分，则要把顺序表达出来。

工具注册表可以说明这个区别。A 用唯一名称注册 format_document，B 注册 search_symbol，卸载时各自只删除自己的条目。如果表只按名称查询，不把插入顺序作为公开语义，移除 A 就不影响 B。这份独立性来自注册表的接口约定，单纯把 A、B 写进两个插件文件，并不能得到同样的保证。
一旦允许同名覆盖，或者清理时直接清空整张表，这个约定就被破坏了。两个插件即使都写了清理函数，也未必能够独立卸载。

明确了归属和独立性，就可以缩小视角，研究一个插件本身。插件加载时，对外产生的是一组副作用；卸载时，需要撤回这一整组修改。“撤回”不必逐字节还原。监听器关闭以后，操作系统的内部计数器可能变了；内存释放以后，堆的布局也不会恢复原样。在其他插件的修改保持不变时，只要通过模型允许的操作，无法区分“目标插件已被卸载”和“它从未加入”的受管状态，就足以认为修改已经撤回。这在论文里叫观察等价（observational equivalence）。它允许忽略内部实现细节，但不能把接口仍能观察到的差别也当作相同。

接下来，要找到完整撤销这组副作用的办法。运行时面对任意 JavaScript 代码，无法等到卸载时再猜测它改过什么、该怎样恢复。掌握这些信息的是执行操作的代码，所以撤销方法必须在副作用发生时就交出来，由上层统一管理。
顺着资源管理的工程直觉，这些撤销函数应该归入当前插件实例，并按执行的反序调用。后创建的资源往往依赖先创建的资源，打开连接以后再建立监听，退出时就先移除监听，再关闭连接。每取得一个新的撤销函数，就把它接到已有清理逻辑的前面，自然得到后进先出的撤销累加器（accumulator）。
这样，插件内部即使分成多个辅助函数，也不需要在卸载回调里重新罗列所有资源。每一处取得资源的代码交出自己的撤销方法，外层只负责组合和调度。

把这个要求写成 API，就是执行操作的代码返回清理方法，把何时清理的控制权交给框架。前端开发者很容易想到熟悉的useEffect范式。

TypeScript
1
2
3
4
useEffect(() => {
  const watcher = fileService.watch(workspace, onChange)
  return () => watcher.close()
}, [fileService, workspace])

Cordis 的ctx.effect也采用类似的形式。

TypeScript
1
2
3
4
ctx.effect(() => {
  const watcher = localFs.watch(workspace, onChange)
  return () => watcher.close()
})

React 的useEffect 会在规定时机调用清理函数，也要求清理逻辑正确地撤销 setup 的工作。论文把这项要求作为组合论证的前提，返回的函数必须撤销对应修改，后面的推导才能成立。两段 API 都把清理交给框架调度；清理函数是否正确，仍需由实现来保证，Cordis 也不会自动证明这一点。

从“怎样单独卸载插件”往下拆解，我们得到了最小的操作单元，一次归属明确、同时交出撤销方法的副作用。怎样把这些单元组合回可撤销的插件，留到后面的论文论证部分。

§怎样只让相关插件跟着变化

副作用上的独立性允许我们保留不受影响的插件，服务之间的依赖则决定谁需要跟着变化。文件服务被替换，索引插件仍然需要调整；与文件服务无关的插件，则不应因此退出。
要确定这个范围，运行时需要一张随当前绑定更新的依赖图。不过，整张图不必由某个插件集中描述。使用方声明需要什么，供给方登记能提供什么，运行时把两端连接起来，就能从局部关系得到整体关系，也能反向查出谁依赖谁。
视角由此缩小到一个插件对环境的要求。远端文件服务需要网络和鉴权，索引插件需要文件读写和监听。这就是论文所说的上下文需求。
怎样把需求表达给系统，已有很多工程方案。静态import、插件的依赖清单、DI 的装饰器，都能表达某一层次的依赖；响应式系统还会从实际读取中被动收集关系。论文选定的是执行前显式声明的模型，没有比较这些方案各自的优劣。

索引插件需要文件系统能力。如果它在声明里写死某个本地实现，替换服务时就得连使用方代码一起修改。因此，需要为这项稳定的需求取一个名称，也就是依赖键（dependency key）。使用方声明需要fs，供给方登记符合接口约定的实现，运行时决定这次绑定到谁。
DSH 使用的 Cordis 通过inject表达这类声明。下面沿用假设的fs服务，省略类型扩充和索引实现，API 形式见官方服务与依赖文档：

TypeScript
1
2
3
4
5
6
7
8
import type { Context } from '@deepseek-ai/cordis'
export const inject = ['fs']
export function apply(ctx: Context) {
  const fs = ctx.fs
  // 使用本次绑定的文件服务建立索引。
}

供给方则通过 ctx.provide 登记已经创建好的服务：

TypeScript
1
ctx.provide('fs', remoteFs)

inject表达需求，ctx.provide登记供给，ctx.fs取得本次运行所绑定的服务。运行时不必理解索引算法，只要把声明和实际绑定联系起来，就能还原当前的依赖关系。
关系变化后怎样传播消息，也符合熟悉的发布订阅思路。依赖声明可以看作订阅依据。服务供给或可用状态发生变化时，运行时通过通知机制重新检查相关插件的依赖，判断是否需要调整它们的运行状态。

空间方向的要求也由此落到了局部。从“怎样找到受影响的插件”，到一个插件需要什么，再到需求与具体供给的绑定。管理好这些关系，运行时就有了确定变化传播范围的依据。

§两个方向在 Context 汇合

依赖关系确定了文件服务退出时会影响谁，撤销机制让这些插件能够清理自己留下的修改。索引插件先移除旧文件服务上的监听，旧服务随后退出；新服务准备好以后，索引插件再建立监听和索引。无关插件继续运行，有依赖的插件按顺序退出和重新进入。把这些加载、运行和清理规则组织起来，就得到了插件生命周期。

Cordis 用 Context 同时承载两类信息。副作用经它追踪，撤销方法归到相应的插件实例；服务也经它提供和取得，依赖绑定因而能被运行时管理。提供服务本身又是一项副作用，供给方退出时，自己加入的绑定也要撤回。时间与空间的管理在这里联系起来。
这就是论文的上下文范式（context paradigm）。Context 把“改过什么”和“依赖什么”放进同一套运行时结构。这些保证以插件遵守约定为前提，Context 自身不提供安全沙箱隔离；绕开它修改共享状态，就不能直接套用论文的结论。

从系统需求一路向下，插件最终被拆成了可以管理的修改和依赖。运行时据此组织插件，无须理解它们的全部业务逻辑。

§论文怎样把结论证明回来

从系统需求出发，自上而下地寻找机制，最后落到具体 API，是一种常见的工程思路。论文从另一端开始。它先规定最小的副作用和依赖操作应当满足什么条件，再把局部保证组合到插件，最后通过生命周期规则推导整个动态系统的性质。繁复的数学过程可以暂且跳过，沿着这几层组合，就能看清结论是怎样得到的。

§从单个副作用到单个插件

一次副作用和它返回的撤销函数，构成了最小的组合单元。执行它，状态从$\gamma$变成$\delta$，同时得到撤销函数$g$；执行$g$，则应当撤回这次改变。这份撤销约定是 Definition 8 对每个单元提出的前提。沿用前文的观察等价口径，可以把它简写为：

$$\begin{array}{rl}e(\gamma )& =(\delta ,g)\\ g(\delta )& \simeq \gamma \end{array}$$

把这样的两个单元 A、B 依次组合起来，得到的仍然可以当作一个副作用。它也会改变状态并返回自己的撤销函数，只不过这个函数内部先撤销 B，再撤销 A。只要 A、B 各自满足撤销约定，组合后的单元就仍然满足同一份约定。这正是 Theorem 11 所说的Witnessing survives effect composition，撤销正确性的保证在组合以后仍然成立。
组合后的接口和约定都没有改变，因此 A、B 组成的整体可以继续与 C 组合，再作为一个单元参与下一次组合。每一步只需依据上一层已经成立的保证，无须重新展开内部实现。

组合也可以逐步进行。插件每完成一步，运行时就把新的撤销函数接进累加器。此时决定退出，便反序撤回已经完成的部分；继续执行，则得到一段更长、仍可撤销的序列。后面的步骤先被撤回，每个撤销函数就能重新遇到自己那次正向操作留下的状态。Theorem 16 保证了这种逐步恢复，也保证了中间状态始终满足正确性不变量。
论文把这串逐步产生副作用的过程表示为副作用迭代器（effect iterator）。每一步交出新状态、撤销函数和可能存在的下一步，运行时据此继续执行和积累撤销。Definition 17–18 给出了它的形式化定义。

把这串副作用作为插件的加载过程，插件就继承了整个序列的撤销能力。加载时推进迭代器，卸载时执行已经累计的撤销函数。从一次操作到一段过程，再到一个插件，恢复依赖的始终是同一份约定。这便是论文在第 3.1.3 节末尾得到的局部时间可组合性。
再给插件配上依赖声明，这段副作用序列就有了启停条件。依赖全部满足后才能开始执行；从满足变为不满足时，则触发撤销。Definition 21–22 定义了这份声明及其对环境变化的响应，得到局部空间可组合性。“局部”意味着这里暂时只看单个插件自身的副作用和依赖。

§从单个插件到多个插件

单个插件能够完整撤销，还不足以保证多个插件可以安全共存。卸载 A 时，应该只撤销 A 的副作用，并保留 B 的修改。这就需要它们的操作相互独立，可以分两种情况来看。

操作不同依赖键时，独立性来自访问范围的隔离。Definition 29 要求，每个能力操作及其撤销只访问对应键所承载的状态。访问范围确实分开，不同键上的操作就互不干扰，这就是 Theorem 45 的结论。只把名字分开还不够，两个服务如果在背后修改同一个文件，就不能因为依赖键不同而认为它们独立。
操作同一个依赖键时，则要由服务提供方通过 API 保证独立性，这是 Definition 46 赋予能力提供方的责任。前面的工具注册表只有在各自删除对应条目、注册顺序也不影响对外结果时，才能让 A 卸载后保留 B 的工具。服务返回的撤销函数如果会清空整张表，使用方按规矩调用它，也无法保证互不干扰。
独立性同时约束操作、撤销及它们产生的结果，完整条件见 Definition 42 与 Definition 44。服务提供方本身也可能是插件，所以这里仍然依赖编写者履行约定。提供方要正确实现 API 和撤销逻辑，使用方要遵守依赖声明，不绕过 Context 操作共享状态。运行时负责管理这些操作，并不会自动验证它们是否独立、是否可撤销。

两个插件各自执行的，是一串经过 Context 的能力操作。有了上述局部保证，就能依据双方提供和使用的键，进一步判断整个副作用迭代器是否独立。Theorem 47 的条件与结论可以概括为：

如果双方提供的键都不在对方涉及的键范围内，而且共同操作的每个键都满足可交换性要求，那么这两个经 Context 中介的副作用迭代器相互独立。

能力接口满足局部约定后，独立性的保证便能继续传递到插件。判断两个插件能否独立组合，可以依据它们的供给和依赖声明，无须重新检查里面的全部业务代码。
满足独立性条件的单元，撤销时不必共用一条全局的后进先出顺序。Theorem 43 在副作用函数这一层给出的结论可以转述为：

一组各自可撤销、两两独立的副作用依次执行后，以任意排列执行本次运行产生的全部撤销函数，都能恢复到初始状态。

证明中的关键，是先撤销其中任意一步，得到的状态就如同原序列没有执行过这一步，其他步骤已经交出的撤销函数仍然有效。撤销一项之后，剩下的组合继续成立，于是可以依次撤销其余各项。插件内部有先后依赖的步骤，仍然需要反序撤销。
插件之间也有不能独立拆开的关系。索引插件要等文件服务准备好才能加载，也必须在文件服务退出前完成清理。这种顺序通过显式依赖保留下来。第 3.4.2 节末尾 由此分开两类关系。能够换序的操作交给独立性处理；必须排序的操作，在插件内部交给撤销累加器，在插件之间交给依赖拓扑。
现在，插件带着自己的撤销保证，也带着与其他插件组合时需要遵守的边界。把它们放进生命周期规则，接下来就要证明，加载与卸载交错进行时，这些保证仍然成立。

§把插件放进生命周期

插件定义描述需求、供给和加载过程，插件实例持有实际绑定、撤销累加器与当前状态。第四章用一组带前置条件的转移规则管理实例，主要状态如下。

运行时根据当前依赖关系，为实例计算“现在应该绑定谁”，论文称之为目标依赖视图（target view）。依赖完整后，实例提交这份解析结果并开始加载。实际采用的已提交依赖视图（committed view），在本轮加载、运行和清理期间保持稳定。

依赖变化时，索引插件先借助旧文件服务完成清理，再用新绑定开始下一轮。这样就不会把旧引用直接替换掉，让尚未完成的工作混用新旧服务。加载中途发生变化，也会转入卸载，撤回已经完成的部分。
供给方准备好以后，使用方才能加载；使用方清理结束以后，供给方才能完成卸载。绑定在清理期间保持稳定，正是为了让这个顺序可以执行。

论文还把退役（retire）与移除分开。退役会阻止实例开启新的生命周期，实例本身仍留在注册表里。清理和子实例处理等工作完成后，才真正移除它，避免把退出过程仍然需要的运行时对象提前删掉。
论文第五章的配置协调（configuration reconciliation）和 HMR 也沿用这些规则。配置描述目标插件树，加载器用稳定 id 比较目标与现状，把差异转成插入、退役和重新实例化。代码更新时，受影响的旧实例完成退出，再由新代码创建实例。加载器负责表达变化，生命周期规则负责有序地完成变化。

§最终得到哪些系统性质

首先，变化过程中的插件图本身要始终有效。不能留下父实例已被删除的子实例，也不能让仍需清理的插件指向已经消失的服务提供方。只要初始状态符合结构约束，每一步合法转移以后，这些约束就仍然成立。这是 Theorem 64 的保持性（preservation），也是后续结论能够继续推导的基础。

在这张始终有效的依赖图上，撤销保证可以延伸到交错执行的整个过程。旧文件服务卸载完成后，它对受管共享状态的副作用被撤销，其他插件独立产生的修改仍然保留。这就是 Theorem 68 的精确恢复性（recovery exactness）。它把前面“一串副作用能够反序撤回”的结论，推进到了有其他插件穿插工作的情形。

对于需要一起变化的插件，Theorem 70 保证供给方与使用方的先后顺序，Theorem 71 保证加载沿同一份依赖绑定完成，或者转入卸载并恢复。索引插件因此能在旧服务仍可用时清理监听，再等新服务就绪后重新加载。“谁先退出”和“退出时仍使用谁”都受到约束，空间方向的依赖关系才有了系统层面的保证。

有序等待，还需要保证等待能够结束。Theorem 73 给出了进展性（progress）。满足后面说明的无环、有界等条件后，只要还有待处理的生命周期工作，就有规则能够推进；继续执行，最终会到达静止状态（quiescence），没有待执行的生命周期步骤。

不同调度能否得到相同结果，则由 Theorem 80 的合流性（confluence）回答。满足下一节列出的前提后，其结论可以转述为：

从相同初始状态出发，执行相同的编排步骤并保持它们的顺序，不同合法调度到达的静止状态观察等价，允许对无关的实例名称作一致的重命名。

动态运行由此可以与静态组装联系起来。满足定理前提时，相同编排输入下的受管终态，都与按最终有效插件集合及其依赖关系组装出的规范状态观察等价。不同执行过程能够得到等价的终态，中间经历的步骤仍然可以不同。

§这些结论成立到哪里

撤销和独立性必须由插件实现来兑现，受这些保证覆盖的共享交互也必须经过 Context。运行时按规则组织操作，任意插件代码是否符合约定，仍需另行验证。
进展性要求依赖优先关系无环、整个过程中出现过的实例总量有限、副作用迭代有界，并且编排输入最终停止变化。无限创建实例、某一步永远不返回、配置持续变化，都超出了这个终止保证。到达静止状态也允许有插件因缺少依赖而保持未激活。
合流性还要求插件激活完成时，实际提供声明中的全部键，即 Definition 76 的完全履行供给声明。失败扩展明确将失败情形排除在合流结论之外。已完成部分可以按约定撤销，也不能推出成功与失败两条轨迹会得到相同终态。

观察等价比较的范围同样有限。文件服务卸载，不会让已经发送的请求消失；两次调度终态等价，也不意味着中间发送消息的顺序相同。论文区分了受管状态与沿途的外部发送。可撤销的资源取得与已经发生的业务行为，需要分别看待，不能把这里的保证泛化成整个业务过程都可回滚。

§从前端视角对它的评价

§熟悉的机制与不那么显然的保证

从前端经验看，我最初的感受没有变。副作用与清理成对、资源交给上层管理、显式依赖、变化通知、根据目标调整实例状态，都是熟悉的工程做法。只看“万物皆插件”和一个形似useEffect的 API，很难让我觉得出现了全新的架构思想。
熟悉这些机制，却不等于知道它们组合后在什么条件下仍然正确。先移除监听再关闭连接，几乎是资源管理的直觉。允许其他插件在中间工作，还要单独卸载其中一项，一条反序清理链就不够了。我们还得说明哪些操作独立、哪些必须排序，以及依赖改变时谁仍有权使用旧服务。论文把这些原本需要分别考虑的问题，组织成了一条可以检查的论证。

形式化的价值就在这里。工程上觉得“应该能清理干净”“这两个插件应该互不影响”，论文则要求说明这些判断成立的前提，再据此推导组合后的结论。撤销方法和依赖关系也被保存在运行时里，成为实际调度的依据。论文称这种处理为具象化（reification）。放到工程里看，就是让程序直接持有和管理这些原本需要人手协调的信息。

我更愿意把这里的创新概括为整套动态组合机制的组织与形式化。它说明了熟悉的工程做法怎样配合工作，以及哪些约定决定了保证的范围。对我来说，最值得学习的是接口设计与系统保证之间的这层联系。

§保证背后的工程化问题

这套模型让局部保证有了复用的依据。能力提供方封装资源取得、撤销和独立性，使用方遵守声明，运行时安排生命周期。新增插件时，可以沿这些接口约定推理，无须重新理解整个系统的实现。
前提是提供方把约定做对。它不能在 API 内部修改归属不明的共享状态，也不能交出会破坏其他使用方的撤销函数。普通业务插件未必需要自己实现所有清理机制，提供共享能力的那一层却必须承担这份责任。经过 Context 的代码，仍然可能写错。

现实中的故障也提醒人注意这段距离。DSH 的早期预览版讨论中，有用户报告第三方插件的语法错误使整个 profile 无法启动，也有人报告安装插件后加载了两份工具运行时，导致会话中的工具调用失败。这些是特定版本和环境下的用户报告，无法据此判断定理有误，也不足以把问题归咎于某一方。它们说明，模块加载、依赖版本和故障处理仍有各自的工程问题，一份组合性证明不会自动解决这些问题。

从模型走到可靠的软件，还需要插件作者和宿主维护者共同落实这些前提。依赖声明、资源归属或撤销逻辑出了偏差，实现就可能超出定理覆盖的范围。形式化让这份责任更明确，也让我们知道应该检查什么。

§这篇论文给我的启发

我原本想看 DSH 怎样组织 Agent，结果读了一篇插件运行时的论文，倒也没有白跑一趟。最有收获的是看到作者怎样围绕动态组合，把熟悉的工程手段组织成系统，再逐层论证它能提供什么保证。
我平时更习惯从眼前的问题出发。资源需要清理，就找清理机制；依赖需要管理，就找依赖注入。至于这些办法组合后，整个系统还能保证什么，我很少继续往下想。所以刚读论文时，很容易觉得“这不就是那些工程做法吗”。这次先从插件替换的需求往下梳理，再沿论文的论证往上走，才注意到自己平时略过了多少条件。
以后做类似设计，我想多问一步。除了知道监听怎样清理、依赖怎样声明，还要知道另一项功能同时变化时，这些约定能否继续成立。局部的办法怎样成为整个系统的保证，这是这次阅读留给我最有用的问题。