antithesis-research

Antithesis 研究

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

目的和目标

研究目标系统，并产出能够推动其余工作流继续进行的草稿手册资料。成功意味着：

• antithesis/scratchbook/sut-analysis.md 记录架构、状态、并发情况和容易出错的部分
• antithesis/scratchbook/property-catalog.md 列出具体、可测试且带有优先级的属性
• antithesis/scratchbook/deployment-topology.md 描述最精简且实用的容器拓扑
• antithesis/scratchbook/properties/{slug}.md 记录每项属性的证据链和背景信息
• antithesis/scratchbook/property-relationships.md 梳理疑似属性群组及属性间的关联
• antithesis/scratchbook/evaluation/synthesis.md 记录分类后的评估结果和已采取的行动

前提条件与范围界定

每次研究开始时，都要询问用户是否有外部参考资料：

开始之前，有没有这棵目录树之外的文档、设计说明、相关仓库、问题跟踪器或其他资料需要我查阅？“仅此目录”也可以。

逐字记录用户的回答。每个外部参考资料都应包含一个 path（或 URL）以及简短的 why 说明。编排器（此技能）会在整个运行期间保留该回答，并将其作为输入传递给每个会产出顶层资料的参考工作流：sut-discovery.md、sut-analysis.md、property-discovery.md、deployment-topology.md、property-evaluation.md。这些参考资料的 Agent 指令部分都会接收此列表作为输入。列表也会记录在每个顶层资料的来源元数据中（参见 references/scratchbook-setup.md）。收到外部参考资料的任何 Agent 都应将其视为待验证的线索，而非事实——参见 references/validating-claims.md。

除范围问题外，只询问无法安全推断的阻碍因素或范围界定决定：

• 如果仓库或代码库的位置尚不明确，请询问其位置
• 如果工作范围小于整个仓库，请询问最重要的子系统或组件
• 询问值得重点调查的已知事故、已关闭的漏洞或特定故障模式

如果草稿手册资料已存在，应将其作为输入并在其基础上扩展，除非用户要求重新开始。

定义和概念

• SUT： 被测系统。
• 工作负载： 为测试目标系统而设计的合成工作负载
• 安全属性（正确性）： 不良情况绝不会发生
• 活性属性（进展）： 良好情况最终会发生
• 可达性属性： 某条代码路径或某种行为可达或不可达
• 测试模板： 位于 /opt/antithesis/test/v1/{name}/ 的测试命令目录。可能有多个测试模板。每条时间线都会执行单个测试模板中的命令。Antithesis 会忽略以 helper_ 为前缀的文件或子目录。
• 测试命令： 测试模板中的可执行文件，且名称带有有效前缀。有效前缀：parallel_driver_、singleton_driver_、serial_driver_、first_、eventually_、finally_、anytime_
• 时间线： 目标系统和工作负载的一次线性执行。Antithesis 会并行运行多条时间线，并对其进行分支，以搜索有意义的行为。

以文档为依据

使用 antithesis-documentation 技能，确保 Antithesis 专用术语和实现建议有据可依。

• 属性和断言：https://antithesis.com/docs/concepts/properties_assertions/assertions.md
• 有时断言：https://antithesis.com/docs/concepts/properties_assertions/sometimes_assertions.md
• 定义测试属性：https://antithesis.com/docs/reference/sdk/define_test_properties.md
• SDK 运行时模式和生产环境行为：https://antithesis.com/docs/reference/sdk.md
• 针对测试进行优化：https://antithesis.com/docs/best_practices/optimizing.md

参考文件

参考资料	阅读时机
references/scratchbook-setup.md	始终先阅读，以初始化工作区
references/sut-discovery.md	通过结构化的关注重点来发现系统特征
references/sut-analysis.md	分析代码库和了解组件的一般方法
references/property-discovery.md	通过结构化的关注重点来发现属性
references/property-catalog.md	记录属性的格式和方法
references/validating-claims.md	如何看待文档和问题中的主张——在以此为依据之前先验证
references/faults.md	了解故障类型、静默期和进程故障的可用性
references/deployment-topology.md	为 Antithesis 设计容器拓扑
references/property-evaluation.md	将属性目录作为一个整体进行评估

推荐工作流

完整研究流程（新项目）

1. 阅读 references/scratchbook-setup.md
2. 阅读 references/sut-discovery.md 和 references/sut-analysis.md
3. 使用 references/sut-discovery.md 中的多 Agent 或单 Agent 工作流分析系统
4. 扫描代码库，查找现有的 Antithesis SDK 断言。搜索 Antithesis SDK 的导入，以及对断言函数（assert_always!、 assert_sometimes!、assert_reachable!、assert_unreachable! 或其 非宏版本）的调用。对于找到的每条断言，记录文件路径、行 号、断言类型和消息字符串。将结果写入 antithesis/scratchbook/existing-assertions.md。按照 references/scratchbook-setup.md 的要求，在文件开头添加来源前置元数据。如果未找到 断言，则在文件中注明并确认代码库没有现有的插桩。
5. 阅读 references/property-discovery.md 和 references/property-catalog.md
6. 使用 references/property-discovery.md 中的多 Agent 或单 Agent 工作流发现属性
7. 阅读 references/deployment-topology.md
8. 设计部署拓扑，并将其写入 antithesis/scratchbook/deployment-topology.md
9. 阅读 references/property-evaluation.md
10. 使用 references/property-evaluation.md 中的多 Agent 或单 Agent 工作流评估属性目录
11. 处理评估结果：进行完善、补全缺漏，并将偏差上报给用户
12. 在 antithesis/scratchbook/ 下编写或更新其余所有发现结果

定向属性研究

1. 如果系统模型缺失或已过时，请阅读 references/sut-discovery.md 和 references/sut-analysis.md
2. 阅读 references/property-discovery.md 和 references/property-catalog.md
3. 使用 references/property-discovery.md 中的多 Agent 或单 Agent 工作流发现属性
4. 将声称的保证转化为明确的属性。对于事故和错误报告，在将所报告的问题作为属性之前，请确认它确实是系统缺陷（参见 references/validating-claims.md）。为每项属性选择匹配的 Antithesis 断言类型
5. 更新 antithesis/scratchbook/property-catalog.md，并记录假设或待解决的问题
6. 将新属性的证据文件写入 antithesis/scratchbook/properties/{slug}.md
7. 如有新的簇或关联，更新 antithesis/scratchbook/property-relationships.md
8. 阅读 references/property-evaluation.md
9. 使用 references/property-evaluation.md 中的多 Agent 或单 Agent 工作流评估更新后的属性目录
10. 处理评估结果：进行完善、补全缺漏，并将偏差上报给用户

属性扩展（分流后）

1. 阅读 references/property-discovery.md 和 references/property-catalog.md
2. 查看 antithesis-triage 技能的分流发现
3. 使用 references/property-discovery.md 中的关注重点，寻找受分流发现启发的新属性
4. 更新暂存手册中的相关文件
5. 将新属性的证据文件写入 antithesis/scratchbook/properties/{slug}.md
6. 在 antithesis/scratchbook/property-relationships.md 中更新任何新集群或关联
7. 如果扩展内容较多（新增一个属性类别或新增属性超过 3 个），阅读 references/property-evaluation.md 并评估更新后的目录。现有类别中新增 1-3 个属性的小幅扩展，无需进行完整评估。

通用指导

• 优先选择具体、可检查的保证，而不是“测试故障转移”之类模糊的目标
• 如果系统文档或注释声称某项保证成立，就将其作为待测属性；该属性负责验证这一说法，不要在分析中直接断言该保证成立
• 问题中的缺陷报告只是线索，并非事实。在以此为基础开展工作前，请确认所报告的缺陷确实存在于系统中（参见 references/validating-claims.md）
• 不仅要记录不变量，还要说明为什么所选的 Antithesis 断言类型在语义上适合该属性
• 对于活性或非平凡语义状态，使用 Sometimes(cond)；不要将其用于必须在每次评估时都成立的不变量，也不要用它替代 Reachable(...)
• 找出在哪些地方，精简的 SUT 端断言相比仅检查工作负载能显著改善搜索引导，尤其是针对罕见、危险、对时序敏感或外部不可见的状态
• 请记住，Antithesis SDK 断言失败时不会导致程序崩溃；这些断言旨在安全地用于生产代码，在 Antithesis 之外通常会退化为低开销后备机制或空操作
• 聚焦 Antithesis 最擅长的场景：对时序、并发和部分故障敏感的情况
• 保持部署拓扑精简；每增加一个容器，都会扩大状态空间
• 在暂存手册中记下假设和未决问题，不要将其们留作隐含信息
• 如果只要求完成部分研究，仍要更新相关暂存手册文件，并注明尚未完成的事项

输出

• antithesis/scratchbook/sut-analysis.md
• antithesis/scratchbook/existing-assertions.md
• antithesis/scratchbook/property-catalog.md
• antithesis/scratchbook/deployment-topology.md
• antithesis/scratchbook/property-relationships.md
• antithesis/scratchbook/properties/{slug}.md（每个已编入目录的属性对应一个文件）
• antithesis/scratchbook/evaluation/synthesis.md
• antithesis/scratchbook/evaluation/{lens}.md（每个评估视角对应一个文件）

除属性证据文件外，上述列表中的所有顶层暂存手册产物都应包含来源 frontmatter，记录 sut_path、commit、updated 和 external_references。属性证据文件继承 property-catalog.md 中的上下文，无需自己的 frontmatter。参见 references/scratchbook-setup.md。

这些输出应足够具体，以便 antithesis-setup 技能和 antithesis-workload 技能直接使用。

自检

在宣布此技能已完成之前，请根据以下标准检查你的工作。如果你的 Agent 支持生成子 Agent，请使用全新上下文创建一个新 Agent 来执行此检查——向它提供此技能文件的路径，并让它阅读所有输出产物。使用全新上下文的审核者能够发现当前上下文中的检查容易遗漏的问题。如果你的 Agent 不支持子 Agent，请自行检查：重新阅读本文件顶部的成功标准，然后逐项对照实际输出，系统地检查以下每项标准。

检查标准：

• antithesis/scratchbook/sut-analysis.md 存在，并涵盖架构、状态管理、并发模型和容易出错的区域
• antithesis/scratchbook/existing-assertions.md 存在，并列出在代码库中找到的所有 Antithesis SDK 断言（或明确说明未找到任何断言）
• 证据文件能正确区分代码库中已有、部分存在和缺失的插桩——没有证据文件建议添加已存在的断言
• antithesis/scratchbook/property-catalog.md 存在，包含符合 references/scratchbook-setup.md 要求的来源前置元数据，并列出具体且可测试的属性——而不是“测试故障转移”之类含糊的目标
• 每项顶层产物都以符合 references/scratchbook-setup.md 要求的来源前置元数据开头
• external_references 列表反映用户说明的范围；引用过的条目都附有说明其用途的 why 注释
• 在运行开始时提出了范围问题，并将用户的回答传递给了每个执行分析的子 Agent
• 每个属性都有一个描述性 kebab-case 标识作为其规范 ID
• 每个属性都有优先级，并说明选择对应 Antithesis 断言类型（Always、Sometimes、Reachable 等）的理由
• 需要内部控制分支的引导或重放锚点的属性，指出可能的 SUT 侧插桩点，而不只是工作负载可见的检查
• antithesis/scratchbook/deployment-topology.md 存在，并描述了最小容器拓扑——每个容器都有存在理由
• 每个编入目录的属性都有对应的证据文件 antithesis/scratchbook/properties/{slug}.md，其中记录了证据链、相关代码路径和关键观察结果
• 每个属性的目录条目都包含“开放问题”列表，与其证据文件中未解决的问题相对应（简要概述；完整上下文保留在证据文件中）。已解决的问题应移除；剩余问题应按 references/property-catalog.md（“开放问题约定”）中的规定标记。
• 每个 (partial: ...) 或 (needs human input) 标记都必须有证据文件中的调查日志条目作为依据（见 references/property-catalog.md 中的“调查日志”），记录检查了什么、发现了什么以及还有什么未查明。未标记（尚未调查）的问题不需要日志条目。需要人工输入的未解决问题是可接受的结果——必须在目录概览中清晰呈现，不能只藏在证据文件里。
• 经调查后判定无效的属性，须在目录中标明并说明原因
• antithesis/scratchbook/property-relationships.md 存在，并将相关属性归为若干簇，简要说明推测的关联和主导关系
• property-relationships.md 中引用的每个属性标识都对应目录中的一个属性
• 属性应聚焦于 Antithesis 最擅长的场景：对时序敏感、对并发敏感以及部分失败场景
• 文档或注释中声称的保证都应转化为待测试的属性；分析不得将任何保证表述为已确立的事实
• 如果从错误报告中提到某个具体缺陷存在，必须引用一手证据，证明该缺陷确实存在，并排除报告者的环境或配置问题——不能只链接到问题报告或指出症状相符
• 已完成属性评估：antithesis/scratchbook/evaluation/synthesis.md 存在，并按类别整理发现
• 已将评估后的优化应用于目录
• 已通过有针对性的探索补齐评估中发现的缺口，并将由此得到的属性连同证据文件一并加入目录
• 已向用户展示评估偏差（如有）及其支持证据
• 输出足够具体，antithesis-setup 和 antithesis-workload 可以直接使用——没有含糊的步骤或缺失的细节