运行期不变量

只有拥有**两个可独立观察、可能分叉的运行期事实**的包，才把自己的关系检查注册进共享注册表； 没有这种关系的包不创建 `Invariant.cs`，也不挂 installer。违约时抛出带包名归属的错误， 让"谁的契约被谁违反了"在运行期就能定位，而不是等到数据已经写坏。 对应实现：src/Tether.Invariants/。设计时还有一个离线的对照面： 形式化建模用 Lean 4 对核心语义穷举交错并产出反例报告。

为什么单独一个包

产品层的包彼此不可见，只通过服务接口相遇。这带来一个问题：跨包的时序契约没有天然的归属地。比如”turn/end 不能在还有 step 打开时出现”——这是会话包的契约，但违反它的往往是 Agent 循环包。

做法是把检查的注册集中，检查的所有权留在各包：

public sealed class SessionInvariantPlugin : Plugin
{
    public override IReadOnlyList<Type> Inject { get; } = [typeof(IInvariantRegistry)];

    protected override void Apply(Context context)
    {
        var registry = context.Require<IInvariantRegistry>();
        // 注册即回收：插件卸载时检查一并摘除
        context.Effect(registry.Register("Tether.Core.Session", Install).DisposeAsync);
    }

    private static void Install(Context context, InvariantFail fail)
    {
        // context 是本注册独占的子上下文
        // fail 已绑定包名，调用即抛 InvariantError
    }
}

因此 Tether.Invariants 在依赖图里是按需引用的横切关注点：只有发布真实 runtime invariant 的包引用它；注册表本身只依赖 Cordis。

两个委托

// 抛出带包名归属的违约
public delegate void InvariantFail(string message);

// 把一个包的检查装进该注册独占的子上下文
public delegate void InvariantInstaller(Context context, InvariantFail fail);

InvariantFail 收到的消息不带前缀，最终异常消息由注册表拼成 invariant violated by "包名": 消息。

注册表

IAsyncDisposable Register(string packageName, InvariantInstaller installer);

几条硬性行为：

• 包名必须非空白，且不能包含任何空白字符，否则抛 ArgumentException；
• 同一个包名不能重复注册，重复抛 InvalidOperationException；
• 包名即使因筛选而未激活，也仍然占位——避免”以为注册上了其实被同名挤掉”；
• 安装器在一个由 _owner.Fork() 产生的子上下文里运行，注册的一切随该子上下文回收；
• 安装器自身抛异常时，注册表会回滚包名占位并回收子上下文，再把异常抛出。

子上下文隔离的意义是：检查逻辑自己也遵守注册即回收纪律，取消一个包的检查不会残留监听器。

启用与筛选

InvariantRegistryOptions 有三个选项：

筛选顺序是：先看全局开关，再看白名单（非空时必须命中其一），最后看黑名单（命中即排除）。也就是说黑名单优先级高于白名单。

正则在构造时就编译并校验，三种情况直接抛 ArgumentException：条目为空或有首尾空白、同一列表内有重复正则、正则本身非法。这样配置错误在装配阶段暴露，而不是等到某次检查该跑却没跑。

违约错误

public sealed class InvariantError : Exception
{
    public const string Code = "INVARIANT";
    public string PackageName { get; }
}

Code 是稳定的机器可读码，PackageName 指出契约的所有者。宿主可以据此把违约与普通异常分开上报——Tether.Headless 就是这么做的：

error = ex is InvariantError invariant
    ? $"{invariant.GetType().Name}:{invariant.PackageName}:{InvariantError.Code}:{ex.Message}"
    : $"{ex.GetType().Name}:{ex.Message}";

实例：会话括号结构校验

Tether.Core.Session 注册的检查是理解这套机制最好的例子。它订阅每一条提交的会话事件，维护一份轻量轨迹（最后序列号、当前打开的 turn 与 step、本 step 内未配对的调用 id），并断言：

这些正是会话与事件溯源里描述的括号结构与Agent 生命周期里 turn/step 编号规则的可执行版本——文档写的约定，这里是运行期强制。

实例：Interaction 的 durable companions

Tether.Interaction 把 approval 与 direct command 的审计约束注册到同一个 inspector registry， 所以 live append 在 commit 前失败，cold replay 也不会因“当前 service 通常会配对”而跳过历史校验。

这些事件都是 log-only；检查 durable closure 不会把 command 或 approval 伪装成模型可见 user/message，也不会替 direct command 打开 turn。

新增 invariant 的审查标准

提交 runtime invariant 前必须同时说明六件事：

1. owner 关系：Register 的 package name 必须就是源码程序集，失败能归到拥有该契约的包；
2. 两侧 observation：明确列出两个来自真实运行路径、可以分别观察的事实；
3. 可能漂移原因：说明两侧为何会因并发、生命周期、不同 producer 或 replay 而独立分叉；
4. 检查时机与 failure routing：写清 pre-commit、awaited policy 或 contained notification，以及失败去向；
5. disposer：registry registration 和内部 listener/provider subscription 都必须挂在 child EffectScope；
6. negative test：必须构造一次真实可达的分叉并断言 owning package。

以下都不是有效 runtime invariant：empty installer、只检查 service presence、plugin metadata、effect 数量或固定示例。 这些约束应留在依赖图、插件框架或普通 unit/acceptance test；没有独立关系的包不建 companion 文件。

已注册检查的包

Tether.Invariants 自己只提供 IInvariantRegistry 与 registry，不注册产品关系，也不需要空 companion。

下一步