代理在多大程度上运用了测试/验证技术？

我们之前提到，虽然让编码代理使用有效的测试技术比以往任何时候都更容易达到特定的质量标准，但软件质量似乎在下降：/ai-coding/，这表明开发者使用的默认设置可能并不太有效。在这里，我们测试简单地指导代理使用特定技术或库是否能提高实现的正确性，作为一种测试，看看当由没有测试经验但可能听说过应该应用某些技术或使用特定库的人指导时，代理的效果如何。

我们将重新使用在这篇关于代理程序语言效果比较中讨论的 Zstd 实现评估：/pl-tokens/，而是比较在给代理提供实现 Zstd 的提示时，不同测试技术和测试库的表现，以及不同附加说明，如“使用测试驱动开发”、“使用 Lean 4”、“使用 QuickCheck”、“使用基于属性的测试”等。我还运行了一些其他评估，例如 IMAP RFC 的评估，这里会简要讨论。

我事先登记了一些关于各条件表现的猜测：

下面，我们有一张非常杂乱的图，显示了测试条件的结果（codex 配合 GPT-5.6 Sol，使用 medium 和 xhigh 努力）。在查看数据时，我倾向于偏好比大多数人更加密集和杂乱的图，例如这里的第一张图：/android-updates/。因为大多数人会觉得这种图杂乱到难以阅读，所以我在向他人展示信息时，倾向于将信息拆分成一系列图表，每张图显示较少信息。出于下面讨论的原因，我在这里不会这样做，仅仅展示这张极其杂乱的图，其中 x 轴为成本，y 轴为通过 100%（隐藏）测试的运行比例，取每个条件和努力下 80 次运行的平均值（鼠标悬停在项目上显示 bootstrap 协方差，50% 不确定性：https://statmodeling.stat.columbia.edu/2016/11/05/why-i-prefer-50-to-95-intervals/，并尝试让相似的事物颜色相近，例如正式方法用蓝色调，基于属性的测试用绿色调等）：

我们可以看到的一点是，没有任何一种方法表现特别出众。然而，默认（没有额外指令）表现明显高于平均水平。看看xhigh，平均来看，与形式化方法相比，模糊测试和基于PBT的条件表现略好，而在中等水平时情况则更加混合。测试相关技能codex推荐我们尝试的方法表现欠佳，尽管我们的快速自定义技能表现尚可（一个主要区别在于我们的技能旨在引导远离默认行为，朝更有效的行为发展，而其他技能更像是教程）。TDD表现不佳，如预期（有一项技能还建议代理使用TDD，而在代理尝试遵循指令的情况下，该技能也表现不佳）。

如果我们仔细看看代理所做的事情，很快就会发现，通常来说，代理并不擅长使用这些工具或技术。正如我们在这里所指出的：/ai-coding/，以及所有我交流过的人也指出的那样，代理在测试方面表现非常差，而且似乎默认情况下并不理解如何合理地进行测试。例如，这是Gary Bernhardt的评论：https://x.com/garybernhardt/status/2067002665427775613：

AI代理对测试的做法，大致如下：

采用十五年前某人反对mock的病态案例，而这个人实际上从未真正使用过mock。天真地梦想过度使用mock。

将这些病态情况作为测试策略的骨干。

在xhigh上，代理通常能够让它们编写的测试通过，但它们写的测试质量很差（例如，它们会向一个使用四个比特流的功能测试提交四个相同的比特流，并因此错过由于比特流顺序错置而产生的任何错误）。正如我们之前在Zstd评测中关于语言方面所指出的：/pl-tokens/#appendix-medium-in-a-loop-vs-ultra，使用低强度在一个简单循环中运行会得到更差的结果（代理会做更多这种操作，并且正确性下降时容易停滞）。

下面我们将按条件查看代理的操作情况，从正确率最差到最好排列，但我建议任何人都不要根据这个顺序得出任何强有力的结论。

这里的许多失败似乎类似于我们在研究编程语言对令牌使用和正确性的影响时看到的失败：/pl-tokens/，因为这些失败通常是特殊情况。例如，在编程语言方面，我们发现代理在 Clojure 中对字节转换语义的理解错误率相当高，但在 Java 中却不如此，尽管代理“应该”（也可能某种程度上确实知道）通过使用 unchecked-byte 而不是 byte 可以获得 Java 字节转换语义。

Verus：https://github.com/verus-lang/verus 使用 SMT 求解器和各种类型的推理来证明代码符合规范。

虽然 Verus 可以证明代码符合规范，但代理没有这样做。相反，他们对与 Zstd 相关的各种抽象属性进行了证明。我自己没用过像 Verus 这样的工具，所以无法说明专家甚至初学者通常会做什么，但从阅读教程来看，我觉得奇怪的是代理没有尝试使用 Verus 来验证任何实际代码，而只是用它进行抽象推理，因为它似乎旨在使证明实际代码属性变得容易。

此外，如果我们看看所证明的属性，通常证明的属性很少，并且所证明的属性并不有趣。例如，代理会证明诸如“在给定有效的光标/索引/距离的情况下，结果操作保持在边界内”，这类证明并不坏，但实际上并不是错误的来源。此外，代理经常编写空洞的证明，实际上是 A => A。一个实际的 Verus 证明的例子是：

在代理实际上证明某些东西的情况下，他们通常证明相对简单的内容，并避免证明那些可能有错误的部分的属性（例如，代理经常未能反转 encode 和 decode 的比特流顺序，并且会编写无法检测此问题的测试，因为测试是回文的；也许在这里进行某种反转的证明可能会让代理以不同的方式“思考”这个问题）。

当仅提供 Verus 和 Verus 文档时，似乎代理并没有从 Verus 中获得价值。

如果我们看结果，总体来说 xhigh Verus 的结果还可以（正确率略低于平均值，但成本要低得多）。medium 的结果成本一般，但正确运行的百分比最低，平均正确测试数量也最低。由于代理实际上并没有从 Verus 中获得价值，它们为正确性所做的工作主要是传统测试（内置 Rust #[test] 函数的单元测试）。从 medium 提升到 xhigh 时，代理在传统测试上花了更多的精力，而在使用 Verus 上只增加了一点点努力，这使得 xhigh 的结果还可以。

看实际测试，对于两个 Verus 代理表现较差的功能之一（四流跳表：https://github.com/facebook/zstd/blob/dev/doc/zstd_compression_format.md），Verus 代理在 160 个案例中写了 89 个测试，巧合的是，与 Default 代理数量完全相同，但 Verus 代理更容易写出糟糕的测试。他们更可能在测试中编码错误结果，以及制作容易通过但覆盖不充分的测试，例如让四条流完全相同。我所说的失败是特异性的，就是指这种情况。Verus 本身并不必然导致在不使用 Verus 时写出糟糕的测试，我们通常也不会期望使用 Verus 的人写出不好的单元测试，就像我们不会期望使用 Clojure 的人在字节转换上犯更多错误一样，但出于某种原因（可能是巧合）这里发生了这种情况。

我不知道 AI 实验室内部的人是否能得到关于事情为什么发生的更好信息，但在外部，一般很难判断这种情况的发生原因（即使我们对语言问题提出了一个合理假设，也需要运行很多语言的不同样本，而我们参考的研究同一问题的论文没有观察到语言流行度与代理有效性之间的相关性，因为它们要么研究的语言太少，难以推断这种微弱相关性，要么研究的问题过小、过于简单）。

Alloy 通常被称为有界模型检查器。对于 Alloy 6 来说，这种说法可能不完全正确，因为它引入了一些额外的功能，但这超出了我的专业知识范围。我的理解是，使用 Alloy 时，你通常是证明模型的性质（而不是证明你的代码能够正常工作）。

Alloy 的正确性得分是第二差，并且与往常不同，它在中等和极高复杂度上的表现普遍较差。虽然未显示（因为似乎没有增加任何信息），总体来看，最大复杂度和极高复杂度的结果高度相关，而它们与中等复杂度的结果有较大差异。

正如我们在 Verus 中看到的，使用 Alloy 的代理几乎完全依赖标准的 Rust #[test] 来验证正确性，并且大部分时间都在摆弄 Alloy。再次强调，糟糕地使用形式化工具并没有帮助提高正确性。

有个别 Alloy 使用案例接近发现问题或风险，但即便如此，数量也很少。在一个案例中，Alloy 找到了一个反例，这促使代理实现了 Rust 版本，并对潜在 bug 进行了缓解。不幸的是，这个反例依赖于 8 位溢出，而实际实现使用的是 64 位 usize，对于给定输入不可能发生溢出，因此它只是增加了代码的复杂性，而并未防止实际的 bug。

在另一个案例中，Alloy 规范不正确，相关测试失败。测试失败后，代理修正了 Alloy 规范。如果规范本身是正确的，也许代理就会在没有失败的情况下编写正确的代码。有一些情况可能发生了这一良性过程，但不清楚是否真正避免了潜在的 bug。

Alloy 代理确实对与 Zstd 算法更紧密相关的对象进行了建模，而不同于 Verus 代理（后者主要检查算术等内容），但这仍然是错误的建模。

差异测试是一种技术，你将相同的输入提供给多个实现，然后比较结果以发现问题。从原理上讲，这似乎是对大型语言模型尝试的一种合理方法，因为我们通常会从不同的尝试中得到不同的结果，正如我们在这里指出的：/pl-tokens/#appendix-medium-in-a-loop-vs-ultra，让一个代理更多地迭代某个实现（可能只是整个程序的一部分，甚至可能只是某个函数的一部分）通常不如让代理从头开始重新启动。

但这给我们带来了第三差的结果。在这种情况下，我们在 xhigh 上的结果略高于平均水平，而在 medium 上的结果远低于平均水平。没有代理创建两个完整的实现进行比较。在 160 次运行中，有 135 次可以算作做了差异测试，但像我们看到的其他情况一样，这些测试通常很简单，实际上没有什么用处。而且，在差异测试可能捕捉到漏洞的情况下，代理并没有以独立的方式实现功能，而只是做同样的事情两次，并在两个版本中编码了相同的漏洞。

我有时会告诉代理独立地执行任务，并让它们在不同的上下文中启动，但这种方法在差异测试中没有有效执行，代理通常只是写了两次相同的东西。

讨论官方 Hegel 技能如何改变 Hegel 的行为是有意义的，但按正确性逆序排列时，Hegel 技能似乎排在 Hegel 之上，因为结果在正确性上更差。有关该技能的讨论，请参见下面的 Hegel 部分。

Lean 4 可以描述为一种交互式定理证明器：https://en.wikipedia.org/wiki/Proof_assistant。

虽然我没有对 Lean 提出预注册的猜测，但如果我预先注册了关于哪些形式化工具表现良好的猜测，我会把 Lean 放在我预期表现良好的列表中，因为它相对热门/流行，因此由于 RL 环境中的合成数据，它看起来相对可能具有良好的性能。

Lean 代理确实证明了属性，例如 Verus 条件，代理大多数进行的是算术证明，这些证明没有触及容易出错或有风险的领域。

像其他形式化条件一样，Lean 代理在很大程度上依赖标准的 Rust 测试。正如迄今为止的形式化条件那样，做一些不重要的证明并不能提高正确性。

QuickCheck 是一个基于属性的测试库：https://en.wikipedia.org/wiki/Property_testing，可能长期以来是最知名的此类库，尽管 Hypothesis 目前可能占据这一地位。

不幸的是，代理在使用基于属性的测试时的效果与他们使用迄今为止看到的形式化工具一样有限。在使用 QuickCheck 时，代理主要编写非常简单的“冒烟测试”，几乎没有进行检查。他们还使用随机输入，而当完全随机时，对于测试像 Zstd 这样的东西效果很差（因为它们只是进入几条失败/拒绝代码路径之一）。

此外，被检查的属性相对较少。虽然所有代理都使用了 QuickCheck，但在 160 次运行中有 63 次仅检查了单一属性。代理再次主要依赖传统测试，尽管技术上他们确实使用了 QuickCheck。出于某种原因，代理实际上编写了比默认条件或大多数其他条件下更多的传统测试，但进行了更少的测试-修复迭代（这使得该条件的成本低于平均水平）。

TDD 在此处的表现不如人意，就像在 IMAP RFC 评估中一样。

TDD 提示似乎导致代理行为发生了巨大变化。代理生成了两倍数量的测试，并采用更迭代的测试-代码-测试-代码等工作流程，尽管 TDD 拥护者可能会说代理实际上并没有使用 TDD。只有少数情况下，代理进行了一些细粒度的迭代 TDD。

总体而言，代理事先编写了更多测试；例如，在进行实质性（非存根）实现之前，在 160 个案例中有 67 个案例中代理有一个或多个失败的测试，而默认条件下是 0 个案例。

对于广泛的测试类别，TDD 有更多各种类型的测试。有更多的小型、琐碎的测试，同时也有更多的集成测试和端到端测试。任何明显的高层次“代理做了太多或太少的 X”似乎都不符合数据。如果我们查看具体的失败以及它们是如何被测试遗漏的，可以观察到 TDD 条件下也存在这些情况。例如，当有四个哈夫曼流时，Zstd 使用了一种称为跳转表的东西。

虽然 TDD 代理写了更多覆盖一般情况的测试，但他们更有可能在此类情况下未通过 eval 测试。由于某些原因，TDD 代理更有可能编写不覆盖难处理情况的测试（例如，使四个流完全相同然后也使它们很简单，就像我们在 Verus 中看到的那样）。这是另一个让我好奇的问题，即 AI 实验室的人能看到什么样的情况，因为从外部来看，为什么用 TDD 训练代理会让他们写出更差的测试和实现并不明显。

如果我们只有 TDD 和一些测试条件可用，一个假设可能是，TDD 编写的代码通常似乎有很多不太好的小测试，因此也许用 TDD 训练代理会导致他们编写更多这类无效测试。但为什么在 Verus 中也会看到相同的模式则不明确。如果我们在一个开放模型上重新运行实验，并检查模型内部实际发生的情况，或许可以判断 TDD 是否存在相同的问题，或者是否存在 Verus（或其他）行为的共同原因？

还有两项技能也导致代理采取更迭代的方法，也许理论上认为更频繁地执行会得到更好的结果，而这两项技能的表现也不佳。一般来说，在所有条件下，代理能够让他们编写的测试在 xhigh 和 max 上通过（未显示，但 max 的正确率略高于 xhigh，而且成本明显更低）。更迭代地使自己的测试通过往往会导致代理编写更多不正确的测试，这些测试会强制执行错误的行为。

Yossi Kreinin 对于为什么 TDD 可能导致测试更差有这样的想法：

仅供参考，我认为如果你在写代码之前先写测试，会更难测试那些难的情况，因为你对什么会困难了解得少。即使你进行随机测试——我认为“tdd”并不与之相关——你也不太可能将测试分布引导到有漏洞的方向。如果你写了代码或者至少可以查看它，你就会知道哪些看起来显然是正确的，哪些可能行也可能不行，因为它的工作原理不容易理解。换句话说，TDD 会将你引向黑箱测试，而对于复杂的机制来说，在我看来，黑箱测试效果似乎不如白箱测试；我相当确定人类是这样，但不太确定对于智能体是否也是如此。

我猜 TDD 表现不佳的推测是正确的吗？严格从结果上看，答案是肯定的。从我的推理来看（虽然没有明确以书面形式预注册，但我确实知道当时的思考过程），答案并不清楚。我的思路大概是这样的，正如我们最近在各种语境中讨论过的那样，要让智能体真正做正确的事情而不是仅仅过拟合，是实现智能体良好性能或正确性的关键。就整体方法论而言，而不仅仅是这条指令如何改变了智能体的行为，TDD 似乎容易导致过拟合。

智能体确实写出了较差的测试，有时还使用了一种相对昂贵且低效的迭代工作流程，但我不认为我原本预期的人类使用TDD并指导智能体实现那个失败模式是这里的真正问题，而那正是我的直觉来源。我会给这里的推理评分为“可能正确，也可能不正确”；我认为需要更多评估和调查来决定这一点，我猜更多数据的结果可能会显示我最初的推理是错的。

现在我们进入结果接近平均水平的范围。Spin 在中等和极高难度上表现稍低于平均水平，但成本低于平均水平。正如我们在其他正式工具中看到的，Spin 的使用总体上效果不理想。在本例中，使用 Spin 对某类行为建模与通过或未通过覆盖该行为的隐藏测试之间没有相关性。使用 Spin 是表面的，不具生产力。

Hegel 是一个基于属性的测试库，基于 Hypothesis：https://github.com/hypothesisWorks/hypothesis/。

正如我们现在可能预料的那样，代理并未有效使用 Hegel。在他们使用它的程度上，使用得非常表面化，而且通常是在大量依赖普通测试之后才使用它。由于单纯指出代理实际上并没有真正做这件事会显得重复，我会让这些部分简短，只突出特定的好奇点。

代理实际使用的工作流程通常是

如上所述，Hegel 技能并没有改善正确性。正确性反而更差（尽管差距很小，也可能是随机的）。更引人注目的是成本更高（中等增加 26%，极高增加 41%），原因似乎具有因果关系。

该技能导致代理生成更多的测试。额外的测试主要是检查畸形输入不会引发 panic 以及往返测试。前者是代理已经倾向于在所有基于属性和模糊测试条件下过度执行的操作，因此在这里的额外努力并没有用处。后者似乎并不是一个本质上糟糕的想法（我甚至经常明确指导代理创建往返测试，而且这些测试似乎对于检查特定属性很有用），但它并没有在最易出错的区域执行。如果没有额外指示，代理倾向于为相对简单且已经可能正确的属性创建往返测试。

至于成本，有多个原因。一是该技能相当大（技能本身 34k 字符，同时还加载了一个 45k 字符的 Rust 专用参考，最终超过 20k 个 token）。这些内容在运行开始时加载，并在之后的许多操作中反复读取。这导致中等情况下平均额外成本增加 16%，极高情况下增加 18%（按原始 token 计算，中等平均增加 90 万，极高增加 180 万；尽管这些缓存命中率很高，初次读取后的命中率为 99.85%，但由于仍有多次重读，所以这仍然占总成本的相当一部分）。

一个乘法成本（这个乘数已包含在前面的数字中）是该技能还指定了一组结构化的操作，这会导致更多的工作量。这些工作并没有提高正确性，因此增加了成本而没有相应的益处。

需要注意的一点是，该技能在160个案例中“仅”使用了157次。正如使用大型语言模型（LLM）时通常的情况一样，操作和结果是随机的。如果你有一个认为代理在特定任务中应该使用的技能，它可能会使用，也可能不会使用，这取决于一些对 AI 实验室外的人来说似乎不透明的因素。

在这种情况下，160 次运行中只有 108 次实际上打开了技能：https://github.com/trailofbits/skills/blob/d3323cefbcf645678b8dc481de204b02ad3d02dc/plugins/property-based-testing/skills/property-based-testing/SKILL.md 来阅读它。该技能建议在 Rust 中使用 proptest，但技能建议添加依赖需要批准，而这些都是单次自动运行，因此没有执行。

与到目前为止看到的其他属性测试案例一样，属性测试是初步的，并且没有以有用的方式进行。

Rstest 是基于测试夹具的：https://en.wikipedia.org/wiki/Test_fixture#Software_test_library.

We previously noted that, while it's easier than ever to hit a particular quality bar by having coding agents use effective test techniques, software quality seems to be getting worse：/ai-coding/, indicating that whatever defaults developers are using may not work very well. Here, we test if simple instructions to agents to use particular techniques or libraries improve implementation correctness, as a kind of test to see how effective agents are when guided by someone with no expertise in testing who's maybe heard that you should apply certain techniques or use certain libraries.

We'll re-use the Zstd implementation eval discussed in this comparison of agentic programming language effectiveness：/pl-tokens/ and, instead, compare different testing techniques and testing libraries when agents are given a prompt to implement Zstd with different addendums, such as "Use test-driven development", "Use Lean 4", "Use QuickCheck", "Use property-based testing", etc. I also ran some other evals, such as on the IMAP RFC, which are briefly discussed.

I pre-registered some guesses on how conditions will do:

Below, we have a very messy graph which shows the results for the conditions tested (codex with GPT-5.6 Sol, with medium and xhigh efforts). When looking at data, I tend to prefer much denser and messier graphs than most people, such as the first graph here：/android-updates/. Because most people find these kinds of graphs unreadably messy, I tend to split information out into a series of graphs, each of which shows less information, when presenting information to others. For reasons discussed elow, I'm not going to do this here and am just going to present this extremely messy graph where we have cost on the x axis and the fraction of runs that passed 100% of the (hidden) tests on the y axis, average of 80 runs from each condition and effort (mousing over items shows bootstrap covariance, 50% uncertainty：https://statmodeling.stat.columbia.edu/2016/11/05/why-i-prefer-50-to-95-intervals/, and there's some attempt at making like things similar colors, e.g., blue-ish for formal methods, green-ish for property-based testing, etc.):

One thing we can see is that nothing really wildly outperforms. However, Default (no additional instructions) does well above average. Looking at xhigh, on average, the fuzzing and PBT-related conditions did a little better than formal methods on average, with the situation being a lot more mixed at medium. The testing-related skills codex recommended we try underperformed, although our quick custom skill did ok (a major difference is that our skill is designed to nudge away from their default behavior towards more productive behaviors whereas the other skills seem more like tutorials). TDD didn't do well, as predicted (one skill also suggested that agents used TDD, and that skill also fared poorly in the cases where agents attempted to follow the instruction).

If we actually look at what agents did, it quickly becomes apparent that, in general, agents don't know how to use these tools or techniques very well. As we noted here：/ai-coding/, and as everybody I've talked to has also noted, agents are really bad at testing and don't seem to understand how to test reasonably "by default". For example, here's a comment by Gary Bernhardt：https://x.com/garybernhardt/status/2067002665427775613:

AI agents' approach to testing, more or less:

Take the pathological cases dreamed up by someone objecting to mocks 15 years ago, without ever having actually used mocks. Naive dreams of excessive mocking.

Make those pathologies the backbone of your testing strategy.

On xhigh, agents were generally able to get the tests they wrote to pass, but they wrote poor tests (e.g., they'd submit four identical bitstreams into a test of a feature that uses four bitstreams and miss any bug that would occur because they transposed bitstreams). And as we noted previously on the Zstd eval with respect to languages：/pl-tokens/#appendix-medium-in-a-loop-vs-ultra, running at a lower effort level in a naive loop gets worse results (agents do even more of this and stall out with lower correctness).

Below we'll look at how agents did things for each condition, ordered from worst correctness to best, but I would caution anyone against drawing any kind of strong conclusions from the ordering.

A lot of the failures here seem analogous to the failures we saw when we looked at the impact of programming language on token usage and correctness：/pl-tokens/, in that the failures are often idiosyncratic. For example, with programming languages, we saw that agents had a fairly high rate of getting the semantics of byte conversion incorrect in Clojure but not Java, even though agents "should" (and probably sort of do) know that they can get Java byte conversion semantics by converting with unchecked-byte instead of byte .

Verus：https://github.com/verus-lang/verus uses an SMT solver and various types of reasoning to prove that the code matches specifications.

Although Verus can prove that code matches specifications, agents didn't do that. Instead, they made proofs about various abstract properties relating to Zstd. I've not used a tool like Verus myself, so I can't speak to what an expert or even a beginner user would normally do, but from reading the tutorial, I find it a bit odd that agents didn't attempt to use Verus to verify any of the actual code and only used it to do abstract reasoning, as it seems designed to make it easy to prove properties about the actual code.

Additionally, if we look at the properties proved, there were generally few properties proved and the properties that were proved were uninteresting. For example, agents would prove things like "given a valid cursor/index/distance, the resulting operation remains in bounds", which isn't bad to prove, but wasn't really a source of bugs. Also, agents would frequently write vacuous proofs that were effectively A => A . An actual Verus proof of this form was:

In cases where agents actually proved something, they generally proved something relatively simple and avoided proving properties about the parts that were likely to have a bug (for example, agents often failed to reverse the bitstream order for encode and decode and would write tests that failed to detect this because the tests were palindromic; perhaps some kind of proof of reversal here might get agents to "think" about this in a different way).

It doesn't seem that agents were getting value out of Verus when just provided with Verus and the Verus docs.

If we look at the result, the aggregate xhigh Verus results are fine (slightly lower correctness than average, but much cheaper). The medium results had average cost and the lowest percentage of correct runs as well as the lowest average number of correct tests. Because agents didn't really get value out of Verus, what they actually did for correctness was mostly just traditional tests (built-in Rust #[test] functions with unit tests). When going from medium to xhigh, agents spend much more effort on traditional testing and only a bit more effort on using Verus, which allowed the xhigh result to be ok.

Looking at the actual tests, for one of the two features which agents using Verus did much worse on (the four stream jump table：https://github.com/facebook/zstd/blob/dev/doc/zstd_compression_format.md), Verus agents wrote a test for this in 89 out of 160 cases, coincidentally the exact same number as Default agents, but Verus agents were much more likely to write bad tests. They were more likely to encode incorrect results in the tests as well as make easy to pass tests that don't cover the space well, such as making all four streams identical. This kind of thing is what I meant when I said that the failures were idiosyncratic. There's nothing about Verus that necessarily makes one write poor tests when not using Verus and we wouldn't, in general, expect a human who's used Verus to write bad unit tests, in the same way that we wouldn't expect a human using Clojure to make more byte conversion mistakes, but this happened here for whatever reason (possibly a coincidence).

I don't know if folks inside AI labs can get access to better information on why things happened, but here on the outside it's generally quite difficult to tell why something like this happened (even when we formed a plausible hypothesis for the language issue, it required running many samples of many languages, and papers we looked at which studied the same thing didn't observe the language popularity / agentic effectiveness correlation because they either looked at too few languages to be able to reason about such a weak correlation or they looked at problems that were too small and too trivial).

Alloy is often called a bounded model checker. This is maybe not quite right with Alloy 6 since that introduces some extra features, but this is way outside of my area of expertise. My understanding is that, with Alloy, you normally prove properties about your model (as opposed to proving that your code works).

Alloy got the 2nd worst correctness score and, unusually, scored generally poorly on both medium and xhigh. Although it isn't shown (because it doesn't seem to add anything), in general, results were highly correlated between max and xhigh, which were quite different from medium results.

As we saw with Verus, agents using Alloy pretty much relied on standard Rust #[test] for correctness and mostly faffed about with Alloy. Once again, using a formal tool poorly did not help with correctness.

There were individual cases of Alloy use that were close to finding an issue or risk, but even then, only a small number. In one case, Alloy found a counterexample which then caused the agent to implement the Rust version with a mitigation for the potential bug. Unfortunately, the counterexample relied on an 8-bit overflow that couldn't happen in practice because the actual implementation used 64-bit usize with no possibility of overflow given the inputs, so it just made the code more complex without preventing an actual bug.

In another case, the Alloy specification was incorrect and a related test failed. After the test failed, the agent fixed the Alloy specification. Had the specification been correct, perhaps the agent would've written the correct code without the failure. There were some cases where it's possible the good version of this happened, but it's not clear if an actual potential bug was prevented.

Alloy agents did model things that were more closely related to the Zstd algorithm than Verus agents (which mostly checked things like arithmetic), but it was still the wrong modeling.

Differential testing is a technique where you give the same inputs to multiple implementations and then compare results to find issues. In principle, this seems like a reasonable thing to try with LLMs as we often get different results from different rolls of the dice, and as we noted here：/pl-tokens/#appendix-medium-in-a-loop-vs-ultra, having an agent iterate more on an implementation (which might be only part of the entire thing, perhaps even only part of a function) often works worse than having the agent restart from scratch.

But this gave us the third worst results. In this case, we had slightly above average results on xhigh and far below average results on medium. None of the agents created two full implementations to compare. Out of 160 runs, 135 did something you might call differential testing, but like the other conditions we've seen, these were generally trivial and effectively useless. And, in the cases where differential testing might've caught a bug, instead of implementing things in independent ways, agents just did the same thing twice and encoded the same bug in both versions.

I sometimes tell agents to do things independently and get them to launch with separate contexts, but this was not done effectively for differential and agents would generally just write the same thing twice.

It makes sense to discuss how the official Hegel skill changes Hegel behavior, but in reverse correctness order, Hegel Skill appears above Hegel because the result was worse on correctness. See the Hegel section below for discussion of this skill.

Lean 4 can maybe be described as an interactive theorem prover：https://en.wikipedia.org/wiki/Proof_assistant.

Although I didn't pre-register a guess about Lean, if I had pre-registered guesses on which formal tools would do well, I would've put Lean on the list of things I'd expect to do well because it's relatively hot/trendy and therefore seems relatively likely to have good performance due to synthetic data from RL envs.

The Lean agents did prove properties, like the Verus condition, agents mostly did arithmetic proofs that didn't hit the bug-prone or risk surface areas.

Like the other formal conditions, Lean agents relied heavily on standard Rust tests. As with the formal conditions so far, doing a few proofs of things that don't matter didn't help with correctness.

QuickCheck is a property-based testing library：https://en.wikipedia.org/wiki/Property_testing, probably the best known such library for a long time, although Hypothesis might currently hold that crown.

Unfortunately, agents were about as effective at using property-based testing as they were at using the formal tools we've seen so far. When using QuickCheck, agents mostly wrote very simple "smoke tests" that didn't check much. They also used random inputs, which, when fully randomized, are pretty poor for testing something like Zstd (because they just go down one of a few failure/rejection code paths).

Also, relatively few properties were checked. Although all agents used QuickCheck, 63 out of the 160 runs only checked a single property. Agents once again mostly relied on traditional testing, although they technically did use QuickCheck. For whatever reason, agents actually wrote more traditional tests than under the Default condition or most other conditions, but did fewer test-fix iterations (which resulted in this condition coming in with below average cost).

TDD underperformed here as well as in the IMAP RFC eval.

The TDD prompt seemed to cause large changes to agent behavior. Agents produced twice as many tests, and worked in a much more iterative test-code-test-code-etc. workflow, although a TDD advocate would probably say that agents didn't actually use TDD. There were only a few instances of agents doing some kind of fine-grained iterative TDD.

Overall, agents wrote more tests up front; for example, agents had one or more failing tests in 67 of 160 cases before doing substantial (non-stub) implementation, vs. 0 of 160 for the Default condition.

For broad test classes, TDD had more tests of every kind. There were more small, trivial tests and there were also more integration and end-to-end tests. Any kind of obvious high-level "agents did too much or too little of X" doesn't seem to fit the data. If we look at specific failures and how they were missed by tests, we can observe that the TDD condition had a number of these. For example, Zstd uses something called a jump table when there are four Huffman streams .

TDD agents were more likely to fail the eval test for this although they wrote more tests that cover the general case. For whatever reason, TDD agents were more likely to write tests that don't cover hard cases (e.g., making all four streams identical and then also making them trivial, like we saw with Verus). This is another case where I'd be curious what kind of visibility people at AI labs have since it's not obvious from the outside why priming agents with TDD made them write worse tests and worse implementations.

If we only had TDD and a few test conditions to go on, a hypothesis might be that TDD'd code often seems to have a lot of small tests that aren't very good, so maybe priming agents with TDD causes them to write more of these sorts of ineffective tests. But it's not clear why we should see the same pattern with Verus. Maybe we could tell whether or not this is true for TDD if there's a shared reason for the Verus (or other) behavior by re-running the experiment on an open model and inspecting what's actually going on inside the model at some level?

Two of the skills also caused agents to run in a more iterative approach, perhaps on the theory that executing more frequently would give better results, and both of those skills also underperformed. In general, across all conditions, agents were able to get the tests they wrote to pass on xhigh and max (not shown, but max had slightly better correctness than xhigh at substantially better cost). Getting their own tests to pass more iteratively tended to get agents to write more incorrect tests that would enforce incorrect behavior.

Yossi Kreinin had this thought for why TDD might result in worse tests:

fwiw, I think if you write the tests before the code, it's harder to test the harder cases since you know less about what is going to be hard, and even if you do random testing which I don't think "tdd" is associated with, you are less likely to steer the distribution in the direction where the bugs are. if you wrote the code or at least can look at it, you know what seems trivially correct and what might or might not work since it's not easy to understand what it does. in other words, tdd steers you towards black box testing which for complicated machinery seems to me to be less effective than white box testing; pretty sure this is how it works with people, less sure about agents

Was my guess that TDD would underperform correct? Strictly on the result, the answer is yes. On my reasoning (not explicitly pre-registered in writing, but I do know what I was thinking), I think it's not clear. My thinking was something like, as we've recently：/benchpocalypse/ discussed：/ai-coding/ in a variety of contexts：/pl-tokens/, getting agents to actually do something like the right thing and not just overfit is a key part of achieving good performance or correctness with agents. Speaking to the methodology in general and not how this instruction changed agent behavior, TDD seems primed to cause overfitting.

Agents did write worse tests and sometimes used a relatively expensive and ineffective iterative workflow, but I don't know that the failure mode I'd expect from a human using TDD and then directing agents to implement was the real problem here, and that problem was where my intuition came from. I would rate the reasoning here as perhaps and perhaps not in the right vicinity; I think more evals and investigation would be necessary to decide this and I would guess that the result of additional data would be that my original reasoning is wrong.

Now we're getting into the range where results weren't far from average. Spin did moderately worse than average on both medium and xhigh, at below average cost. As we saw with the other formal tools, usage of Spin was generally ineffective. In this case specifically, using Spin to model a certain class of behavior had no correlation to passing or failing the hidden tests covering that behavior. Usage of Spin was superficial and not productive.

Hegel is a property-based testing library based on Hypothesis：https://github.com/hypothesisWorks/hypothesis/.

As we might expect by now, agents didn't use Hegel effectively. To the extent they used it, they used it superficially, and they generally used it after heavily relying on ordinary testing. Since just saying that agents didn't really meaningfully do the thing is repetitive, I'll make these sections short and only highlight particular curiosities.

The actual workflow agents used was generally

As noted above, the Hegel skill didn't improve correctness. Correctness was worse (though it was close enough that this could've been random). What was more striking was that cost was much higher (26% higher on medium and 41% on xhigh), for reasons which seem causal.

The skill caused agents to generate more tests. The additional tests were mostly checks that malformed inputs don't cause a panic and round-trip tests. The former is something that agents were already inclined to do an excessive amount of for all of the property-based and fuzzing conditions, so additional effort there wasn't useful. The latter doesn't seem like an inherently bad idea (I even often explicitly instruct agents to create round-trip tests and they seem to be useful to check specific properties), but it wasn't done in any of the most bug-prone areas. Without additional instruction, agents were inclined to create round-trip tests for relatively trivial properties that were already likely to be correct.

As for the cost, there are multiple reasons for the cost. One is that the skill is fairly large (34k characters for the skill, which also loads a 45k Rust-specific reference, which ends up being more than 20k tokens). This was loaded at the start of the run and was re-read on many subsequent actions. This resulted in an average additional dollar cost of 16% for medium and 18% for xhigh (by raw tokens, the average increase was 900k on medium and 1.8M on xhigh; although the cache hit rate on these was very high, 99.85% after the initial read, they were re-read enough that this was still a substantial fraction of total cost).

A multiplicative cost (this multiplier is included in the previous numbers) is that the skill also specified a structured set of operations that cause a lot more work to get done. This work didn't increase correctness, so this increased cost without a concomitant benefit.

One thing to note is that the skill was "only" used in 157 out of 160 cases. As is generally the case when using LLMs, the actions and results are random. If you have a skill available that you think an agent should use for a particular task, it may or may not use it depending on factors that seem opaque to people outside of AI labs.

In this case, only 108 out of 160 runs actually opened the skill：https://github.com/trailofbits/skills/blob/d3323cefbcf645678b8dc481de204b02ad3d02dc/plugins/property-based-testing/skills/property-based-testing/SKILL.md to read it. The skill suggests using proptest in Rust, but the skill suggests approval is required to add a dependency and these were all single-turn autonomous runs, so this wasn't done.

As with the other property test cases seen so far, property testing was rudimentary and not done in a helpful way.

Rstest is a fixture-based：https://en.wikipedia.org/wiki/Test_fixture#Software test library.