---
name: formal-docs-landing
description: 定义期第 6 步，正式落盘：判断哪些设计写成长期维护的正式文档、哪些以源码为文档，按产品、项目顶层、领域包组三层落盘，做五类判据的确定性文档评审；形式化件同样落盘并验证。细化设计完成，或人说「落盘」「写进正式文档」「评审文档」时加载。改代码不改设计不加载。
---

# 正式落盘

定义期的最后一步。把定义期定下来的东西分成两类：长期维护的写进正式文档，读代码更快的以源码为文档。这一步完成就进入交接期。

## 判据

看读代码的效率是否低于读文档。

| 以源码为文档 | 写正式文档 |
| --- | --- |
| 应用服务接口、函数签名、类型形状：代码本身说得清 | 统一语言：词的定义读代码读不出来 |
| 单个模块的内部结构 | 领域边界与职责：谁拥有什么，读代码要翻很多文件 |
| 测试用例：它们就是行为的说明 | 领域协作图与上下文图：关系跨文件跨包 |
| 配置项的取值 | 不变式与它们的守法：散在代码里看不全 |
| | 形式化的定义、模型与证明，以及它们对应代码的哪些步骤 |
| | 已定的取舍与为什么不选另一条路 |

每项设计产出都在[落盘决定表](landing-template.md)里标一个结论，不留「都写一点」。

正式文档是写的人交给没有本次上下文的读者，交出之后的代理只依赖它。转手会丢信息，回路越紧越稳，一块多大由接的一方验得完多少定。做法加载技能 `think-closed-loop`。

## 三层

| 层 | 放什么 | 位置 |
| --- | --- | --- |
| 产品文档 | 概念、边界、产品规则与取舍 | 从项目接入点取 |
| 项目顶层文档 | 要求、架构、领域关系、工程约定 | 从项目接入点取 |
| 领域包组文档 | 本领域的架构、规格、技术与领域说明 | 随包 |

每份正式文档只写最终做法，不写版本对比与推导过程；历史归变更记录。文档不依赖对话记忆：没有「如前所述」「按我们讨论的」。写法加载技能 `pstack:technical-writing`；写给代理读的部分加载技能 `mattpocock-skills:writing-for-agents`。

形式化的定义、模型与证明同样落盘，并记录模型对应代码的哪些文件与函数、最后一次确认一致的提交。

## 文档评审

评审用确定性判据，不做对抗性评审。评审者拿到的是落盘决定表和文档，逐条核，不评价写法好坏。派只读子代理时按 `delegate-brief` 的派评审者一节。五类判据：

| 判据 | 核什么 | 怎么报 |
| --- | --- | --- |
| 落盘遗漏 | 决定表里标了「正式文档」的，文档里有没有；本程更正过的裁定，文档是按更正后的写 | 列缺的点与该落的位置 |
| 工作日志式表达 | 把过程、会话或草稿状态写成了规范的句子 | 只列句子，不改写 |
| 断链 | 链接与锚点能不能解析 | 命令从项目接入点取；失败的原样列出 |
| 下层违背上层 | 下层文档与上层已接受承诺矛盾的两处原文；下层写了持久化形态（表、行、记录种类、一次提交写什么）时，逐条对照上层的持久化不变式（什么是事实、什么是可重建的状态、一次提交里必须一起写的东西） | 引原文，不引概括；持久化形态每条写对照的是上层哪一条、符合还是矛盾 |
| 图 | 有必要补的图和建议补的图；只在图能降低理解难度时建议 | 写放哪一节、说明什么关系 |

各面分开交回。没有发现时写没有发现，并写清看过的路径。

## 进入交接期

文档评审无未处理项，形式化件已落盘并验证，就进入交接期：定约、定程、交出，交出时走一遍交接点核对单。一程的承诺、大小与交出收回归交接期，由设计会话做，人在场。做法加载技能 `pass-the-baton`。