spec-rigor-review

用途

spec-rigor-review 是一个代码库审查技能，用于找出那些“本可由机器强制执行”的规则，以及让这些规则可被强制执行所需的代码重构。它的核心判断是：写在注释、命名约定或某个人记忆里的规则，没有任何东西在执行它。

该技能把可强制执行的规则分为三类：

技能定义了一套审查流程：

确定范围：使用用户指定的路径、包或 diff。若用户未指定，则选择包含业务规则、状态转换和与其它系统边界的包，并说明选了哪些。默认不审查整个仓库。
阅读现状：检测语言、正在使用的模式与生成器、任何模型或证明；找到运行每项检查的命令及其接入位置。只有在不改变任何内容且不下载任何内容时才运行检查，并记录其退出码。
寻找候选：通过 techniques/schema-candidates.md、techniques/model-candidates.md、techniques/proof-candidates.md 寻找候选规则。
审计现有检查：通过 techniques/audit-existing.md 审计。一个无法失败的检查比没有检查更糟，因为它报告了并不存在的安全性。
寻找阻碍：通过 techniques/refactors.md 找出阻碍。
排序：在每个表内按（违规成本）×（该检查捕获违规的概率）÷ 工作量排序。金钱、权限、状态机以及与其它系统的边界排在最前。优先选择能表达该规则的最便宜层次：类型先于模式检查，模式检查先于模型，模型先于证明。
报告后停止：审查是只读的，在用户选定发现项之前，不编辑文件、不安装工具、不触发下载。
编写用户选定的检查：遵循 techniques/writing-checks.md，并用 techniques/triage.md 处理每个反例和每个未证明的目标。

报告以“What exists”开头：语言、模式与生成器、模型与证明、运行每项检查的命令、以及是否接入 CI。

随后是各分节，每节按最有价值的发现排在最前。每个发现都有 ID（S1、V1、W1、R1）。某节没有发现时用一行说明。字段较短时用表格，否则给每个发现一个带标签的块。

模式与类型候选（S）：位置、一句话规则、证据、当前如何执行、建议的执行方式、工作量（S/M/L）。
验证候选（V）：位置、一句话不变量、证据、工具、将提供的保证（采样、有界、有限模型上穷尽、或已证明）、工作量。需要先重构的候选标注“needs R1”，其工作量不含重构。
薄弱现有检查（W）：位置、哪项审计检查失败、有问题的行或命令、最小修复。每个失败检查一行。
重构（R）：位置、阻碍、建议改动、解锁的检查、工作量。
未覆盖（Not covered）：因缺乏证据而排除的规则及什么能确定它们、更适合属性测试或模糊测试的规则（指向 test-rigor-review）、以及这些工具都捕获不到的缺陷。

位置用 file:line 或跨行时的行范围表示。每个反例、以及每个“检查无法失败”的断言，都要标注为 predicted 或 confirmed；只有实际运行过才算 confirmed。审查期间要确认某个断言时，在仓库之外的临时副本中操作。

报告结尾给出首先要做的三件事及各自理由。相互依赖的发现（如一个重构及其解锁的检查）算作一件。

每条规则都需要证据，来自文档、名称与签名、代码中已有的断言、现有测试，或用户陈述的业务规则。用户拥有规则。绝不发明规则，也绝不为让检查通过而弱化规则。当一条陈述的规则有两种读法时，报告两种读法并询问指的是哪一种。
一个发现是一条人能用一句话检查的规则。若无法如此简短地陈述，就还不适合报告。
检查只有在被观察到失败后才算数。对于自己写的检查，故意破坏规则一次并记录命令、非零退出码和输出。对于审计的检查，尝试在临时副本中让它失败。
精确陈述保证。采样不是穷尽，有界不是证明，证明覆盖的是写下的规格而非其背后的意图。
说明模型如何与代码保持关联。若关联是手动的，要说明。
从项目及其文档学习每个工具的语法。不要凭记忆写语法；这些工具每月都在变。

对照用到的每个技术文件检查工作。跳过的内容要在“未覆盖”下给出理由。

技术文件包括：

适用于希望把隐含规则显式化、并让机器强制执行这些规则的代码库审查场景，尤其关注业务规则、状态转换和系统边界。

限制：该技能是只读审查，不直接修改代码；每条规则必须有证据，不能凭空发明；检查必须被观察到失败才算数；保证需精确陈述，采样不等于穷尽、有界不等于证明。关于具体收费、价格、平台支持等信息，资料中暂未提供。