正式落盘

位置：定义期第 6 步。上一步 detailed-domain-design，下一步 pass-the-baton。顺序与例外见入口技能 single-session-dev-flow。

定义期的最后一步。定义期产出的东西很多，能进项目正文的很少。这一步把它们分成三路：约束落到它的拥有者；源码已经表达的不写；这一程自己用的材料留在过程目录。这一步完成就进入交接期。

例：一程定下了「失败的调用不能让这一轮记成完成」。它是一条不变式，写进规格。为它试过的三种做法、选中这一种的推导、验收用的命令，是这一程的材料，留在过程目录。重试函数的签名在源码里，不写。

为什么少写

文档每多一份，以后每次改动就多一处要同步的地方。没人同步的文档会说错话，读它的代理照着错的做。所以进项目正文的只有约束，而且每条信息只有一个源头：源码说了的，文档不再说；写成了检查或证明的，文字不再留。

判据

能约束以后开发的只有四样。一项设计产出进不进项目正文，只问它是不是这四样之一：

一条约束落在它能落的最强的一样上：能证明的写成形式化模型，能机械判定的写成静态检查，这两样都装不下的才写成文字。写成了检查或证明，文字版就删，规格里的不变式用一句话指过去。

规格里的「应然设计」写目标语义：失败、未知、取消、恢复、并发下应当怎样。写成规则，不写成实现。

不是这四样的各有去处，都不进项目正文：

每项设计产出都在落盘决定表里标一个去处，不留「都写一点」。

一程的 spec 不是项目的规格。spec 是这一程的承诺，装验收标准、实现决定与切片，放在过程目录，一程结束就清理。这一程改了应然的，把改的那几句写进项目的规格。

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

落在哪

位置从项目接入点取。槽位名沿用「三层正式文档的位置」，装的只是约束类文档。项目没填时按下表：

一个领域只有一份规格，领域下面的模块不各带一份：边界与不变式是领域的性质，模块只是工程上的拆分。项目有产品规则时，产品规则是产品这一层的规格，位置从接入点取。

怎样写

每份约束类文档只写最终的应然，不写版本对比、推导过程与日期；历史归版本库。文档不依赖对话记忆：没有「如前所述」「按我们讨论的」。不写实现状态：没做的事在代码里就是没做，文档不记它。写法加载技能 pstack:technical-writing；写给代理读的部分加载技能 mattpocock-skills:writing-for-agents。

已有的文档与这一程定下的应然矛盾时，改掉或删掉矛盾的那一段，不在旁边补一段新说法。

形式化的定义、模型与证明同样落盘。模型里的名字取自代码，对应关系靠名字，不另记一份对应哪些文件、哪个提交的清单。

文档评审

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

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

怎样防止长回来

项目能挡的让检查去挡，不靠每一程自觉：新模块的模板不生成文档；允许出现的文档列成白名单，白名单之外的进不了仓库；规格的标题与体量有检查；正文里的日期、工单号与实现状态被检查拒绝。项目没有这些检查时，在交付声明里写一句「没有防止多写的检查」，这一程不自己加。

进入交接期

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