尽管编码代理在应用有效测试技巧后更容易达到特定质量标准，软件质量却似乎仍在恶化，说明开发者默认采用的方式可能效果不佳。为此，我们用Zstandard（Zstd）实现任务作为评测基准，分别指示代理使用不同测试技术或函式库，观察这些指令能否显著提升实现正确性。

我们之前注意到，虽然现在让编程代理使用有效的测试技术比以往更容易达到特定质量门槛，但软件质量似乎在变差，这表明开发者使用的默认方式可能不太奏效。这里我们测试给代理简单指令使用特定技术或库能否改善实现正确性，算是考察在无测试专业知识的人指导下代理的效果。

复用 Zstd 实现评估，比较不同测试技术和库，给代理实现 Zstd 的提示并附加如“使用测试驱动开发”“使用 Lean 4”“使用 QuickCheck”“使用属性测试”等。也跑了 IMAP RFC 等评估简要讨论。

所有实现用 Rust。测试的 26 种提示条件：ACL2、Alloy、“审计并模糊风险区域”、“先审计”、Creusot、默认（无额外指令）、差分测试、模糊测试、Hegel、Insta、Judgement（代理选最佳技术）、Kani、Lean 4、“别犯错”、变形测试、变异测试、属性测试、Proptest、QuickCheck、rstest、Rust 内置测试框架、SMT 求解器（Z3、cvc5、Yices 均可用）、Spin、TDD、TLA+、Verus。另测 4 技能：Hegel 官方技能、ECC Rust 测试技能（25万星3.8万叉）、Trail of Bits 属性测试技能、我写的测试技能（我习惯用提示而非技能）。除我的外，技能是 codex 找的相关顶尖技能。

预测

预注册猜测： * TDD 会表现不佳（55% 置信） * 形式化方法不会超额（52%） * “别犯错”不优于无指令（95%） * ECC 测试技能不优于（65%） * Hegel 技能不优于（65%） * ToB 测试技能不优于（55%）

整体结果

有混乱图（codex GPT-5.6 Sol medium/xhigh，成本 x 轴通过隐藏测试比例 y 轴，每条件80次平均）。无远超者。默认远高于平均。xhigh 模糊和属性测试略好于形式化，medium 混合。测试技能 codex 荐的表现差，自定义技能还行（因引导离默认）。TDD 如预测差。

看代理实际做，明显不会用工具。引 Gary Bernhardt：AI 代理测试：1 拿反对 mock 的病态案例从不真用 mock；2 让病态成测试骨干。

要求用特定技术，这没大变。代理要么写惯常测试塞进框架，要么表面用技术没价值。技术命名后做 Gary 说的事但针对那技术（形式化证无关属性，属性测试随机命中无效）。IMAP 等结果无不同。无论问题类型代理没有效用形式化或测试库。

xhigh 代理能让写的测试过但测试差（如四个相同比特流测四流特征漏转置 bug）。低努力更糟。

好奇实验室没造 RL 环境学测试。之前代理擅运行优化因可造 RL。可能缺有效测试知识。

下按正确性最差到最好看各条件，但警告别强结论。

很多失败类似编程语言影响，特异的。如 Clojure 字节转换错多 Java。语言流行度与性能中等相关因训练数据多。这里无清晰模式，除代理只有库名时基本无效。跳到最后。

Verus

Verus 用 SMT 证代码匹配规范。代理没做，证 Zstd 抽象属性。少且无聊如证有效游标操作保边界，常写空洞 A=>A。没获价值。xhigh 结果还行（正确略低但便宜），medium 成本均正确最低。靠传统测试。四流跳转表 89/160 写测试同默认数但更差（易错结果全同流）。

Alloy

有界模型检查。正确倒数第二差。代理靠标准测试胡搞 Alloy。个别近发现但少。一反例依赖8位溢出实际无。另一规范错测试败后改规范。建模比 Verus 近算法但仍错。

差分测试

同输入多实现比结果。第三差。xhigh 略均上 medium 远低于。没建两完整实现。135/160 做点但琐碎。可能抓 bug 处写两遍同 bug。

Hegel 技能

反向顺序 Hegel Skill 在 Hegel 前因正确更差。见下。

Lean 4

交互定理证明。Lean 证属性类似 Verus 算术不命中 bug。靠标准测试。

QuickCheck

属性测试库。代理用同形式工具无效。大多简单冒烟测试。随机输入对 Zstd 差。63/160 只查一属性。靠传统测试但写更多传统少迭代成本低于均。

TDD

TDD 和 IMAP 都差。提示大改行为：测试加倍迭代。67/160 有失败测试 before 实现 vs 默认0。各类测试多但更易失败跳转表虽写多覆盖一般。写不覆盖难案例（全同流）。为何 TDD 更差不清。两技能更迭代也差。xhigh 让测试过但更迭代致更多错测试强制错行为。

Yossi Kreinin：先写测试难测难案例因不懂什么难，随机也少导向 bug。TDD 黑盒不如白盒。

我猜 TDD 不佳正确？结果上。理由不清。以为 TDD 过拟合。代理写更差测试有时贵工作流。

Spin

模型检查。略差于均成本低于均。用 Spin 无效建模与该行为测试无关。

Hegel

基于 Hypothesis 属性库。代理没效用。工作流：读RFC/API、实现、普通测试、读Hegel文档、写1-4简单属性测试、继续普通测试。技能没改善正确成本反高（medium26% xhigh41%）因技能大加载重读且指定结构增工无益。157/160用。

ToB 技能

108/160 读技能。建议 proptest 但需批依赖单轮没做。属性测试原始无帮助。

Rstest

fixture 库。代理基本没用只写标准单元在内，没用 fixture。

Rust 测试

标准内置框架。明确要求增测试（medium双 xhigh25%多）但没更好。错因不测重要或实现错测试。加测试没增风险覆盖。

Yossi Kreinin：固定输入输出风格鼓励此。生成输入需分类输出促思考正确；固定易编码输出以为对。

Creusot

同 Verus 空间。没效。

变异测试

改代码测测试效。代理没真做变异而普通加少量不像。少数。

Judgement

自适应用测试。大多标准单元。少数模糊。

模糊测试

随机输入。代理发随机字节走无效路径。偶结构化随机（10/160）半找真 bug。5/160 有效是较有效之一。表明可训或导更好。

Insta

快照库。几乎没用靠传统。用 Insta 常写普通单元。

SMT

指示用 Z3 cvc5 Yices。代理当草稿算东西。即使建模也不对。例如应 byte1+(byte2<<8)+0x7F00 许多写 byte1+(byte2<<8)|0x7F00，证属性仍写错代码不比默认好。

TLA+

行为建模。above average 但仍差默认。159/160 建模型一般状态机。30 建模 Huffman/FSE。晚建模。有时改模型错但没改 Rust。复杂建模没更好正确。

变形测试

查相关输入输出关系。如插可跳帧边界不改输出等。合理但不命中常错区。代理像醉汉路灯找钥匙。xhigh 用更少。

ECC

技能还行因大部分忽略。153/160读致更多测试。早看越差。7没读全对9晚看全对故原始分还行。受影响低于均（小无用测试）。技能说红绿 TDD 致多测试无效。

提 Caveman mode 方差大，160次多但表面 ECC 还行。需更多跑平均噪声。人常只看头数。

默认

无指令。above average 不奇怪。告诉做无用不如不告诉。

审计

实现后审计。152/160做151称改。一般区但不独立上下文常同错。42独立代理更差。xhigh 最好正确 medium 低于均成本增。总体约同默认。

Em Chu：审计我 token 大多去向有用。指令别生子代理自己读；别执行代码。LLM 若允许更笨。还加 BS 对抗等。

审计并模糊风险区

Zstd 此指令聚焦 FSE Huffman 比特等风险。medium 忽略 xhigh 遵循。没比无指令好。代理常随机输入无效不趣。人多靶向有趣输入代理没做。多看崩溃不查属性。

别犯错

技术分高于默认但行为无不同近随机。

Kani

模型检查库。实际用形式于代码 Kani 覆盖最好因真用但偶发表面多。1/160 真抓非平凡 bug 改代码。成本高因读输出贵。

ACL2

定理证明。多 OOM 不计数偏。虽高于默认但不因果。同形式证不影响正确性。

Proptest

属性库。同随机大多无趣过度随机。但 shrinking 有时价值。

属性测试

每代理选 proptest 成第二 proptest。类似测试不太好但有时找 bug shrinking 赢。有趣第二臂也 above average。

技能

我写简单技能。Max Bittker 说写编码我测试知识的技能，结果他早猜对。

技能内容： * 实现前想易错区；各述可能错和歧义解释，做结果不同检查（偏好非对称/边界） * 实现后高风险独立重推导无上下文比（新鲜不重用） * 可行用属性或随机探空间最小化无恐慌随机 * 随机倾探有趣状态路径（不朴素同错路径）需结构化 * 不确定独立推理查正确（新鲜不重用）

得最高分但没按意图。几乎没新鲜上下文。代理识风险如比特反转但没做好（medium#35 识独立仍败因回文）。模糊手写。若指示 proptest 可改。指令减失败模式有些用但测试差于人。初稿不糟没真就绪。

之前没细拆数据因看代理做大多无效比坏用 Verus vs QuickCheck 无趣。有趣代理能识风险区但不管啥技术都失败用。只叫测试也差。我的快速技能可改但需超2分。Yossi 评测试状态糟所以 fallback 训练差。

代理稍好用 proptest 但仍低于合理人。

如何让代理写好测试？

经验：引导设合理测试分类结构，加东西 ok-ish。我偏随机/模糊/属性。

Jamie Brandon 快照测试同感：代理说做快照实际单元。另一项目能写端到端 mock IO 但需移测试单独 crate 和 AGENTS.md。

我更靠代理写测试代码（CLI 打字）他手写。但设合理结构就行。

类似早问题：轻指令差；看做打几句快好。猜模型内有理解如何做但非默认需 priming 实践。

好奇能否打包技能或实验室训更好或间接改进够写不错测试。

预测准确度

• TDD 不佳 True
• 形式不超额 True 但非因预期（代理无效所以不能超）
• 别犯错不超 True 因无操作比无效好
• ECC 不超 True
• Hegel 不超 True
• ToB 不超 True 未注册：
• Lean 形式中好 False
• 我的技能中差 False（Max 猜对）

技能

我常觉工作流旧因不用 skills 用 scratchpad。看 Thorsten Ball 谈不依赖及几人有效也不用疑没错过。实验感觉技能不助反伤低置信。其他两实验官方技能更差。现在更看个人用因失败可预测可修。

写技能朴素想法

看的技能像人类教程解释怎么做。模型已有知识给改行为陈述而非教无知。不同 harness 模型努力默认不同塞文本不真改多忽略。ECC 读后忽略大多 TDD 影响没真跟。GPT-5.5到5.6 工作大改不认为同技能通用。个人用针对特定做几个。测试无通用因任务特定。可能技能问问题发指令但模型快改进不值调。试的技能同失败。

附录：一些回应

David R. MacIver 说 Hegel 技能糟。因代理写技能差大家都用代理写。友人建 benchmark 确认缺在改。

附录：实验细节

快速写略。分布同语言影响类似。几看似有趣结果细看因短提示实验错修得无聊负面除 codex 荐技能反生产。

脚注1 IMAP 结果较无趣。仅单跑完美（别犯错 medium）。所有方法无效。TLA+ 本适 IMAP 但代理先 Rust 后建模小邮箱不建模错区。RFC 不现实真实更歧义失败同或更差。

脚注2 ChatGPT fact check 说段落错因有论文训代理写测试但训写差单元。正导致差。有 RL 随机测试论文但没进大模型训练。

脚注3 语言优势论可能模型好后成真但无由。像扑克 range advantage 不来自 solver。用实验看 work 别抛 cocktail 想法。

社区对用 AI agent 执行各类测试技术的实验反响分化，多数人质疑 agent 易机械遵循流程却丢失业务目标与架构，少数人认为适当约束下仍有价值。分歧主轴在于测试失效源于 agent 约束遵循力弱，还是实验脱离代码架构现实。

认为 agent 容易机械执行测试流程却丢失业务目标与真实约束

• 多种经验指出，agent 常满足易验证的表面指令（如先写检查界面元素存在的测试、生成随机字节做模糊测试、改动后跑全量套件），却无法从业务需求独立推导有意义用例，也难以将真实目标作为主约束，导致不同测试技术结果趋同。（较多人） > 形式上技术用了，但目的丢了，这或许解释了为何不同测试技术结果相似（@nseskin）

认为实验脱离代码架构现实且方法不够严谨

• 有效测试八成在于代码架构而非测试框架，作者未说明代码如何架构管理，使结论效用有限；此外手动变异测试不如接入自动化框架并以构建失败强制达标，后者 agent 无法忽略。（较多人） > 测试代码的方式不能也不应与架构代码的方式解耦，而作者没提代码如何架构（@siscia）

认为在正确架构约束和调优下 agent 测试仍有价值

• 强制依赖注入或六边形架构并做简单覆盖率检查，能以较少精力产出够好代码；若语言默认风格鼓励，agent 也知道如何让非法状态不可表示。有开发者自嘲不擅长测试，反而觉得 agent 做得合理。（少数人） > 经验里 agent 知道如何让非法状态不可表示，只是若非语言默认风格便不去做（@ngruhn）

认为测试理论本身的缺失放大了 agent 的无力感

• 相比性能优化有量化指标与售卖话术，测试缺乏切实评估体系和理论，行业悲观地将测试丢给低能力者且不愿投入改进，这使自动化测试难有标准。（少数人） > 测试任务留给最没能力的人，且几乎不努力改进，因为被视为预算黑洞（@crabbone）

有价值的补充

• 更有趣的实验方向是手写非平凡系统的高层规约（如活性等），看 agent 能否通过引导精化产出满足规约的实现（gz09 设想）。
• agent 常过度纠结浮点边缘情况（如空值、无穷），可能源于训练数据中此类属性测试过量，但与业务规则无关（movpasd 观察）。
• 即使形式验证也可能巩固错误设计：有开发者让 AI 做架构改动完全反向，测试全绿却证明不该存在的东西正确，形式验证只会更强证明此“正确性”（andai 经历）。
• 用“鹰隼无视驯鹰人”类比模型无视项目约束、执意运行全部测试，开发者只得写确定性钩子拦截错误调用并长期打磨规则（ianjbutler 类比）。