Harness as a Language×Bounded Loops：Agent 脚手架的语言化与可验证化 精读

论文 A 链接：Harness as a Language: A Minimalist Agent Framework With Maximal Expressivity 论文 B 链接：Bounded Loops: Pre-Run Spend Bounds, Proved Termination, and Verified Completion for Agent Harnesses 代码仓库 A：jaz-lang/jaz、jaz-lang/jaz-evals 代码仓库 B：qualixar/bounded-loops（Apache-2.0） 发表时间：2026年9月 机构 A：MIT CSAIL（Omar Khattab、Armando Solar-Lezama 组）+ 独立研究者 机构 B：Qualixar / Independent Researcher（印度）

一、论文背景

1.1 什么是 agent harness，它为什么突然变得重要

如果你用过任何 LLM agent 产品——写代码的 Claude Code、查资料的深度研究、跑任务的 OpenHands——你接触到的其实是一个「三明治」结构：中间是 LLM 本体，外面两层是agent harness（脚手架）：上层负责把用户请求组织成提示、管理工具调用、决定循环什么时候停；下层负责把模型输出接到真实环境（文件系统、API、浏览器）。

一个直观的类比：LLM 像一位能力极强但不稳定的临时工，harness 就是他的岗位说明书、工位布置和考勤制度。临时工能不能干好活，很大程度不取决于他自己，而取决于岗位是怎么设计的。

harness 之所以现在成为研究焦点，是因为两个压力同时到来：

1. 能力压力。模型本身越来越强，很多以前需要精心设计的「外挂系统」（记忆系统、自我改进循环、任务分解器）正在被证明可以由模型自己完成——前提是 harness 给它足够的表达自由。这引出了论文 A 的问题：harness 到底需要多少「设计」？
2. 信任压力。agent 跑一千步、花几十美元，如果它说「我做完了」，你信吗？它说「我花了 20 美元」，你怎么在开跑前知道？2026 年一项针对 70 个开源 agent 项目的调查（论文 B 引用的 Graph Harness proposal，Wei 2026）显示 42 个仍在用无结构 agent loop——完成与否完全取决于模型自己说。这引出了论文 B 的问题：harness 的哪些性质可以证明而不是期望？

两篇论文恰好从这两个方向同时出发，结论却指向同一个地方：harness 不该是一堆工程惯例的堆叠，而应该是一个有精确语义的数学对象。

1.2 概念阶梯：从 agent loop 到 CodeAct 到 RLM

要读懂论文 A，需要先理清 agent 执行范式的演进：

• ReAct（2022）：模型每步输出一个动作（调用某个工具），观察结果，再决定下一步。动作是「硬编码」的——工具的输入输出格式都是定死的。类比：给临时工一张固定格式的工单，每做一步填一格。
• CodeAct（2024）：把模型放进一个代码环境（REPL），让它直接写 Python 代码来编排工具调用。循环、条件、变量都是免费的。类比：给临时工一台电脑，让他自己写脚本。
• RLM 递归语言模型（2025）：在 CodeAct 基础上允许 agent 递归调用自身作为子 agent，且子 agent 的输出作为Python 变量（而非文本）返回给父 agent。论文 A 的多位作者正是 RLM 的作者，JAZ 是 RLM 的直接延伸。

每一步演进都在增加表达力，而表达力的增长不断解锁新能力。但截至论文 A 之前，记忆和自我改进这两类能力仍被普遍认为需要专用外挂系统——Letta（MemGPT）用分层记忆管理做长程回忆，ACE 用 Generator-Reflector-Curator 三角色循环做持续自我改进。论文 A 的核心主张就是挑战这个共识。

1.3 概念阶梯：从声明边界到验证式 harness

论文 B 的背景则来自另一个传统——形式化验证：

• Durable execution：Temporal 等平台让工作流在进程崩溃后可恢复，并提供超时与重试上限。但完成条件写在工作流代码里，检查器和工作代码在同一仓库、同一部署里，「检查器独立于工作」只是团队的纪律约定，不是系统强制的性质。
• 运行时保证（Runtime Assurance, RTA）：航空领域的 Simplex 架构让一个「不可信的高级控制器」在运行时被一个「可验证的回退控制器」监视，违规即接管。NASA 已将其形式化到 PVS 定理证明器中。论文 B 的 worker/gate 分离与此同构。
• 工作流网（Workflow Nets）与重置弧：van der Aalst 的 Petri 网工作流验证理论证明了带重置弧的网络其可达性不可判定但终止性可判定——论文 B 的修复边（repair edge）正是一种重置弧，它站在了这条可判定性边界上。
• 变异测试（Mutation Testing）：给程序注入机械故障看测试套件能否发现，是度量「测试本身质量」的标准手段。论文 B 把它改造成了度量「验证器本身质量」的仪器。

论文 B 做的事，是把这两个传统焊在一起：harness 不仅要声明预算，还要在运行前证明这预算必然被遵守；不仅要有完成判定，还要让这判定的可靠性本身可测量。

二、论文定位和关联工作

2.1 论文 A 的定位：harness 极简主义路线的收官

围绕「harness 该多厚」这个问题，领域里存在清晰的谱系：

关键定位：论文 A 不是又一个框架，而是一个表达力定理加实证。它形式化定义了 invoke 原语（附录给出了 λ 演算扩充的严格语法与操作语义），论证从 ReAct 循环到树搜索到递归子 agent 都是这个原语的特例，然后用两组受控实验证明：这个理论上极小的内核，在实践上足以击败两个成熟的专用 harness。

2.2 论文 B 的定位：验证传统向 agent 领域的移植

关键定位：论文 B 自称是对 Graph Harness 工作的延伸而非纠错——它跨过了后者明确排除的修复边构造，付出的代价是上界多一个 (R+1) 因子；同时它造出了后者只能假设的量：手写验证器的实测误接受率。

2.3 两篇论文的互补关系

一句话概括：论文 A 回答「harness 最小可以是多少」，论文 B 回答「harness 的承诺最大可以证明到多少」。A 把 harness 压缩成一个语言原语，B 给这个原语组成的循环装上类型化的预算与静态验证器。A 的世界是动态的、生成式的——agent 在运行时写自己的控制流；B 的世界是静态的、验证式的——人在运行前读清单。两者拼起来，正是「harness 从工程偶然走向数学对象」的一体两面。

三、问题定义

3.1 论文 A：把「harness 该有什么能力」抽象为「语言该有什么原语」

论文 A 的核心洞察是一个深层的结构相似性：

agent harness 设计 ≈ 编程语言设计

具体对应关系：

形式化定义（Definition 1）：给任意图灵完备语言加一个原语 invoke(x1 := e1, ..., xk := ek)，其语义是：把所有输入序列化为字符串提示交给 LLM，LLM 生成的代码（在同一种扩充语言中）成为该函数的函数体，随即执行。由于语言本身含 invoke，模型写的代码可以递归地包含新的 invoke 调用。

这个定义有两条公理般的性质（由此产生全部表达力）：

1. 递归子 agent 是默认的——模型输出语言里天然含 invoke，写子 agent 调用不需要任何额外机制。
2. 模型所见的一切皆是变量——不仅数据与工具，连用户提示和 REPL 历史本身都是代码环境里的变量（__history__），可以被引用、传递、按引用交给子 agent。

抽象的精妙之处在于：它把「harness 有哪些功能」这个开放问题，替换成「这个原语能表达什么」这个封闭问题——后者可以用理论论证（闭式循环即尾递归 invoke）加受控实验来回答。论文 A 由此提出的问题是：这个极小原语，配上纯提示（无手工工具、无外挂系统、无文件系统），能否实现传统上需要专用 harness 的能力？

3.2 论文 B：把「agent 可信运行」抽象为「三个可证性质」

论文 B 的核心洞察是：

agent harness 的运维契约 ≈ 可判定程序的花费契约

三个类比：

形式化定义：一个有界循环（bounded loop）是三元组 ℒ=(W,G,B)——worker（尝试干活的 agent）、gate（worker 写不进的独立验收器）、B（声明预算：尝试上限 m、无进展窗口 w 等）。有界循环图把这些循环组成 DAG，外加一个修复关系 E_r：下游失败时可把已完成的子 DAG 重新放回待执行状态（这是唯一的「回头边」）。

问题定义：能否证明以下三性质，且全部在运行前可读？

1. It finishes（终止性）：修复边会重置内部预算计数器（正是单循环归纳法依赖递减的量），在带重置弧的网上一般的可判定性不存在——什么充分条件下可证？
2. It does not drift（不漂移）：没有节点可以不经 gate 判决到达 done——worker 的自我声明不得出现在任何 guard 中。
3. It does not overspend（不超支）：声明的天花板在一次尝试内部被执行，而非仅在尝试之间。

抽象的精妙之处：论文 B 没有去证明「工作正确」这种不可能的性质（gate 本身可能错），而是证明「完成的依据来自哪里」这种控制流性质——这恰好是可以在不假设 worker 任何行为的前提下严格证明的。代价是 gate 质量成了新的经验问题，论文 B 用第二套方法（变异测试）度量它，形成闭环。

四、问题解法

4.1 论文 A：invoke 原语 + JAZ 框架

核心类比：DSL 化的 harness 就像乐高积木说明书，而传统框架是手工胶水。 乐高说明书只规定积木块（原语）和插接规则（语义），不规定你搭什么；手工胶水框架则把每一步怎么粘都焊死了。JAZ 选择做乐高。

JAZ 的实现在 invoke 原语之上只加了三个薄层：

1. 动态作用域 scope。with scope(web_search=web_search) 块内的所有 invoke（含递归子调用）自动获得该变量。为什么用动态而非静态作用域？因为 invoke 没有静态实现（每次调用生成新函数体），静态作用域无从谈起——这是从原语定义直接推出的语言设计决策。

2. Hooks 系统。回调点覆盖 invoke/LLMQuery/REPLExec 三个层面的 Enter/Send/Complete/Exit 事件，内置 hooks 包括可观测性（Logger、Tracing）、资源控制（BudgetPool 预算池、IterationLimit、RecursionLimit、ContextWindowWarning）、校验（ReturnType、ValidateReturn）。关键设计：hook 只能发出静态可组合的 effects，多个 hook 的冲突写入以错误拒绝而非顺序依赖——这让 BudgetPool 这类全局约束成为可能。

3. Config 系统。Config(llm, repl, protocol) 三元组同样可局部可全局，顶层用 GPT-5.4、子 agent 用 GPT-5.4 nano 的分层配置一行搞定。

两个案例的解法：

• 长程记忆（StuLife）：当上下文窗口用到 70% 时，ContextWindowWarning hook 注入一条消息，提示 agent 执行「尾递归委派」——把完整历史通过 prev_history=globals().get("prev_history", []) + __history__ 按引用传给子 agent。关键：历史是变量，所以传递零成本且无损。这个模式统一了现有所有上下文管理方案：compaction 对应只传摘要，Chroma Context-1 对应传过滤后的历史——都只是这个一般模式的特例。

• 持续自我改进（AppWorld）：顶层 invoke 天然控制传给子 invoke 的全部输入，于是自然成为 meta-agent：批量派发任务给子 agent、失败后读子 agent 的 __history__ 变量诊断、修改提示与技能（skill）、自适应调整批大小。对比 ACE 固定的「每个任务后 Reflector+Curator」流程，JAZ 的 meta-agent 有完全的代码表达力来自由设计改进策略。

4.2 论文 B：有界循环图 + 三定理 + 度量仪器

核心类比：可证终止的花费契约就像出行前预算表，而不是月底看账单。 月底账单（post-hoc 观测）告诉你花了多少，但为时已晚；预算表（pre-run manifest）在出发前就告诉你最坏情况。论文 B 的工程量正在于把账单变成预算表。

解法分四层：

第一层：裁决三值契约（Theorem 4.1）。 gate 只能返回三值：pass（读到了工件且条件成立）/ reject（读到了且不成立）/ incapacity（根本无法形成意见）。关键设计：判 incapacity 的合法情形只有两种——调用格式错误、锚区（gate 代码与参考数据所在区）文件缺失。worker 自己的工件为空或损坏不算 incapacity——那是一个 reject（关于工作的答案），不是 harness 的失灵告白。区分 pass 与 incapacity 边界的判据是所有权：出问题的文件是谁负责的？这在运行前就写在防篡改声明里。推论 4.1 一针见血：「没有东西可查」是关于工作的发现，不是无能力的自白。

第二层：终止性与闭式上界（Theorem 5.2 + Corollary 5.1）。 单循环终止是平凡的归纳，难点在修复边：它重置预算，正好重置了内部归纳法依赖递减的量。解法是一个充分条件组（Assumption 5.1），其中承重的是全局修复预算：修复轮数 R 是全图单一计数器，跨边界递减、永不重置。若按每节点计预算（系统中所有其他预算的惯例），两个节点可以互相修复到永远。在此条件下，字典序二元组 (R−ρ, 剩余预算) 严格递减，终止得证，且总尝试数有闭式上界 A(G) ≤ (R+1)·Σᵥ mᵥ——每个量都是清单里已写的字面量，运维者不跑任何东西就能算出最坏情况。修复功能的代价清晰可见：就是那个 (R+1) 因子。

第三层：done 的健全性（Theorem 7.1）。 直接从控制流证明：图报告 done 时，每个节点都在 append-only 哈希链账本里有 gate 的 pass 判决。证明的实质是它从未触碰什么——程序中不存在任何读取 worker 自我声明的分支。更强的是 Corollary 7.1：任何拿到运行目录的第三方都可以重放账本验证此性质，不需要重跑、不需要信任生产方——「保证」与「保证声明」的区别所在。

第四层：度量 gate 本身。 一个关于 gate 的证明，价值上限是 gate 的价值。如何度量一个验证器？论文 B 的仪器是两层变异测试：Tier 1 是机械算子，其「盲性」（不参考任何 gate）由语法树断言在构建时强制（Theorem 10.1）；Tier 2 由 5 个独立 agent 模型只看循环的声明目的、不知检查器的情况下编写「满足字面、违背意图」的语义变异体。标签由变异操作在编辑前固定，与 gate 行为无关，故不存在等价变异体选择偏差（Theorem 10.2）。

测量结果的自反性是全文最独特的部分：把仪器对准自己，发现了 47 个已出货且通过评审的缺陷 gate；发现了自己论文里「六处声明了边界但从未执行」（包括一条定理的前提）；发现了测量装置本身有 24 个循环因覆盖缺陷而静默消失；冻结 gate 后换一族新鲜算子，假接受率从 0 回升到 23.3%——那个 0 证明的是语料耗尽而不是质量。

五、评估指标与实验证据

5.1 论文 A 的实验体系

主指标：Pass rate（通过率，通过分数任务的百分比）与 Score（平均分），双数据集双 setting 设计：

实验一：StuLife 长程环境（1284 个模拟大学一学期的任务，一次运行约 7000-8000 次环境交互、3000-5000 次 LLM 调用；939 个计分任务，其中 207 个「远回忆」任务需回忆 50+ 个任务前交付的信息）。模型统一 GPT-5.4 nano：

解读要点：远回忆子集是真正的区分器——JAZ 比专用 harness Letta 高 8 个百分点，成本不到一半；比同门 CodeAct+subagents 高一倍多。消融设置（用 hook 移除 __history__ 和提示变量来重构 CodeAct）确保差异只来自 invoke 的两条定义性质。

实验二：AppWorld 持续自我改进（417 个 test-challenge 任务的完整序列，GPT-5.4 顶层 + GPT-5.4 nano 求解器）：

解读要点：JAZ 的 meta 成本（9.9 美元）显著低于 ACE（17.1 美元），因为 meta-agent 可以批量派发任务、按需读取轨迹片段，而 ACE 每个任务后都要跑昂贵的 Reflector+Curator。ACE 原始在线模式估算成本超过 180 美元，论文限制其只在前 42 个任务上学习以公平比较。

为什么这些实验能证明核心主张：严格的任务/方法解耦协议（环境提供任务描述、方法只提供任务无关指导）、字节级一致的控制提示、缓存命中率控制系统误差 <2%、以及最重要的——消融即重实现（CodeAct 是 invoke 减去两条性质的受控版本）。这让「表达力是差异来源」的归因站得住。

5.2 论文 B 的实验体系

主指标：α（假接受率，gate 放过缺陷工件的概率）与 β（假拒绝率，拒绝合法工件的概率），两者必须同报——只报 α 的 gate 可以靠全拒来刷零，只报 β 的可以靠全收。附带上界利用率 U=a/m（实际消耗/声明上限）。

证据链八组实验（E1-E8）：

上界紧性验证（Section 6）：9/9 工作负载预测尝试数与观测完全一致，U 精确截止在 1.0；软上界 4/4 情况精确达到。特别地，上限恰好为 1.0 而非 1.1 是收据设计的功劳（区分「未花费的 lap」与「尝试」）。

为什么这些实验能证明核心主张：论文 B 的主张是「验证器必须被度量」，其最有力证据是自反性的——仪器在自己身上找到了 47+14 个通过评审的缺陷，E7 证明了即使零误报也只是语料饱和，E8 证明了仪器存在结构性盲区。这种「用最强证据反对自己」的论证方式，比任何正面数字都更有说服力。

六、效果优势的根源解释

6.1 根源机制与证据链

论文 A：为什么极简 invoke 能胜过专用 harness？

因果链一（远回忆场景）：

1. invoke 的性质 2（一切皆变量）使历史可按引用无损传递给子 agent【机制，论文实验直接支持——任务 #1282 分析显示 JAZ 在 69 层递归深度后仍保有完整 prev_history 并一步检索到 497 个任务前的协议讲解，而 CodeAct+subagents 因手抄提示有损丢失指令，Letta 的混合搜索无法做精确子串匹配】
2. 引用传递 vs 手工复制 → 信息保真度差异随委派深度复利放大 → 深递归场景下 JAZ 的远回忆优势（69.9% vs 32.0%）是结构必然而非偶然【因果推理，由任务分析支持】
3. 专用 harness 的刚性源于其内嵌假设：Letta 假设「检索=向量+关键词搜索」，在需要精确匹配的虚构协议名场景失效——对手工胶水的每一条焊缝，都存在一个恰好从焊缝处断开的任务【论文的 Takeaway 2，机制层面论证】

因果链二（自我改进场景）：

1. invoke 让 meta-agent 获得全代码表达力 → 可自由设计批处理、选择性读轨迹、自适应批大小【机制，实验轨迹分析支持】
2. ACE 的固定流程（每任务后 Reflector+Curator）使其 meta 成本十倍于 JAZ → 成本效率差异是流程自由度的直接经济后果【论文实验支持】
3. JAZ 优化对象是「invoke 的一切输入」（提示+技能+一切），ACE 只优化提示 → 优化空间维度差异【论文实验支持】

诚实说明：JAZ 对 Letta 的整体优势（72.6 vs 70.9）在全集上并不悬殊，主要优势集中在远回忆子集与成本；这符合机制预测——普通任务上记忆机制不重要时两者应当接近。

论文 B：为什么类型化预算+独立 gate 的架构优于声明式约定？

因果链：

1. 「声明」与「执行」是不同的工件——论文 B 在自己系统里找到了最极端的反例：max_wallclock_s 在全部 69 个清单里声明、验证、显示、记录，却只在尝试之间比较一次；一个声明 120 秒的循环实际跑了 300+ 秒，最终被一个「没人写过的 300 秒 runner 默认值」停掉【论文核心自曝，最强证据】
2. 未强制的边界还会掩盖第二个缺陷：一旦强制执行，发现 69 个循环中 65 个声明的数值（每尝试 6 秒）根本装不下真实 agent 的单轮耗时（实测中位数 48.3 秒）——未强制的边界压制了能暴露其自身数值荒谬的信号【论文实验支持】
3. 独立性必须是 harness 强制的结构性质而非部署纪律——「同仓库的验证步骤」满足三条件定义的第一条而不满足后两条，worker 能说服性地描述工作等于直接对着自己的法官说话【机制论证，Remark 3.1】

6.2 相关工作检索与对照

以下为外部检索交叉验证的结果（检索日期 2026-09-25）：

6.3 综合判断与未决问题

多项研究共同支持的机制：

• 「按引用传递上下文」优于「文本复制」——RLM（+130% 量级）与 JAZ 远回忆（+38pp）在完全不同任务上给出同向证据，机制来自信息论层面的无损性，属于结构性优势。
• 「预运行预算必须由结构保证而非 agent 预测」——token 消耗研究证明 agent 自预测相关性 ≤0.39 且系统性低估，论文 B 的闭式上界是唯一可靠来源。
• 「验证层本身必须被度量」——论文 B 的 E7（冻结后 23.3%）与 E8（外部审计发现结构性盲区）证明未度量的零没有信息量。

仍属合理推测的机制：

• 「表达力溢价在更长任务序列上继续扩大」——JAZ 只测了两个环境，StuLife/AppWorld 的序列长度是否足以外推到数千任务尚无证据。
• 论文 A 作者宣称的「agentic 行为是计算表达力的后果」这一哲学论断，比其实验能支撑的范围更宽。

优势的适用条件与失效条件：

• JAZ 的优势条件：任务需要 agent 程序化访问自身上下文（精确检索、引用传递）、或需要 meta-agent 灵活设计改进流程。失效条件：任务可干净分解且每步有标准做法时，手工流程（LangGraph 式显式图）的可审计性与可维护性可能反超；当模型能力弱到无法驾驭完全自由度时，结构化脚手架更稳。论文 B 的证据条件：gate 是确定性代码、worker 单轮可被外部进程打断。失效条件：LLM-as-judge 单独作 gate（论文 B 自己证明合取组合下 α 不升，析取组合即失效）、以及「模型同时写了工件和检查器」时结构独立≠统计独立——这是论文 B 明确承认的最大缺口。

七、必要知识反推

假设让一个零基础的人分别复现这两篇论文，他最少需要什么？

7.1 论文 A 的必要知识

领域知识层：

• agent loop 的实际运作方式（提示如何组装、工具如何调用、上下文如何累积）——不理解这个就无法定位「哪些是 harness 强加的、哪些是模型自发的」。
• 记忆系统（MemGPT/Letta 的分层与检索机制）与自我改进系统（ACE 的三角色循环）的现状——它们是对照系，不懂其设计假设就看不出 JAZ 在哪里击穿了这些假设。

方法论知识层：

• 编程语言理论：λ 演算的操作语义、语言原语的语法/语义区分、动态 vs 静态作用域、尾递归与循环的等价性——Definition 1 及附录形式化全靠这些。没有「闭式 agent loop = invoke 的尾递归」这个观察，整个第一性原理推导无从谈起。
• 受控实验设计：混淆变量控制（prompt 双盲拆分、缓存命中率控制、消融即重实现）——JAZ 的结论强度完全建立在「CodeAct 是减法消融」这个设计上。

工程知识层：

• Python REPL 的机制细节（globals、repr、变量生命周期）与 LLM API 的前缀缓存机制——「为什么不能让模型手写尾递归调用而要 harness 自动追加」的答案藏在这两处的工程约束里。

融合的关键节点：语言理论（递归即循环）× agent 工程（REPL 即环境）在「invoke 的函数体由 LLM 运行时生成」这一点上化学反应——一旦把 LLM 看作「运行时函数体提供者」，整个框架设计就从「加什么功能」变成「原语语义是什么」，全部后续决策（动态作用域、hook 只发静态 effects）都成了必然推论。

7.2 论文 B 的必要知识

领域知识层：

• agent 生产的真实形态：agent CLI 以子进程运行、headless 模式权限自动拒绝、工作目录语义差异——E5 的「差点发布假发现」全部来自对这些生产细节的无知。
• 分布式系统与持久执行的现状（Temporal 的超时/重试语义、K8s 的 activeDeadlineSeconds）——论文 B 的贡献定位是「这些系统有什么、缺什么」，不懂现状就说不清三个增量是什么。

方法论知识层：

• Petri 网与重置弧的可判定性地图（Dufourd 1998、Finkel & Schnoebelen 2001）——没有这张地图，就会试图证明不可证的东西（工作流健全性）或宣称不可判定其实可判的东西（带修复的终止性）。字典序测度 (R−ρ, Σ) 的选择直接来自嵌套循环终止证明的标准技术。
• 形式逻辑中的真空性（vacuity，Beer et al. 2001）——「未被前件满足的性质通过了检查」这一缺陷类在模型检验界有成熟名字与检测工具，把它迁移到 agent gate 是论文 B 最有想象力的知识搬运。
• 变异测试理论（等价变异体问题、DeMillo 1978 传统）与统计学（Wilson 区间、anytime-valid 置信序列、估计对象与覆盖率的区分）。

工程知识层：

• 防篡改设计（写权限分区、锚区、哈希链账本的第二原像抗性）、以及「测试驱动地验证 guard」的纪律：论文 B 给每个 guard 配测试的方法是删掉 guard 确认测试变红——「通过的测试证明不了什么」正是其自身论文的论点。

融合的关键节点：工作流验证（重置弧地图）× 软件测试（变异测试）在「gate 是手写检查器」这一点上融合——当验证器不是形式逻辑公式而是任意代码时，模型检验的工具箱失效，变异测试成为唯一可用的度量仪器；而真空性概念恰好横跨两者，成为从形式方法向 harness 工程输送工具的桥梁。

八、论文中可以提取的通用性灵感

灵感一：原语极简化——把「功能清单」压缩为「语义定义」。 核心思想：当你要设计一个系统家族时，与其罗列功能，不如定义一个最小的语义原语并证明功能是其特例。论文证据：invoke 一个原语覆盖记忆与自我改进两类专用系统，且理论上闭式循环、递归都是其特例。推广场景：数据库中间件（把「缓存/分片/重试」定义为查询算子的语义组合而非独立模块）；机器人技能库（把操作技能定义为「感知-动作」原语的递归组合）；教育系统设计（把教学法定义为「学习事件」原语的编排而非课程表）；BI 报表平台（把所有图表定义为一个「聚合原语」的参数化）。

灵感二：一切皆变量——给参与者对其上下文的程序化访问权。 核心思想：系统参与者的效率上限常取决于它能否引用而非复制自己的历史与输入；「所见即变量」是把只读界面升级为可编程界面的分水岭。论文证据：远回忆任务上按引用传递历史带来 +38pp 的提升，而复制式传递在 69 层递归后信息有损衰减。推广场景：人机协作界面（给人类对其操作历史的脚本化访问，而非翻聊天记录）；API 设计（返回引用/句柄而非内联大对象）；组织管理（让一线员工程序化地引用全部决策记录，而不是层层口头传达）；科研工具（让分析脚本引用完整实验历史变量）。

灵感三：声明的边界必须等于执行的边界——否则声明是装饰。 核心思想：任何写在配置/文档/承诺里的约束，如果不在每个相关执行点被强制，它不仅无效，还会掩盖暴露其无效的信号。论文证据：max_wallclock_s 声明于 69 个清单、展示于每个横幅、记录于每张收据，却只在一个错误的点被执行；其无效还掩盖了 65 个循环的数值本身装不下真实工作负载。推广场景：安全合规（「禁止访问生产库」必须由网络层强制而非文档约定）；个人效率（预算写在备忘录 vs 绑定支付限额）；API 治理（限流声明必须在网关每跳执行）；自动驾驶约束（「不得越过车道」由控制层钳制而非驾驶手册）。

灵感四：三层裁决——把「你的错」与「我不能」分开回答。 核心思想：任何验收环节应输出三值：合格/不合格/无法评判，且第三项的合法情形必须极窄并事先声明（判据是所有权而非严重性）。论文证据：二元契约下 worker 发坏 JSON 会让整个运行停止，而正确的做法是让 worker 重试；裁决边界从防篡改声明读出，可证明全且不重叠（Theorem 4.1）。推广场景：代码评审（评审人区分「代码有错」与「我看不懂/上下文缺失」）；医疗诊断（区分「检查异常」与「检查无法完成」）；客服工单（区分「需求被拒」与「材料不足」）；自动驾驶 RTA（区分「动作危险」与「传感器失效」）。

灵感五：度量验证器，而不是相信验证器。 核心思想：任何「检查别人」的组件，其自身的错误是静默且讨好性的（往让系统好看的方向错），因此验证层必须被独立于其作者的仪器度量。论文证据：47 个通过评审的缺陷 gate；作者自己对刚修完的缺陷类又写出新实例；换一族新鲜测试算子后「零缺陷」变 23.3%。推广场景：安全审计（审计清单本身需被红队检验）；考试系统（考题需经统计校验区分度而非命题人自审）；医疗质检（质检仪定期用标准品校准）；机器学习评估（基准数据集需被对抗性验证无泄漏）。

灵感六：预运行的闭式上界——把最坏情况变成可计算的清单。 核心思想：对不可精确预测的随机系统，把「最坏情况」表达为清单中已声明量的闭式函数，让人在承诺之前读到数字。论文证据：A(G) ≤ (R+1)·Σmᵥ 全部是清单字面量，运维者无需运行即可授权；代价 (R+1) 因子被显式定价而非隐藏。推广场景：云计算配额（部署前读出最坏成本公式）；项目管理（缓冲时间 = 显式乘数×任务估计和）；手术排程（最坏时长的闭式估计）；政府采购（预算上界在招标前可算）。

附录：两篇论文的速览对照卡

两篇论文放在一起读，会看到一个正在成形的学科共识：agent harness 不再只是「让 LLM 干活的脚手架」，而是一种可以被定义、被证明、被度量的计算系统。语言化定义它能做什么，验证化证明它承诺什么，度量学检查它是否兑现——工程偶然正在被三步替换为数学对象。