以证据为先的文档 是做什么的？
文档不是关于系统的故事。它是一本声明分类账：每一个实质性陈述必须可追踪到一种机制和证据，其限制条件与声明在同一位置说明。
一句自信的话很廉价。工作是让读者能够分辨出哪些已被证明、哪些已测试、哪些仅被审查过、以及哪些仍悬而未决。
核心规则
每个实质性声明包含四部分：
- 机制 — 系统中什么部分使该声明成立。
- 证据 — 证明性工件：证明、模型、测试、分析报告、追踪、基准测试或审查记录。
- 范围 — 声明的适用范围以及信任边界之外的内容。
- 状态 — 证据支持的最强真实标签。
如果缺少其中之一，则声明未就绪。将其重写为设计意图、计划或开放问题——不要将其伪装成结果。
声明分类账
在文档中或链接的证据文件中维护一个表格：
| ID | 声明 | 机制 | 证据 | 范围 / TCB | 状态 | 限制条件 | 最后验证时间 |
|---|---|---|---|---|---|---|---|
| C-01 | 只有角色X可以写入表T | 权限检查 + 数据库策略 | 负面测试 T-04..T-11 | PostgreSQL 14–17；角色Y、无角色会话 | 已测试 | 超级用户和DBA不在威胁模型内 | 2026-11-02 |
规则：
- 每行一个声明，而不是每个文档一行。
- 声明必须可证伪。“系统是安全的”不是声明；“角色Y无法通过任何受支持的入口点写入T”才是。
- 链接工件，而不仅仅是工具名称。“SARIF”是一种格式；报告路径和已审查的规则集才是证据。
- 当工件重新运行时更新
最后验证时间；过时的证据是一个发现，而不是一种形式。 - 保留负面结果。“我们试图破坏它但因X而失败”是证据；隐藏它会造成错误的覆盖错觉。
状态阶梯
使用证据支持的最强标签，绝不使用更强的标签：
| 状态 | 含义 |
|---|---|
proven (已证明) | 基于声明的假设和TCB的机器检查证明 |
model-checked (已模型检查) | 对模型的穷举或有界探索；说明边界和模型到代码的差距 |
tested (已测试) | 尝试违反声明的已执行测试，记录环境和结果 |
static-refinement (静态精化) | 静态分析或精化检查；说明工具、规则和未解决的发现 |
reviewed (已审查) | 仅人工审查；无可执行或形式化证据 |
open (开放) | 声明存在但证据不存在；这是一项风险，而非结果 |
较低的状态并非失败。夸大的状态才是。
不要写 verified、proven、correct、secure、safe、complete、guaranteed、certified 或 compliant 而不附带相邻的状态和范围。如果该词能在没有证据的情况下幸存，就删除该词。
证据强度
优先选择能够因正确原因而失败的证据：
- 在显式假设下对所声明属性的形式证明。
- 在声明边界内的穷举模型检查。
- 基于属性或模糊测试，附带记录的语料库和预言机。
- 当机制被移除时会失败的有针对性负面测试。
- 带有审查规则集和分类处理的发现的静态分析。
- 具有命名审查员和检查列表的代码审查。
- 断言或轶事。
层次并非绝对：一个有针对性测试可能比误用的证明更强。将证据与声明匹配。一个模型证明但不能精化代码的，不能证明代码。一个因平台首次拒绝才通过的测试，不能证明你的防护。
范围和信任边界
在声明旁边说明边界，而不是在遥远的附录中：
- 涵盖的版本和平台。
- 排除的特权角色：超级用户、DBA、部署管理员、秘密管理器、构建系统、操作员。
- 假设：加密原语、时钟、网络、存储、租户隔离、配置。
- 哪些是符号建模的，哪些是真实执行的。
- 哪些超出范围及原因。
一个不受限定的声明是关于一切的声明，这几乎总是错误的。“针对角色Y，在配置文档化的PostgreSQL 14–17上安全；DBA在模型之外”既诚实又有用。
工作流
- 清单声明。 阅读文本，标记每一个断言属性、结果、保证或合规状态的句子。
- 分类每个声明。 它是设计意图、需求、实现事实、测试结果、形式结果还是发布声明？
- 分配ID和状态。 添加机制、证据、范围、限制条件和
最后验证时间。 - 将声明与工件进行测试。 打开报告，重新运行命令，或询问缺失的工件。不要接受文件名作为证据。
- 重写无支持的声明。 将其转换为“设计意图”、“已计划”、“尚未验证”或开放问题。保留雄心；删除虚假的确定性。
- 检查反面情况。 对于每个安全或正确性声明，命名尝试违反它的测试或分析。如果没有，则将声明标记为
open。 - 审查语言。 删除禁词、模糊量词和不受限定的绝对词。参见
references/banned-words.md。 - 固化证据。 记录命令、提交ID、环境、日期和工件路径，以便评审人能重现结果。
- 门控发布。 发布说明只能声明分类账支持的内容。明确列出剩余风险和开放声明。
审查清单
- 每个实质性声明都有ID、机制、证据、范围、状态和限制条件。
- 每个
tested状态的声明都命名一个在机制被移除时可以失败的测试。 - 每个
model-checked状态的声明都说明边界和模型到代码的差距。 - 每个
proven状态的声明都说明假设和TCB。 - 负面结果和已知失败都呈现出来，而不是被过滤掉。
- 日期和版本是最新的；过时的证据会被标记为过时。
- 特权角色和超出范围的路径都被命名。
- 没有禁词出现在没有相邻证据和范围的情况下。
- README、架构文档、API合同和发布说明之间不矛盾。
- 读者可以仅凭文档重现证据。
反模式
- 未来时态。 “系统强制……”而它只是一个计划。
- 文件名作为证据。 “详见 report.pdf”但没有结果、范围或日期。
- 工具名作为证明。 “使用静态分析验证过”但没有规则、发现和分类处理。
- 范围漂白。 将狭窄的测试结果呈现为全产品范围的保证。
- 绿灯套件绝对主义。 “所有测试通过”但没有说明哪些测试、在哪些平台上、以及它们试图违反什么。
- 合规扮演。 将标准名称用作证书；映射不是审计。
- 隐藏限制条件。 附注存在但远离声明。
- 过时的确定性。 将旧提交的结果呈现为当前状态。
- 没有负面证据。 只记录成功；失败和拒绝消失。
输出形态
当被要求撰写或审查技术文档时，生成：
- 一份简短的声明摘要，按状态计数。
- 声明分类账（内联或链接）。
- 开放声明和残余风险，明确与结果分离。
- 范围和假设，紧邻它们限定的声明。
- 证据索引，包含路径、命令、日期和版本。
使用 references/evidence-template.md 作为分类账和发布说明的模板。发布前使用 references/banned-words.md。如果仓库包含标准交叉引用，则位于 references/standards-map.md；技能本身不依赖于某个标准。
根据文档规模调整输出。简短的发布说明需要紧凑的声明表格和简短的残余风险部分，而不是完整的审计包。认证证据文件需要完整的分类账、证据索引和范围。不要将详尽性与长度混淆；每一行都必须携带读者需要的信息。