antithesis-mutation-testing

Antithesis 变异测试

技能版本： 2026-10-21 4f8d80b

目的和目标

验证的是判定器，而不是被测系统。

一次绿色运行只能说明没有观察到坏情况，并不能说明该属性能够发现问题。变异测试消除了这种模糊性：针对每个属性，注入一个专门用于破坏该属性的真实缺陷，在 Antithesis 下运行，并确认该属性触发。

成功意味着：

• 每个范围内的属性都被变异体证伪，或具有其他四种判定之一：不可变异、待处理、已撤回或已细化（参见 references/evidence-and-report.md 中的“判定和限定条件”）
• 每项证伪都有运行记录作为依据，且证据表明属性因预期原因而失败，而非因无关连锁反应受到波及
• 修复过程中发现的错误判定器和工作负载缺口；将有问题的属性交回 antithesis-research
• antithesis/scratchbook/mutation-testing/report.md 记录每个范围内属性的结果及证明该结果的运行
• 用户的工作树不包含任何变异——所有变异体都位于分支中，并由 clean.sh 确认。经授权的修复可以提交到该分支；变异绝不能提交

使用 antithesis-research 技能构建属性目录，使用 antithesis-setup 技能搭建测试框架，使用 antithesis-workload 技能实现断言和测试命令。使用 antithesis-launch 技能提交运行——不要直接运行 snouty launch。使用 antithesis-triage 技能读取结果。

先决条件

• 如果 Antithesis 工作手册（通常为 antithesis/scratchbook/）缺失，或未能涵盖代码中的断言，请根据这些断言和基线运行重建目录——参见 references/catalog-reconstruction.md。这不会阻止测试，但会缩小测试范围能够覆盖的内容。
• 如果 Antithesis 配置目录包含 manifests/ 子目录，请勿继续。Kubernetes 测试框架目前尚不支持：变异体选择通过为每个变异体构建一个镜像并在 docker-compose.yaml 中替换标签来实现。请告知用户并停止。务必在下文的 Compose 检查之前检查这一点——Kubernetes 测试框架没有 docker-compose.yaml。
• 如果 Antithesis 没有 docker-compose.yaml，且也没有 manifests/ 目录，请勿继续。使用 antithesis-setup 技能创建 Compose 测试框架。
• 如果被测系统和工作负载中完全没有 Antithesis SDK 断言，请勿继续。请先使用 antithesis-workload 技能——没有可供验证的判定器，重建也无法替代这一环节。
• 如果未安装 snouty，请勿继续。安装选项参见 https://raw.githubusercontent.com/antithesishq/snouty/refs/heads/main/README.md。
• 如果 snouty 版本低于 0.8.0，请勿继续。使用 snouty --version 查看版本，并使用 snouty update 更新。
• 如果此仓库没有从源代码构建的被测系统服务，请勿继续。部分服务从源代码构建、部分服务使用预构建版本的情况也可以接受，可通过限定范围处理（见下文）。

基线门槛

在设计任何变异体之前，当前代码状态必须有绿色基线。 在存在 Bug 的 SUT 上进行变异测试毫无意义：你无法区分某个属性是因变异体触发，还是原本就已失败。

**绿色意味着：**每项安全类属性（Always、AlwaysOrUnreachable、Unreachable）均通过。

此外，还要检查你打算变异的属性是否实际出现在本次运行的属性列表中。这需要将目录 slug 映射到属性名称——运行报告中的 name 是断言的消息字符串，不是你的 slug——因此现在就按 references/sweep-and-verdicts.md 中的“先将 slug 映射到属性名称”建立映射。Antithesis 从未编入目录的断言无法被证伪；这不会导致门槛失败。将每个缺失项标记为待处理 — 未编入目录，然后继续处理其余项（references/catalog-reconstruction.md 会诊断缺失原因）——但对于使用 fallback SDK 或 JavaScript 的服务，缺失只意味着“本次运行未命中”：像处理其他属性一样对其进行变异，并从运行事件中读取标记（references/catalog-reconstruction.md 中的联接表）。只有当它们一个都没有出现时，才说明测试框架已损坏，而不只是未完成：停止并报告。

同时检查检测信号——Software was instrumented、Symbols were uploaded、Thread pausing was enabled（antithesis-triage、references/instrumentation.md）。报告这些信号，但仅在支持覆盖率检测的语言中将其作为门槛条件。Python 仅用于编入目录，fallback SDK 不会发出这些信号；这两种情况下，模糊测试器都没有覆盖率反馈来引导其发现差异，因此对于仍存活的变异体，应优先延长重新运行时间，而不是判定为预言机错误，并在报告中说明这一点。

绿色不要求运行中的每项属性都通过：

• Reachable 或 Sometimes 失败不会阻止扫描：记录下来，将其交由 antithesis-workload 处理，并纳入范围界定——同一未充分测试区域内的安全属性很可能会被标记为待处理 — 工作负载缺口。
• 遥测和流量属性（Hypervisor utilization、Customer output volume 等）不是 SUT 正确性信号。忽略它们。

安全属性失败时，停止此技能。报告失败情况，并引导用户使用 antithesis-workload 或 antithesis-research——但请先读取 counterexample_count。Always 和 Sometimes 意味着 Reachable（antithesis-triage、references/properties.md），因此即使从未触达某项安全属性，它也可能显示失败，而实际上并未违反任何不变量。counterexample_count 大于零表示真实违反，必须停止扫描；既没有反例也没有示例，则表示从未评估——这是覆盖率缺口，按上述失败的 Reachable 处理。

读取 status.md 中记录的基线；只有当其 base_tree 指纹与当前指纹匹配时，该基线才有效。首次扫描时，按 references/evidence-and-report.md 定义的格式在此处创建文件，并持续写入——如果只在结束时写入，扫描就无法恢复。如果没有有效基线，则按 references/sweep-and-verdicts.md 中的“建立基线”进行建立。

正在重建目录时，应先运行本次运行，并以此提供属性列表。门槛本身不变——安全属性失败仍会停止此技能，无论目录是否为其命名。

上限以运行次数计。实测基线墙钟时间若与访谈中的经验法则相差很大，应调整计划，而非重新请求授权——在上限内继续。

定义和概念

• SUT： 被测系统。
• 变异体： 一处小而真实的源码改动，旨在违反且仅违反一项属性；它会构建为独立镜像，并以 mNN-<slug> ID 标识。
• 被证伪（被杀死）： 在带有该变异体标记的历史记录中，该变异体运行时目标属性失败，且日志将失败原因与偏离行为联系起来——绝不能仅凭整个运行中标记为绿和目标为红这两个计数来判定（references/sweep-and-verdicts.md，“Attributing a falsification”）。
• 存活： 变异体已运行，错误代码已执行，而目标属性仍然通过。通常说明变异体、判定器、工作负载或属性存在缺陷——判定阶梯会将这些情况与搜索始终未触及该用例区分开来。
• 基线： 使用与每个变异体相同的源码构建、未打补丁的 SUT 的一次运行。即对照组。
• base_tree： 分叉的 mutation-base 提交对应的 git 树哈希。它是判断已记录基线是否仍然适用的指纹。
• 公告： 由变异体补丁携带的一条启动日志，用于证明部署的是正确的构建。可在本地检查，无需消耗任何运行预算。
• 标记： 由变异体补丁在发生偏离行为的位置携带的信号，用于证明错误代码已执行。如果 SDK 收录了断言目录，则使用 Reachable 断言；否则使用日志记录。
• 附带损害： 变异体运行时，目标属性以外的其他属性也发生失败。这种情况可以预期；只有证据表明确实存在不同的违规行为时，才予以计入。

启动访谈

先扫描——问题 2 的报价以 N（安全类属性数量）为基准，只有扫描才能提供这个数字——然后在做任何其他事情之前问完全部五个问题。这些答案决定了此技能会花费多少资源、会在没有你参与的情况下推进多远，以及它可以更改你的代码树中的哪些内容。

始终扫描源代码中的 SDK 断言调用点——不只是目录缺失时才扫描（references/catalog-reconstruction.md 列出了各语言的拼写形式）。这能告诉你当前属于以下三种情况中的哪一种：

• 目录存在且与扫描结果一致——统计其中的安全类属性数量；这就是变异体数量
• 没有目录——重建目录（references/catalog-reconstruction.md）；扫描所得的安全类属性数量就是变异体数量
• 目录存在，但扫描发现了目录从未提及的断言——目录已过时。只重建缺失的条目，并说明这一点

无论哪种情况，都要向用户展示属性列表及其类别——在花费任何预算之前，正是纠正名称或范围判断的时机。

1. 分支位置。 临时变异副本的存放位置。默认：Agent 的暂存区。还要询问是否应从副本中排除任何大型构建目录（参见 references/mutation-harness.md）。
2. 预算与并发。 报出一个范围：N 个变异体加一次基线运行，最低需要 N+1 次运行；但考虑到重试、更长时间的重新运行，以及每轮核心修复后都要进行完整的重新扫描，合理估算约为 5N 次运行——建议将其作为本次会话的总运行上限。此外还要加上约 N × T 次镜像构建，其中 T 是构建一套完整镜像所需的次数——通常这是更大的数字。T（根据服务数量估算）和实际的单次运行耗时（对于 15 分钟的运行，连同设置和报告约为 45 分钟）都要等基线测量后才能确定；应明确说明这一点。然后询问允许同时进行中的运行数量——无论如何，提交操作都会串行执行（references/sweep-and-verdicts.md）。
3. 轮次。 每次扫描后设置检查点，还是自主迭代。
4. 对源代码的更改。 此技能可以直接将断言和工作负载修复应用到用户的代码树中，还是应提出修复但不应用？无论哪种情况，变异补丁都不会触及实际代码树——这里指的是扫描发现的问题修复。
5. 遇到有问题的属性时。 停下来转交给 antithesis-research，还是直接完善目录——纠正属性，或在概念上无法证伪时撤下该属性——然后继续处理其他属性。

选择自主、完善和应用，即可让工作流持续运行，直到收敛或耗尽预算。

在花费任何资源之前，将答案写入 antithesis/scratchbook/mutation-testing/interview.md——包括路径、五个答案和已商定的范围（格式参见 references/evidence-and-report.md）；每当答案变更时都要更新。这是唯一记录用户授权内容以及停止后的扫描恢复依据的地方。

此处确认的运行上限，是本次会话的长期授权额度。 在此额度内进行后续轮次，无论采用哪种工作流，都无需重新确认；后续会话恢复时只需重新确认一次。若某轮会超出上限，就必须停止——在设有检查点的工作流中询问；在自主工作流中则写出报告，列明尚未完成的事项。从首次启动开始，就要在 status.md 中记录已用运行次数，并与上限对照。

文档依据

使用 antithesis-documentation 技能访问以下页面。优先使用 snouty docs。

• 属性与断言：https://antithesis.com/docs/concepts/properties_assertions/assertions.md
• SDK 参考：https://antithesis.com/docs/reference/sdk.md
• 故障注入：https://antithesis.com/docs/product/fault_injection.md

参考文件

参考资料	阅读时机
references/mutation-harness.md	始终阅读——分叉、补丁布局、标签、构建、验证
references/catalog-reconstruction.md	草稿本缺失或落后于代码时——重建用于变异的目录
references/mutant-design.md	为某个属性设计变异体时；三部分补丁
references/static-validation.md	在消耗一次运行前追踪击杀链
references/sweep-and-verdicts.md	启动、轮询、分类存活变异体及迭代循环
references/evidence-and-report.md	记录判定结果和最终报告
references/resume.md	先前的扫描已生成 interview.md 时——恢复扫描

推荐工作流

首轮扫描

1. 扫描源代码中的 SDK 断言调用点，进行初始访谈，并将答案记录在 interview.md 中
2. 阅读 references/mutation-harness.md；将测试框架复制到 antithesis/scratchbook/mutation-testing/，解析每个脚本使用的路径（--source、--patches、--images、--fork），并创建分叉
3. 使用从此仓库构建的 compose 镜像名称填充 antithesis/scratchbook/mutation-testing/images.txt（references/mutation-harness.md，“Tags”）
4. 满足基线门槛（见上文）
5. 如果草稿本中没有目录，请阅读 references/catalog-reconstruction.md，并根据断言和基线运行重建目录
6. 选择范围内的属性（见下文“范围”），并利用基线分流结果排除未执行的属性
7. 阅读 references/mutant-design.md 和 references/static-validation.md
8. 为每个范围内的属性设计一个变异体；在支持的情况下，将每个属性委派给一个子 Agent（见 references/static-validation.md）。审查这一批变异体，并在接入任何变异体之前拒绝薄弱、易崩溃或无法杀死的候选项
9. 在分叉中编写已接受的变异体，每个变异体使用一个 mut/<id> 分支，并通过 sync-patches.sh 导出
10. 构建基线和每个变异体镜像，然后使用 verify-mutant.sh 在本地验证每个变异体
11. 阅读 references/sweep-and-verdicts.md；启动扫描，每次按顺序执行一个 select-mutant.sh → 启动任务，运行可重叠进行，但不得超过约定的上限
12. 轮询、分流并分类每次运行
13. 阅读 references/evidence-and-report.md；记录判定结果并编写报告
14. 在扫描收敛或被放弃时，以及发生任何故障后，运行 clean.sh——但不要在准备恢复扫描时运行；如果达到上限时仍有未完成的属性，则视为需要恢复：分叉中保留任何尚未导出的变异体分支，其 base_tree 是恢复时进行差异比较的依据（references/resume.md）。如果必须先清理，请运行 sync-patches.sh；恢复时会将任何指纹漂移视为实际变化，并重新建立基线

一轮排查后的迭代

1. 阅读 references/sweep-and-verdicts.md
2. 等待所有运行结束，并在更改任何内容前对每个存活项进行分类——在运行过程中应用真实代码树修复，会使该运行所依据的基线失效
3. 一并应用本轮所有已诊断出的修复；凡是涉及用户代码树的操作，都要遵循访谈问题 4
4. 重新分叉前，先使用 sync-patches.sh 导出每个已修订的变异体；否则 fork.sh 会拒绝执行——绝不要用 --force 绕过此限制（references/mutation-harness.md 中的 “When a script stops on an assumption”）
5. 按双分支规则重新运行：仅变异体补丁发生更改时，只需重新运行发生更改的变异体；若 SUT、工作负载或断言有任何更改，则必须重新建立基线并进行完整排查。启动变异体前，重新构建并验证每个变异体——分叉之间的标签保持不变，因此过期镜像会在不提示的情况下直接运行
6. 更新报告，并在排查结束后运行 clean.sh

恢复已停止的排查

预算耗尽、拒绝检查点、会话结束——无论因何停止， 都应根据记录的状态恢复，而不是重新推导。如果不存在 interview.md， 则这是首次排查：先运行开场访谈。否则，阅读 references/resume.md 并按其中说明操作：它会核对 status.md 与平台状态，从旧分叉中恢复尚未导出的工作，判断记录的基线是否仍然适用，并在正确步骤重新进入上述两个工作流——不会重复处理任何在当前 base_tree 下已有判定结果的变异体。

范围

断言类别	处理方式
Always、AlwaysOrUnreachable、Unreachable	变异。 安全属性通过只能算是负面证据——这项技能要排除的正是这种空洞通过
Sometimes(cond)	仅建立基线。 只有当其条件在所有时间线上都为 false 时，Sometimes 才会失败，因此，受微妙前置条件限制的变异体会在从未满足前置条件的时间线上保持通过
Reachable	仅建立基线。 Reachable 通过已能证明工作负载驱动系统到达了该状态

“在范围内”是指目录中的每个安全类别属性——无论最终是否为每个属性生成变异体，报告都必须涵盖它们。两类属性不会进行变异，但仍须给出判定：

• 基线中未触发。 对于 Always 和 AlwaysOrUnreachable，基线中的 example_count 为 0，意味着断言从未评估，而变异体从未被触及就不可能被杀死。不过，一次 15 分钟的随机运行只是一次抽样，且恰恰会低估最值得验证的深层、罕见状态：将其排除出范围前，先用更长时间的基线确认，然后将其转交给 antithesis-workload，并记录为待处理——工作负载缺口。此判定是暂定的：它与梯级中的判定一样，属于同一个工作负载不佳工单，受问题 4 和其他实际树修复所遵循的上限约束。请在确定范围时检查这一点。 Unreachable 是个例外：其健康状态是 example_count 为 0。 其受保护区域是否被触发，正是变异体标记所要证明的。请从断言扫描中确认类别——目录的 Type 字段会将所有三个安全类别合并为 Safety，因此，仅查看目录就会把所有 Unreachable 都排除在范围之外
• 无法变异。 该属性归属于并非在此仓库中从源代码构建的组件（例如，标准数据库镜像、托管队列）。这是关于测试框架的事实，并非属性存在缺陷——绝不能据此撤回
• 未编入目录。 断言存在于源代码中，但从未出现在基线的属性列表中。请根据 references/catalog-reconstruction.md 中的检测说明，将其记录为待处理——未编入目录；除非服务使用备用 SDK 或 JavaScript，在这种情况下，缺失是正常的，应像其他属性一样进行变异（参见其中的连接表）。如果变异体始终无法通过 verify-mutant.sh，或其补丁已变为 STALE，也应归为同一判定：扫描未能得出结果，并如实说明

确定范围时，请留意条件看起来显然可满足的 Sometimes——也就是名义之外的 Sometimes(true)。请将其作为目录观察结果报告，并采用 antithesis-workload 自审要求的 Reachable(...) 改写；切勿擅自应用。

通用指导

• 变更始终只以补丁形式存在，而且只存在于分支中。 绝不要将突变体补丁应用到用户的工作树；oracle 和工作负载的修复应提交到那里，突变体则绝不提交。
• 每个属性只设置一个突变体，用于模拟真实的错误。 例如删除保护条件、翻转比较运算符、偏差 1 或缺少限幅，而不是蓄意破坏。
• 不要钻循环的空子。 通过将工作负载削弱为狭窄的确定性路径来获得击杀，或将突变体粗暴改成一眼就能看出的蓄意破坏，都不如如实记录一个无法击杀的候选项。目标是构建能捕获真实错误的目录，而不是堆出一片绿色勾选。
• 将断言重新关联到随后会验证该断言的突变体，并不能证明任何东西——重新扫描得到的击杀属于循环论证。只有断言确实有误时才这样做，并将其记录为精炼后证伪，绝不能只记录为普通证伪。
• 暴露错误 oracle 的突变体是成功，而不是绕路。 将它发现的缺口记录在该属性的证据文件中。
• 获准实施的修复若被推迟，扫描就尚未完成。 当访谈问题 4 的回答是应用修复时，关于错误 oracle和错误工作负载的诊断是待办事项，而不是观察结果。先迭代成本较低的突变体侧修复；待其稳定后，在运行上限内提交实际工作树中的修复并重新扫描（参见 references/sweep-and-verdicts.md 中的“迭代”）。
• 优先精炼属性，而不是撤回属性；撤回时绝不能不作说明。
• 突变体运行会有意导致属性失败。 启动时必须始终指定专用的 --source 和 --ephemeral，以免被误认为用户真实测试历史中的回归。

输出

• antithesis/scratchbook/mutation-testing/patches/ — 每个突变体对应一个补丁；补丁集即已接入的突变体列表
• antithesis/scratchbook/mutation-testing/mutants/{id}.md — 各突变体的证据：目标、错误、击杀链、预测和实际判定结果
• antithesis/scratchbook/mutation-testing/interview.md — 商定的路径、答案和范围；后续会话据此恢复工作
• antithesis/scratchbook/mutation-testing/status.md — 扫描状态、基线记录、运行 ID；扫描进行期间可从此处恢复
• antithesis/scratchbook/mutation-testing/history.md — 每次已完成运行的追加式日志：运行 ID、突变体、目标属性、尝试、诊断、采取的措施
• antithesis/scratchbook/mutation-testing/report.md — 每个范围内属性的结果
• 在每个 antithesis/scratchbook/properties/{slug}.md 文件末尾追加一个 ## Falsification 部分
• 重建的 antithesis/scratchbook/property-catalog.md、其证据文件和 existing-assertions.md（仅当原先没有目录时）
• 在用户的实际工作树中应用的断言、工作负载和目录修复

自检

在宣布此技能已完成之前，请根据以下标准检查输出产物；如果支持子 Agent，请安排一位具有全新上下文的审核者，并向其提供此技能文件的路径。

• interview.md 记录了路径、五个回答和商定的范围，并与用户实际授权的内容一致——包括恢复时所做的任何变更
• 在设计任何变异体之前，已在报告的 base_tree 上建立通过的基线，并在 status.md 中记录其运行 ID
• 每项范围内的属性都恰好有一个来自 references/evidence-and-report.md 中“Verdicts and qualifiers”的判定；除 falsified 外，所有判定都有理由，并注明获取该判定时的 base_tree
• 每项证伪都引用运行及证据，将变异体的标记与目标属性反例所来自的历史关联起来——绝不能只引用两个全局运行计数，不能只凭附带损害，也不能因为某个变异体率先触发就将附带损害归功于它
• 每次启动运行都使用了分支的配置目录
• 每个变异体都模拟了针对恰好一项属性的真实开发者失误；没有任何变异体被粗暴改造成破坏行为，也没有缩小工作负载来强行触发杀死
• 对未被杀死的变异体，根据杀死链条中断的环节进行分类，而不是笼统地归为“属性未检测到”
• 根据访谈问题 4 的要求，对真实树应用或提出了修复；绝不只凭静态跟踪应用修复。之后都进行了全新的基线测试和完整扫描；仅针对变异体的修复不会触发这些操作；只要剩余预算足以重新建立基线并重新扫描，就不会遗漏问题 4 授权的任何修复
• 没有因 not mutatable 而撤回任何属性；撤回的条目都附有理由，其证据文件都加注说明而未删除，且报告列出了所有尚无经过验证属性对应的 SDK 断言
• 扫描未超出商定的预算和并发限制，也绝不会在通过 select-mutant.sh 选择变异体到启动之间同时有两个变异体在执行；每次已完成的运行都在 history.md 中有一行记录
• 每个已启动变异体的公告都在启动前经过本地验证，并在其自身的事件记录中得到确认
• 重建的目录在其来源记录中标注为重建，访谈期间已向用户展示其断言扫描结果，且报告说明扫描仅验证了原本就存在的断言
• report.md 列出了每项范围内属性及其判定；对于被证伪的属性，还列出了证明该结论的运行 ID
• 分支已删除，用户的工作树中不含任何变异