AI Agent 用好测试与验证技术了吗？
我们此前曾指出，虽然让 coding agent 借助有效的测试技术来达标比以往更容易，但软件质量反而在下降，说明开发者默认的用法可能并不奏效。本文我们测试：给 agent 下达简单的指令（让它用某个测试技术或某个库）能否提升实现的正确性——这相当于模拟一个没有测试经验、只是听说过"该用某某技术或某某库"的人来指导 agent，看看实际效果如何。
我们复用上文agent 编程语言效果对比中提到的 Zstd 实现评测，但把对比维度换成了测试技术和测试库：在让 agent 实现 Zstd 的 prompt 后附加不同的补充指令，例如"使用 TDD""使用 Lean 4""使用 QuickCheck""使用 property-based testing"等。此外，我还跑了 IMAP RFC 等其他评测，后文会简要讨论。
所有实现均使用 Rust。共测试了 26 种提示条件：ACL2、Alloy、“审计并模糊测试高风险区域”、“先审计”、Creusot、Default（无额外指令）、差分测试、Fuzzing、Hegel、Insta、Judgement（要求 agent 自行选用最佳技术）、Kani、Lean 4、“不许出错”、蜕变测试、变异测试、基于属性的测试、Proptest、QuickCheck、rstest、Rust 内置测试框架、SMT 求解器（Z3、cvc5、Yices 均可用）、Spin、TDD、TLA+ 和 Verus。另外还测试了 4 个 skill：使用官方 Hegel skill 的 Hegel、ECC Rust 测试 skill（ECC 是一个拥有 25 万 GitHub star 和 3.8 万 fork 的 skill 合集）、Trail of Bits 属性测试 skill，以及我自己写的一个测试 skill（我是个守旧派，习惯用 prompt 而不是 skill，也不知道怎么写好一个 skill）。除我自己的 skill 外，其余 skill 都是让 codex 搜寻相关 skill 时排名靠前的那些。
预测
我提前登记了一些对各条件表现的猜测：
- TDD 表现会偏差（55% 置信度）
- 我特意加入 TDD 就是因为觉得它会表现不佳
- 置信度不高，因为我不知道 agent 被要求做 TDD 时会怎么做；也许 agent 并不会真的按 TDD 来，而是做些不会拖后腿的事（又或者我对 TDD 会拖后腿的判断本来就是错的）
- 形式化方法不会表现更好（52% 置信度）
- 我的想法是：形式化方法确实有效且有用（比以往任何时候都更有效），好的测试方法同样有效且有用；在简单问题上，如果两者使用水平相当，形式化方法不应胜出
- 与上一条类似，但这里的置信度更低。原因有二：一是我根本不知道 agent 在被要求执行任意操作时具体会怎么做；二是在 agentic coding 领域，形式化方法（formal methods）的声量远大于有效的测试技术，所以完全有可能各大实验室用合成数据在 RL 环境中训练 agent，让它们非常擅长形式化方法，却没有针对性地训练它们用好测试技术（我预期后者其实更容易实现，只是有效的测试技术相对不够"潮"，所以没人做）
- Make no mistakes 不会优于 no instructions（95% 置信度）
- 这本来就是个玩笑，而且已经很多人试过了。如果真有效，大家早就发现了
- ECC 测试 skill（25 万 stars、3.8 万 forks）不会优于基线（65% 置信度）
- 内容偏长，也没有我预期中真正有用的信息。它指示 agent 使用 TDD；就让它执行 TDD 的程度而言，我认为这反而会让效果变差（它的指令比专门的 TDD 条件更具体，理论上更容易被执行，但据我所知越具体反而越可能失败）；其余内容看起来没什么用处，还额外消耗了 token
- 我所有关于 skill 的预测置信度都不高，因为我不太用 skill，也不确定怎么真正评估它们。我的思考方式是："如果把这段文本作为 prompt 塞进去，让它一直待在 LLM 的 context window 里，效果会怎样？"
- Hegel skill 不会优于基线（65% 置信度）
- 内容很长（SKILL.md 加上链接的 Rust 参考文档超过 2 万 tokens），读起来更像教程而非 agent 指令
- Trail of Bits 测试 skill 不会优于基线（55% 置信度）
- 包含一些看起来可能有用的信息，但篇幅也偏大
Overall results
下面是一张非常凌乱的图表，展示了各测试条件的结果（codex 搭配 GPT-5.6 Sol，分别使用 medium 和 xhigh 两种努力等级）。看数据时，我比大多数人更喜欢信息密度更高、更凌乱的图，比如这里的第二张图。因为大多数人觉得这类图表乱到没法看，所以我给别人展示时，习惯把信息拆成一组图，每张承载的信息少一些。由于下面会讨论到的原因，这里我就不拆了，直接给出这张极其凌乱的图：x 轴是成本，y 轴是通过 100%（隐藏）测试的运行占比，每个条件和努力等级各跑 80 次取平均（鼠标悬停可看到 bootstrap 协方差、50% 置信区间，颜色上大致按类别区分，比如偏蓝代表 formal methods，偏绿代表 property-based testing，等等）：
能看出的一点是，没有哪种方法显著碾压其他方法。不过 Default（不加额外指令）的表现高于平均水平。看 xhigh 档位，fuzzing 和 PBT 相关条件平均略优于 formal methods；medium 档位则差异更不明显。codex 推荐的测试相关 skills 表现不佳，不过我们快速写的一个自定义 skill 还行（主要区别在于，我们的 skill 设计上是把 agent 从默认行为拉向更高效的做法，而其他推荐的 skills 更像教程）。如预期，TDD 表现不好——有一个 skill 也建议 agent 使用 TDD，但 agent 尝试遵循该指令时，效果同样很差。
真正去看 agent 做了什么，很快就会发现：总的来说，agent 并不擅长使用这些工具和技术。正如我们在此前提到的，以及我交流过的所有人也指出的，agent 写测试确实很差，默认情况下似乎并不理解怎样才算合理的测试。比如 Gary Bernhardt 的这条评论：
AI agent 做测试的思路，大致如此：
先把 15 年前那些反对 mock 的人凭空想象出来的病态案例搬出来——他们自己压根没用过 mock。也就是对“过度 mock”的幼稚臆想。
再把这些病态案例当成你整个测试策略的主轴。
结果发现，如果你要求 agent 使用某种特定的测试技术或测试库，效果并不像你期望的那样有多大改变。下面我们会详细看几个具体案例，但从宏观层面来说，面对各种测试技术，agent 往往只有两种表现：要么照常写它们平时会写的测试，只是套进另一种测试技术的框架里；要么表面上用了一下某种技术，却没有做那些真正能从该技术中获益的关键步骤。大多数情况下，当点名列出某种技术时，agent 做的正是 Gary 所描述的那些事，只不过换成了对应的技术（比如形式化方法，它们证明的多半是些无关紧要的性质；property-based testing 方面，agent 则严重依赖完全随机的输入，大量命中无效/被拒绝的用例，或者找一个很平凡的 property，然后对着它跑一堆低价值的随机用例）。在 IMAP RFC 上（每种条件我各跑了 40 次）以及其他几个随机 RFC 上（各跑了几次），结果都没有实质差别。总体来看，无论什么类型的问题——不管是 Zstd 这类位操作问题，还是 IMAP 这样的协议1，或者别的什么——agent 都无法有效地运用形式化方法或各种测试库与技术。
在 xhigh 档位下，agent 通常能让自己写的测试通过，但测试质量很差（比如一个功能需要四个不同的 bitstream，它们却把同一个 bitstream 提交了四次，从而完全漏掉因 bitstream 顺序颠倒才会触发的 bug）。正如我们之前在 Zstd 评测中针对编程语言指出的那样，用更低的 effort 档位在朴素的循环里跑，结果会更糟（agent 会更多出现这类问题，并因卡住而正确率更低）。
我很好奇，为什么 AI 实验室没有创建 RL 环境来教 agent 如何做好测试——软件不能正常运行对 coding agent 的推广来说显然很重要，而测试这件事看起来也很适合用 RL 来训练。如前文所述，agent 在有限运行时间优化问题上已经表现相当不错，这很合理，因为这类问题可以低成本地批量搭建 RL 环境来训练。也许测试这类问题动手做比看上去难，但为有效测试和测试技巧搭建 RL 环境，看起来属于同一类问题。或许瓶颈在于有效测试技巧的知识传播范围不够广，所以没人想到去做，大家只是让 agent 低效地测试（比如只做标准单元测试）2；又或者，这个问题在封装上比运行时优化难得多，出于某种原因？如果 agent 强到一般不需要测试或验证就能写出正确代码，那这个问题可能很快就会变得无关紧要。但至少在从最初到现在（2026 年 9 月）公开 agent 的水平下，如果 agent 能在没有测试专家指导的情况下对测试有个基本概念，应该会显著提升 agentic coding 的效果。
下面按正确率从低到高排列，逐一查看 agent 在各条件下的具体表现，但我建议不要从这个排序中得出任何强结论。
这里很多失败和我们之前研究编程语言对 token 使用和正确性的影响时看到的失败类似，即失败往往是偶发的、特异的。比如在编程语言方面，我们发现 agent 在 Clojure 中搞错 byte 转换语义的比例相当高，但在 Java 中却不是这样——尽管 agent "应该"（实际上可能也确实知道）可以用 unchecked-byte 而非 byte 来获得 Java 的 byte 转换语义。
虽然人们总能给出各种泛泛而谈的解释，说某些语言比另一些更适合 agent 使用，但当我们真正去看 agent 实际做了什么、失败模式又是什么时，我还没听见过哪个说法能站住脚——不管是有人觉得 Elixir、OCaml 还是 J 特别适合 agentic coding，理由都不成立（唯一例外是关于 Rust 内存安全的评论，我们在多语言 pandoc 评测中通过对比 agent 编写的 C、C++ 和 Rust 代码验证了这一点）。实际上我们看到的是各种没有规律可循的失败3。就语言而言，由于观察到语言流行度与性能（成本更低、正确性更高）之间存在中等程度的正相关，合理的推测是：更流行的语言之所以表现更好，是因为有更大的训练数据量（可能包含合成数据，不只是人工编写的代码）。但在本文的场景中，除了 agent 在仅有库名或技术名称时通常不太擅长应用测试/验证手段这一点之外（后面会讨论什么方法更有效），并没有明显的规律可循。如果不想看各条件下的具体情况，点击这里跳到最后一项。
Verus
Verus 利用 SMT solver 和多种推理方式来证明代码符合规格说明。
虽然 Verus 可以证明代码符合规格说明，但 agent 并没有这么做。相反，它们去证明了一些与 Zstd 相关的抽象性质。我自己没有用过 Verus 这类工具，所以无法判断专家甚至初学者通常会怎么做，但从教程来看，agent 完全没有尝试用 Verus 去验证实际代码，而是只用来做抽象推理，这让我觉得有点奇怪——它的设计初衷似乎就是让证明实际代码的性质变得更简单。
此外，从证明了哪些性质来看，一般情况下证明的性质数量很少，而且证明的那些性质也没什么意思。比如，agent 会去证明“给定合法的 cursor/index/distance，操作结果不会越界”之类的东西——证明这个不算坏事，但bug本来就不出在这里。另外，agent 还经常写出实际上等价于 A => A 的空洞证明。下面就是一个真实存在的这种 Verus 证明：
requires
0 < a <= window,
0 < b <= window,
0 < c <= window,
ensures
0 < c <= window,
0 < a <= window,
0 < b <= window,
在 agent 真正证明出一些东西的情况下，它们证明的通常也是比较简单的性质，而回避了那些可能藏有 bug 的部分（举个例子，agent 经常在 encode 和 decode 时没有反转 bitstream 的顺序，而写的测试又因为本身是回文的而检测不出来；如果在反转这里做一些证明，也许能迫使 agent 换个角度“思考”这个问题）。
看起来，仅仅提供 Verus 及其文档，agent 并不能从中获得什么价值。
再看结果：xhigh 档的整体 Verus 结果还算可以（正确率略低于平均水平，但成本低得多）。medium 档的成本属于平均水平，但正确运行的比例最低，平均正确测试数也最低。由于 agent 实际上没从 Verus 中得到什么价值，它们保证正确性的手段主要还是传统测试（Rust 内置的 #[test] 单元测试函数）。从 medium 升到 xhigh 时，agent 在传统测试上投入的精力大幅增加，而在 Verus 上只多花了一点，这让 xhigh 的结果得以过关。
具体看测试内容，在 Verus agent 表现明显更差的两项功能中有一项（four stream jump table），Verus agent 在 160 次中有 89 次写了针对它的测试，恰好和 Default agent 的次数一模一样，但 Verus agent 写出劣质测试的概率远高于对方。它们更倾向于把错误的期望结果写进测试，或者写些很容易通过但覆盖面很差的用例，比如把四条流设成完全相同的。我前面说失败模式很"怪"，指的就是这种。Verus 本身并没有什么东西会让人觉得不用它的时候就会写出差测试；通常我们不会预期一个用过 Verus 的人写单元测试会退步，就像不会预期用 Clojure 的人会在字节转换上多犯错一样。但这里确实发生了，原因不明（不排除是巧合）。
不知道 AI 实验室内部的人能否拿到更好的信息来解释原因，但站在外面的我们通常很难判断这种事为什么会发生。即便是语言那个问题，我们提出的一个合理假设也需要跑很多语言的大量样本；我们看过的研究同类问题的论文也没有观察到语言流行度和 agent 有效性之间的相关性——要么是因为它们看的语言太少、不足以推断出这么弱的相关性，要么是因为问题规模太小、太简单。
Alloy
Alloy 通常被称为有界模型检查器。对 Alloy 6 来说这个说法可能不完全准确，因为它引入了一些额外特性，但这已经超出我的专业范围了。据我理解，用 Alloy 通常是证明你模型的属性（而不是证明代码能跑）。
Alloy 的正确率排在倒数第二，而且难得地，在 medium 和 xhigh 上表现都普遍很差。虽然图表没有展示（因为看起来没有额外信息量），但总体来看 max 和 xhigh 的结果高度相关，且与 medium 的结果差异明显。
和 Verus 的情况类似，用 Alloy 的 agent 基本还是靠 Rust 标准的 #[test] 来保证正确性，Alloy 基本就是在瞎捣鼓。再次证明，用不好形式化工具并不会提升正确率。
个别案例中，Alloy 的使用确实接近发现了问题或风险，但数量很少。有一次，Alloy 给出了一个反例，随后 agent 在实现 Rust 版本时为这个潜在 bug 加了缓解措施。可惜那个反例依赖的是一个 8 位溢出，而实际实现用的是 64 位的 usize，在给定输入下根本不可能溢出，结果只是让代码变得更复杂，并没有真正防住任何 bug。
另一次，Alloy 的规格本身写错了，相关测试随之失败。测试失败后，agent 修掉了这个错误的规格。如果规格一开始就是对的，也许 agent 根本不会写出有问题的代码。确实有些案例看起来像是这种情况，但无法确认是否真的防住了某个潜在 bug。
Alloy agent 建模的内容比 Verus agent（后者主要检查算术之类的东西）更贴近 Zstd 算法本身，但建模方式仍然是错的。
差分测试
差分测试的做法是：给多个实现喂同样的输入，然后对比结果来找问题。对 LLM 来说，这个思路看似合理——毕竟不同采样往往给出不同结果，而且正如我们在这里提到的，让 agent 反复迭代一个实现（可能只是整个系统的一部分，甚至只是某个函数的某一段）通常不如让它从头来一遍效果好。
但这次差分测试排到了倒数第三。具体来看，xhigh 档的表现略高于平均，medium 档则远低于平均。所有 agent 都没有生成两个完整的实现来做对比。160 次运行中，135 次做了某种差分测试，但和前面几个条件一样，这些测试基本都流于形式、几乎没有实际作用。而在差分测试本可以抓到 bug 的场合，agent 往往没有用独立的方式分别实现，而是把同一套逻辑写了两遍，把同样的 bug 复制到了两个版本里。
我有时会让 agent 独立完成任务，并用各自独立的上下文启动，但在差异测试上没能做到这一点，agent 通常就是把同一段代码写两遍。
Hegel Skill
官方 Hegel skill 如何改变 Hegel 的表现，值得一谈。但按正确性从差到好的顺序排列，Hegel Skill 排在 Hegel 前面，因为它在正确性上表现更差。关于这个 skill 的讨论见下文 Hegel 部分。
Lean 4
Lean 4 大致可以算作交互式定理证明器。
虽然我没有事先对 Lean 做预测，但如果当时要预测哪些形式化工具会表现好，Lean 肯定在我看好之列——它比较热门，且因为有来自 RL 环境的合成数据，大概率会有不错的表现。
Lean agent 确实证明了一些性质，比如 Verus 条件，但大多数 agent 只做了不会触及易错或风险区域的算术证明。
和其他形式化条件一样，Lean agent 高度依赖标准的 Rust 测试。与前面所有形式化条件相同，证明几条无关紧要的性质对正确性没什么帮助。
QuickCheck
QuickCheck 是一个基于性质的测试库，长期以来可能是这类库里最出名的，不过现在这个地位或许已被 Hypothesis 取代。
遗憾的是，agent 使用基于性质的测试的效果，和前面那些形式化工具差不多。用 QuickCheck 时，agent 大多只写了一些非常简单的“冒烟测试”，基本没检查什么东西。它们还用了随机输入，但完全随机的输入对测试 Zstd 这类东西效果很差（因为只会走到少数几个失败/拒绝的代码路径）。
此外，被检查的性质也相当少。虽然所有 agent 都用了 QuickCheck，但 160 次运行中有 63 次只检查了一条性质。agent 依然主要靠传统测试，只是名义上用了 QuickCheck。不知为何，agent 在这个条件下写的传统测试反而比 Default 条件和大多数其他条件更多，但测试—修复的迭代次数更少（导致这个条件的平均成本偏低）。
TDD
此处 TDD 表现不佳，IMAP RFC 评测中也是如此。
TDD 提示词似乎显著改变了 agent 的行为模式。agent 产出的测试数量翻了一倍，工作流也变成了更迭代的「测试—编码—测试—编码……」循环，不过 TDD 倡导者大概会说 agent 并没有真正采用 TDD——真正出现细粒度迭代式 TDD 的案例寥寥无几。
整体来看，agent 在前期写出的测试更多。例如，160 个案例中有 67 个，agent 在完成实质性（非 stub）实现之前就已存在一个或多个失败的测试，而 Default 条件下是 0/160。
就各类测试而言，TDD 条件下每种测试的数量都更多——既多了些琐碎的小测试，也多了集成测试和端到端测试。任何「agent 在某方面做得过多或过少」这类笼统的高层判断似乎都套不进数据。如果去看具体的失败案例以及测试为何没覆盖到它们，就会发现 TDD 条件下有不少这类情况。举例来说，当存在四条 Huffman 流时，Zstd 会使用一种叫 jump table 的结构。
尽管 TDD agent 写了更多覆盖一般情况的测试，它们在这个用例上的评测通过率反而更低。不管原因是什么，TDD agent 更容易写出没覆盖到困难情况的测试（比如让四条流完全相同且都变得琐碎，类似于我们在 Verus 中看到的情形）。这也是另一个让我好奇 AI lab 内部能观察到什么的地方——从外部来看，用 TDD 做 prompt 为什么会让 agent 写出更差的测试和更差的实现，并不显而易见。
如果手上只有 TDD 和少数几个测试条件，一个可能的假设是：TDD 风格的代码往往充斥大量质量不高的小测试，所以用 TDD 引导 agent 可能让它们也倾向于写更多这类低效测试。但不太清楚为什么 Verus 也会出现同样的模式。如果在开放模型上重跑实验、在某个层面查看模型内部实际发生了什么，也许就能验证这个假设对 TDD 是否成立——前提是 Verus（或其他情形）背后的原因是同一个。
有两个技能让 agent 以更迭代的方式运行，大概是认为执行更频繁效果会更好，但这两个技能反而表现更差。总体而言，在所有条件下，agent 都能让自己写的测试在 xhigh 和 max 配置下通过（图中未展示 max，不过 max 的准确率略高于 xhigh，而且成本低得多）。更迭代地追求测试通过，往往让 agent 写出更多有问题的测试，反而固化了错误行为。
Yossi Kreinin 对此有如下看法，解释了 TDD 为什么可能产生更差的测试：
我个人的理解是：如果先写测试再写代码，就很难覆盖那些真正棘手的场景，因为你当时还说不清哪些地方会难。就算做随机测试（我认为 TDD 跟随机测试没什么关系），你也更不容易把测试分布往 bug 集中的方向引导。如果你自己写了代码，至少能看一眼，你就知道哪些地方显然没问题、哪些地方拿不准——毕竟代码到底在干什么不容易一眼看明白。换句话说，TDD 会把你引向 black box testing，而面对复杂系统，我认为 white box testing 更有效。在人身上我比较确定是这样，但在 agent 上不太确定。
我当初猜 TDD 表现会差，猜对了吗？单看结果，确实如此。但就我的推理逻辑而言（虽然没有事先书面记录下来，不过我知道我当时怎么想的），答案并不那么明确。我的思路大概是：正如我们最近在 这篇、那篇以及 多个场合讨论过的，让 agent 真正把事情做对而不是单纯 overfit，是取得良好性能或准确率的关键所在。就方法论本身而言（不涉及这条指令具体如何改变了 agent 的行为），TDD 似乎天然容易引发 overfitting。
Agent 确实写出了质量较差的测试，有时还采用了成本较高、效果不佳的迭代式工作流，但我不确定这里真正的问题是否是我预期中人类使用 TDD 再指挥 Agent 实现时会遇到的那个失败模式——我的直觉本来正是来自这一点。这里的推理可能接近、也可能不接近问题的实质；我认为需要更多的评测和调查才能下结论，而且我猜更多数据很可能会证明我原来的推理是错的。Spin
Spin 是一个模型检测器。
现在进入了一个成绩接近平均水平的区间。Spin 在 medium 和 xhigh 两个档位上都略低于平均水平，成本也低于平均。和其他形式化工具一样，Agent 对 Spin 的使用总体上没什么效果。具体来说，用 Spin 对某类行为建模，与是否通过覆盖该行为的隐藏测试之间没有任何相关性。对 Spin 的使用流于表面，没有产生实际价值。
Hegel
Hegel 是一个基于 Hypothesis 的属性测试库。
正如现在大家可能已经预料到的，Agent 也没能有效地使用 Hegel。即便用了，也只是停留在表面，而且通常是在大量依赖普通测试之后才想起来用它。反复说“Agent 没有真正用好这个工具”就很啰嗦了，所以这几节我会写得简短些，只提一些特别值得注意的地方。
Agent 实际的工作流程大致如下：
- 阅读 RFC 和 API/契约文档
- 实现 Zstd
- 运行常规测试
- 阅读 Hegel 文档
- 用 Hegel 写 1-4 个简单的属性测试
- 继续用 Rust 自带的常规测试
如前所述，Hegel skill 并没有提升正确性。正确性反而更差了（不过差距不大，也可能只是随机波动）。更引人注目的是成本明显偏高（medium 上高出 26%，xhigh 上高出 41%），而且原因看起来是因果性的。
该技能促使 agent 生成了更多测试，但新增的测试大多是对畸形输入不触发 panic 的校验和 round-trip 测试。前者本身 agent 在所有 property-based 和 fuzzing 场景下就已经倾向于过度生成了，再多写也没太大意义。后者倒不算什么坏主意（我自己也经常明确要求 agent 写 round-trip 测试，用来验证特定属性时确实有用），但问题是它没有落在最容易出 bug 的地方。在没有额外指令的情况下，agent 倾向于对那些本身就大概率正确的平凡属性去写 round-trip 测试。
关于成本，原因有好几个。首先是技能体本身相当大（技能内容 34k 字符，还会加载一份 45k 的 Rust 专用参考文档，加起来超过 20k tokens）。这些内容在运行开始时就被加载，之后在大量后续动作中反复重读。结果就是 medium 级别平均多出 16% 的费用，xhigh 级别多出 18%（按原始 token 算，medium 平均多了 900k，xhigh 多了 1.8M；虽然这些内容的缓存命中率非常高，初始加载之后达到 99.85%，但重读次数足够多，占到了总成本相当大的比例）。
还有一个乘数效应（包含在上述数字里）：该技能还规定了一套结构化的操作流程，导致要完成的工作量大幅增加。但这些额外工作并没有带来正确性上的提升，等于花了钱却没得到对应的收益。
值得注意的是，该技能在 160 个案例中"仅"被使用了 157 次。用 LLM 时情况通常如此——行为和结果都有随机性。如果你认为某个 agent 应该在特定任务上使用某项技能，它到底用不用，取决于一些对 AI 实验室以外的人来说很 opaque 的因素。
ToB 技能
在这种情况下，160 次运行里只有 108 次真正打开该技能文档去阅读。技能建议在 Rust 中使用 proptest，但文档同时要求新增依赖需经审批，而这些运行全都是单轮自主执行模式，所以这一步没有被执行。
与其他 property test 用例类似，property testing 的用法非常初级，也没有真正起到作用。
Rstest
Rstest 是一个基于 fixture 的测试库。
Agent 实际上基本没有使用 rstest。严格来说它们确实调用了，但只是在 rstest 里写了普通单元测试，完全没有用到 rstest 的核心能力，等于白用了。前面提到的其他技术在表面上至少还有使用（比如用 Hegel 写了一些低价值的 property test），但 rstest 这里彻底不是——它们完全没用到让 Rstest 成为 Rstest 的东西。打个比方，这就好比给 property-based testing 库只写非 property 的单元测试，完全偏离了该库的设计初衷。
Rust test
指的是 Rust 内置的测试框架。Agent 在 Default 条件下主要使用它，在其他条件下也大量依赖。
明确要求 agent 使用内置测试框架后，测试数量确实增加了（medium 档翻倍，xhigh 档多 25%），但正确率并没有提升。Agent 出错时，往往是因为没有覆盖关键行为，或者测试本身的预期就写错了。多写测试并没有实质性地提高对高风险行为的覆盖，也没能减少编码了错误行为的测试占比。
Yossi Kreinin 补充道：
我觉得固定的输入/输出式测试会让机器和人类都陷入同样的陷阱。如果你自己生成输入，就得再写代码来判断输出对不对，虽然这段判断逻辑本身可能有 bug，但至少会逼你想清楚"正确"到底意味着什么、怎么判定，比直接跑一遍就假设输出没问题要有意识得多。但如果是固定输出，你很可能会把代码跑出来的结果原封不动写进去，然后说服自己"这看起来合理"。
Creusot
Creusot 和 Verus 处于同一赛道。
和其他形式化验证条件一样，Creusot 也没有被有效使用。
Mutation testing
变异测试是指修改代码来检验测试的有效性，然后补充测试以达到良好的覆盖率。虽然变异测试是一个标准的编程术语，但 agent 通常并没有真正做变异测试，而是做普通测试、只是偶尔以某种算不上变异测试的方式改动一下代码——就像 TDD 指令确实改变了行为、但没能让 agent 真正实践 TDD 一样。
确实有少数几次出现了真正的变异测试，但数量很少，属于罕见情况。
自主判断
这个条件要求 agent 根据自己的判断灵活选用合适的测试方法。鉴于前面看到的情况，毫不意外，agent 基本都用的是标准的 Rust 单元测试。少数 agent 做了一些有限的 fuzzing。虽然它们可以使用其他测试库和形式化验证库，但都没用上。
Fuzzing
Fuzzing 是以某种方式随机化测试输入的做法。
agent 主要靠发送随机字节，但这大多只是反复走同一条代码路径（无效输入）。它们也会尝试发送有效输入的随机变体，但结果大多同样只是反复触发输入拒绝的路径。
在极少数 agent 生成随机结构化输入的情况下（160 个案例中有 10 个），一半都能发现真实 bug，其中不乏非平凡的案例。160 个案例里只有 5 个比较有效地用了 fuzzing，这算不上好，但已经是我们目前见过的技术运用中效果较好的之一了。这也表明 agent 完全可以被训练得更好，而且不需要重新训练、只需引导就能做得更好。从某种意义上说，它们是会做这些的，只是没人推一把的话通常不会真的去做。
Insta
Insta 是一个快照测试（snapshot testing，有时也叫 golden testing）库，做法是把结果与正确结果的"快照"或"golden 文件"进行比对。一般来说，快照通常是某种序列化数据，比如数据结构对应的 JSON 对象、CLI 输出的日志等。
可以想见，快照测试几乎没被用到，agent 大多还是依赖传统测试。它们确实用了 Insta，但往往只是在 Insta 里写普通的单元测试。
SMT
指示 Agent 使用 SMT solver，环境中已安装 Z3、cvc5 和 Yices。
Agent 大多把 SMT solver 当作草稿纸，用来算 FSE 状态范围、头信息运算之类的内容。即便确实建了模型，也往往没建模到该避开的常见坑点上。
比如，某处运算本应是 byte1 + (byte2 << 8) + 0x7F00，不少 Agent 却写成了 byte1 + (byte2 << 8) | 0x7F00。它们用 SMT solver 证明了该运算的相关性质，但最终还是写错了代码，使得 SMT 的使用效果看起来与 Default（无额外指令）没有差别。
TLA+
TLA+ 是一种用于建模系统行为的语言和工具。
这一档属于"略高于平均"的组（但仍不及 Default），不过如前所述，具体排名不必太当真。虽然未必有统计学意义，TLA+ 在 medium 难度上略高于平均，在 xhigh 难度上则高出更多。
160 个 Agent 中有 159 个建了某种 TLA+ 模型，通常是 Zstd 的状态机模型。就覆盖面而言，有 30 个对 Huffman/FSE/熵编码建模（这些区域常出 bug）。与其他形式化方法类似，TLA+ 建模往往发生在流程较后期（大量常规测试和实现之后）。Agent 偶尔会在 TLA+ 模型中发现并修正错误，但没发现哪个 TLA+ 问题真正导致了 Rust 代码的修改。
虽然确实能看到一些像模像样的 TLA+ 建模，但若它改善了正确性，改善幅度也很小、难以察觉。总体来看，TLA+ 建模更精细的运行并没有更高的正确率。
Metamorphic testing
变形测试的思路是：验证相关联的输入是否产生具有预期关系的输出。例如，对排序函数，交换不相等元素的输入顺序不应改变输出的相对顺序；对加法，给输入加上某个值后，输出也应加上该值（溢出取模）。
正如我们在其他条件下所见，蜕变测试在正确性方面并没有发挥太大作用。确实验证了一些合理的性质（比如，在帧边界插入可跳过的帧不应改变输出、合法的块重划分不应改变输出等），但这些性质并未覆盖 agents 频繁出错的地方，因此验证它们也无济于事。总的来说，agents 似乎成了那个老笑话的忠实粉丝：
一个警察看到有人在路灯下翻找什么东西，便问他丢了什么。他说丢了钥匙，两人便一起在路灯下找。过了几分钟，警察问他确定是丢在这儿吗，他说不确定，钥匙其实丢在公园了。警察问那他为什么在这儿找，他答道："因为这儿有光。"
有趣的是，xhigh 条件下使用蜕变测试的次数反而比 medium 更少。
ECC
ECC 的 Rust 测试 skill 表现尚可，但很大程度上是因为 skill 的大部分内容被忽略了。agents 通常会打开并阅读该 skill（160 个中有 153 个读了），这似乎促使它们生成了更多测试。不仅这个条件下测试数量更多，而且如果我们按 agents 阅读 skill 的时机来区分（早读、晚读、从未读），测试数量的增加也呈现出一种随暴露程度递增的梯度。
虽然 ECC 的得分与 Default 几乎持平，但从 agents 暴露于 skill 程度越高、表现越差这一趋势来看，我倾向于认为这只是巧合。agents 越早阅读该 skill，行为受其影响越大，正确性结果反而越差。
ECC 的原始分数看起来还不错，原因在于：7 个没有读过该 skill 的 agent 表现异常出色，全部 100% 正确；另外 9 个很晚才看 ECC、几乎没受影响的 agent 也表现不错，同样 100% 正确。这也解释了 ECC 的一个反常现象——medium 档的分数和 xhigh 一样高（上面提到的那些 agent 没怎么读 skill 的运行，几乎都发生在 medium 档）。确实，skill 何时被调用可能存在某种偏差，但从整体模式来看，ECC 并不有效——除非你认为 ECC 是个幸运符，能在 skill 没被真正使用时提升成绩，而这更可能发生在低 effort 档位。
当然，agent 不应该被它们没看过的 skill 影响，我们应当只统计真正使用了 skill 的情况。如果只看 skill 实际影响 agent 的那些案例，ECC 得分低于平均水平（介于 Rust built-in framework 和 Creusot 之间），失败模式也和 Rust built-in framework 很相似：生成了大量琐碎且没有意义的测试。该 skill 要求 agent 采用 red-green TDD。agent 的行为大概算不上 TDD 实践者眼中的 TDD，但它们确实会在实现功能前先写个小测试，结果就是测试数量很多。如前所述，这对 agent 来说并不是有效的开发方式，所以结果反而不如不给出任何指令和 skill。
顺带一提，正如我们试用 Caveman mode 时发现的，这类实验方差很大，人们常常因为几次小规模运行就误以为某个 skill 有用。而这次我们对一个 skill 做了 160 次运行——数量相当大，超过任何理性的人会做的程度。可即便如此，单看分数，ECC 表面上还是显得不错。
要消除 LLM 固有的噪声，我们需要多得多的运行次数。像本文这样人工检查结果当然可行，但人们在讨论公开 LLM 基准（无论涉及技能还是其他方面）时很少这么做。我确实试过让 LLM 来分析结果，但一如既往，即便是当前公开的 SOTA 模型，分析质量也差得离谱，充斥着基础的推理错误。更多时候，我只是看到人们传播一个表面数字，哪怕从最基本的统计角度看它毫无意义；更糟的情况是，基准本身就有致命缺陷，正如我们在 Senior SWE-Bench 中所见。
Default
Default 未给 agent 任何测试或验证指令。
鉴于此前的表现，Default 得分高于平均水平并不令人意外。当被要求使用特定库或特定测试技术时，agent 往往做了些没用的事。道理很简单：不告诉 agent 去做无用功，效果自然比让它去做无用功要好。
Audit
Audit 要求 agent 在实现完成后审查代码。160 个 agent 中有 152 个确实执行了审查，其中 151 个声称发现了问题并据此做了修改。agent 选择的审查区域通常合理，但很少会在全新上下文中做独立审查（我通常会要求 agent 这样做），往往只是在审查时重复了实现阶段已经犯过的错误。
42 个运行使用了独立 agent，但这些运行的得分反而更低（不过这未必是因果关系，agent 可能是在更困难的情况下才决定派生一个独立审查的）。Audit 在 xhigh 上的正确率最高，但在 medium 上低于平均水平，而且所有审查操作都显著推高了成本，尤其在 xhigh 上。总体而言，Audit 的表现与 Default 大致相当，无法确定它在 xhigh 上是否真的更好、在 medium 上是否真的更差。这听起来合理，但我觉得现有证据还不足以下此结论。
Em Chu 的评论如下：
这里的结论与我的经验一致。目前我大部分 token 都花在了代码审查上，因为我发现它非常有价值。不过我始终会给出两条指令：
- 不要派生子 agent，自己读代码/diff 并理解
- 不要执行任何代码
因为我发现，一旦允许 LLM 做上面任何一件事，它的表现都会明显变差（当然，我并没有做过量化测试……）。默认情况下，LLM 几乎不会主动阅读或推理代码，哪怕我做的改动远未超出它的 context window。
我通常还会加一些"虚话"，比如"要对抗性地思考""考虑功能的所有可能组合""审视整个输入空间"，但这些是否真的有帮助，我并不确定。
试着做一下确实会很有意思，但正如我最近几篇文章中提到的，我在刻意减少文章中的细节展开，这个话题或许留到下一篇再谈。
对高风险区域做审计和 Fuzzing
对于 Zstd，当 agent 遵循这条指令时，它们会把大量注意力集中在 FSE、Huffman、bit reader 和状态管理上。这些区域恰好是 agent 最容易漏掉问题的地方，所以它们的判断是对的——确实风险更高。针对性 Fuzzing 选的目标区域也比通用 Fuzzing 条件更合理。
在 medium effort 下，agent 基本忽略了这条指令；到了 xhigh 才真正照做。这个条件并没有表现很差，但也没有比不加指令时更好。
观察 agent 的实际行为，一个常见问题是：它们往往只是生成一堆随机输入，而这些输入大多是无效的，根本触及不到任何有意义的边界条件。
人类测试人员在生成随机测试时，通常会刻意引导随机过程去命中"有意思"的输入，但 agent 做不到这一点。Agent 对输出的检查也做得很不到位，很多时候只盯着有没有 crash。Fuzzing 本身就和"只看 crash、不验证属性"挂钩，所以这倒不算太意外；但如果是在测一个 Zstd 实现，人类测试者大概率不会只满足于查 crash。
要求零失误
虽然这个条件在分数上略高于 Default，但实际行为并没有显著差异，分数差距也很小；我倾向于认为这只是随机波动。在我查看结果的每一个层面，它与 Default 的随机抽样结果都难以区分。
Kani
Kani 是一个 Rust 模型检验（model checking）库。
就“真正在最终执行的代码上使用形式化方法”而言，Kani 的覆盖情况最好，因为它确实被用在了 Zstd 代码上。不过这种情况只是偶尔出现，大多数使用都很表面化。
有一次，真正使用 Kani 发现了一个不小的 bug，并促使 Rust 代码做了修改。160 次里只有 1 次算不上亮眼，但这至少说明 agent 有时能摸索出 Kani 的合理用法（我猜测，这意味着如果在 RL 环境中使用，模型可以学会更有效地使用 Kani）。
Kani 的成本明显高于其他条件。原因似乎在于反复读取 Kani 输出的开销很大，导致输入 token 成本居高不下。
ACL2
ACL2 是一个定理证明器。这里需要注意的是，在很多情况下 ACL2 都发生了 OOM（超出 192 GiB 内存上限）。OOM 的结果没有被计入统计，这对结果的偏差影响难以估量。
虽然 ACL2 的得分比 Default 高，但我认为这很难说是因果且显著的效果。和几乎所有其他形式化方法一样，ACL2 大多被用来证明一些对正确性没有实质影响的东西，所以很难理解这为什么会提升正确性。
在这么多不同条件中，除非其他条件的表现严重退化，否则 Default 和效果上等价的 Make no mistakes 本不应该排在最前面。
Proptest
Proptest 是一个基于属性的测试（property-based testing）库。
和其他随机化测试一样，大多数测试都不太有价值，而且过度依赖随机性导致覆盖率很差。
尽管基于属性的测试总体用得不好，但 proptest 的 shrinking（缩小到更简单的能触发测试失败的输入）确实偶尔带来一些价值，这已经比大多数其他方法几乎毫无价值的表现要好。
Property-based testing
和其他基于技术的方案一样，agent 的容器里预装了所有可选工具。每个 agent 都选择了 proptest，所以这个条件实际上变成了第二个 proptest 条件。
和 proptest 条件一样，测试大多写得不好，但确实有时能发现 bug，shrinking 也带来了一些成功案例。
有点意外的是，这个第二组"偶然"冒出来的 proptest 分支同样远超平均水平，和 proptest 本体表现几乎一致。
Skill
这里的 Skill 指我为了测试"拥有一个简单 skill"这一场景专门写的那个 skill（而非我之前让 agent 去搜索相关测试技能时，它返回的那些大而复杂的 skill）。
也许我本来应该用 skill，但我一般不用，而是靠多轮 prompt——先看看效果，再追加指令。因为完全没有实践过，我对"什么才算一个好 skill"毫无直觉。Max Bittker 建议试试用一个测试 skill，把我脑子里关于测试的一些经验编码进去，看看效果。看到结果后，他来了句"我早就说过吧"。
我没有提前写下对这个结果的预测，但我心里的预判是：这大概率不会好使。回想 2015 年我尝试把这些经验用文字传达给其他人的那次经历——坦白说基本是失败的——我并不擅长把"该怎么测试"用文字明确地写出来。我倒是可以坐下来给人现场演示，通常一次就能让人"开窍"，把他们变成远超平均水平的 bug 猎手，但"通过演示来传达"和"用文字写清楚怎么做"毕竟是两种能力，而且前者容易得多。
具体到这次，那个 skill 的内容是：
- 动手实现之前，先预判哪些地方容易出隐蔽 bug；对每个地方列出可能的错误和合理的歧义解读，然后设计一个能区分不同结果的检查点（优先用边界两侧的非对称用例）
- 实现完成后，对高风险区域，脱离生产代码上下文独立重新推导结果并对比（用全新上下文，不复用已有的辅助函数）
- 条件允许时，用 property-based testing 或随机输入来探索空间，尽量把精力花在"不 panic / 不 crash"这类基础随机化上而非更深层的验证
- 做随机化时，偏向能触发有趣状态和代码路径的输入（别只是简单随机然后全掉进同一条错误路径）；必要时需要构造结构化的随机输入
- 如果对细节不确定，用独立的推理来验证哪条路径是对的（换个新上下文，不要复用辅助函数）
这条指令得分最高，但实际效果并不理想。agent 几乎从未真正切换过新上下文，所以那条指令基本是摆设。我们也不确定"独立推理"这个思路本身是否有效——是应该优化措辞来促使 agent 更频繁地执行，还是干脆去掉（虽然理论上存在一个"最优频率"，但我非常怀疑 agent 恰好就在那个频率上）。
在"审计与模糊测试高风险区域"一节中，我们发现 agent 似乎知道如何识别高风险区域。这里也不例外，但"知道"并不等于"做对了"。例如，agent 识别出 Zstd 中编码和解码的位流顺序可能搞反是高风险点，但在覆盖该逻辑的测试上表现并未更好。具体来看 medium 第 35 轮，某个 agent 确实识别了该风险，也做了独立推导和审计，结果仍然失败了。它写了一个相关测试，但输入恰好是回文的，所以无论顺序是否搞反结果都一样——一个把顺序写反的有缺陷实现也能通过。
另一个问题（如果算问题的话）是，所有 fuzzing / property-based testing 都是"手写"的。既然 agent 用 proptest 表现尚可，而 proptest 本身也有不少可以利用的机制，那只要指示 agent 使用 proptest，这方面的能力应该能轻松提升。我们确实给 agent 加了指令，试图减少那种"生成大量无用的、太随机的测试"的典型失败模式，方向上起了作用——确实有更大比例的 agent 写出了有点意义的测试，但质量仍低于我预期的人类水平（或有人类实时指导的 agent）。在没有反复迭代的情况下，我不确定什么通用指导才是好的（相比之下，花几分钟看看 Zstd 的结构再给出针对性指导，在其他问题上倒是效果很好）。
作为一版用来继续迭代的初稿，我觉得这个 skill 不算太差，但也谈不上能用。如果用更多样本来改进它，确保不会过拟合到 RFC 类问题或位运算密集型问题这类场景，或许能跑通。但我平时不怎么写 skill，也从来没迭代过，所以它没能捕捉到我或其他人在真正驱动 agent 时会怎么做。
我的习惯是先给 prompt，再看结果（不一定是看代码，至少看看 agent 说自己做了什么、某种形式的任务总结，以及实验类工作中部分实际结果），然后据此再给下一轮 prompt。所以我不习惯把信息前置，这与根据反馈调整是完全不同的问题。之前做过 fuzzing，我知道 agent 常见的失败模式，这个 skill 本意就是预防这些问题。但即便只是偶尔回头检查一下，也比完全靠事前约束容易做到，事实证明前置的指令并不足以阻止那些典型失败模式，虽然多少有缓解。
总体评价
如前所述，我没有把数据整理成清晰易读的形式。因为一旦看 agent 实际做了什么，会发现它们大多效果很差，比较「把 Verus 用得很糟的 agent」和「把 QuickCheck 用得很糟的 agent」的表现如何，其实没什么意思。有一点稍微有意思：让 agent 识别有风险或容易出现隐蔽 bug 的区域时，它们是能做到的。
但总的来说，不管建议用什么库或什么技术，agent 都没有真正用起来。如前文所讨论，只是让 agent"测试一下"或反复要求它多测，效果都很差。结果发现，让 agent 使用具体的测试技术（其中一些我个人觉得很有效）同样收效甚微。我随手写的那个简易 skill 似乎能稍微改善一些，但要真正有用，远不止我花的那两分钟。Yossi Kreinin 评论说，软件测试的现状一塌糊涂，所以 agent 退化到训练水平时结果不好也不意外——这正是我们观察到的。
不知什么缘故，agent 用 proptest 时表现稍好一些，但测试水平远不及一个读过 proptest 手册、并得到测试方向指引的普通开发者。我很好奇，如果给 agent 更多方向性指引，它在 proptest 上是否比在其他库上更有效，不过这值得另开一篇——我平时赶着半小时出稿，这里已经快写到 9000 词了，早就超出半小时能打出来的合理量了。
怎么让 agent 写出好的测试？
我的经验是：如果你先引导 agent 搭好一个合理的测试与分诊结构，之后让它在此基础上做增量，不需要大量人工盯梢，效果还算可以。受我自身背景（或偏见）影响，我更倾向于随机测试、模糊测试或 property-based testing 这类方法。
我和 Jamie Brandon 聊过这个话题，他在 snapshot testing 上也遇到了类似的情况。他提到，在一个项目里，他让 agent（用了多种模型）做 snapshot testing，agent 嘴上说在做，实际上根本没做——写个单元测试就宣称自己写了 snapshot test。在另一个项目里，他成功让 agent 写出了合理的、带 mock IO 的端到端测试，但前提是把测试挪到独立的 crate 里，并在 AGENTS.md 中写明：测试必须放在该 crate 内，不得修改公共接口。
至少到目前为止，相比 Jamie，我更多是倾向于让 agent 来写测试代码（我的习惯是在 CLI 里跟 agent 打字交互；至少眼下，他比我更习惯手写代码），但具体怎么做其实无所谓，关键是要搭好某种合理的结构。