设计与代码的建模/自动化审查（dsh-model-everything）
English · 中文
把设计与代码里的断言抽象成模型，交给引擎跑一遍：结论带出处与哈希，能复算、能比对。让结论来自一次运行，而不是一次通盘推理：把「想清楚」变成「跑一遍」。
DeepSeek Harness 原生插件。把设计与代码里关于行为的断言变成可运行、可审查、可导出的模型：
- 核验断言：逐条对着源码检查，引用到
file:line。
- 跑模型：状态机、协议、多机协作、数据模型先建成可执行模型，再交给引擎跑。
- 审图：UML 图按模型读、按模型审，并与模型对照。
- 对照重构：重构前后各建一份模型，两份报告摆一起比。
- 留痕：结论固化成带哈希的报告，可复算、可比对、可导出。
能力范围
| 域 | 做什么 |
|---|
| 事实核验 | 把一份设计/规格/评审意见里的可验证断言列出来，逐条对着代码核验并给出出处。核不了的直接说明 |
| 行为验证 | 状态机与协议：结构检查、对抗性探测、预算与时限、before/after 回归。多机组合查死锁，以及永不发生的会合（握手事件） |
| 图 | UML 2.5 各图族的渲染、解析与建模审查（含 render→parse 往返一致性对照），覆盖 Mermaid 与 PlantUML 两种记号 |
| 结构 | 组件/包/类/部署图按依赖图审计：孤立节点、悬空引用、环、矩阵与分层违规、缺失的必需边 |
| 数据 | 数据模型与迁移：结构、迁移覆盖、拷贝一致性、回滚对称、前后数据回归 |
| 并发 / 同步 / 异步 | 挖掘"工作怎么被执行"的断言（线程安全、锁、中断、async/await、事件循环…）并路由到能判定它的工具；它自己不证明 |
| 导出 | 已验证模型导出为 UPPAAL / TLA+ / PRISM / SPIN 的输入 |
| 报告 | 报告正文渲染、基线比对（report_diff）、哈希规范 |
典型用法
重构 harness
重构可以改实现，不能改行为。这个判断交给引擎，不必通读 diff：
- 重构前：从当前代码抽出 BEFORE 模型（
uml_parse 读已有的图，或按 schema 手写）。
- 重构。
- 重构后：抽出 AFTER 模型。
- 回归：
model_verify 带 beforeModel 与 stateMapping 跑前后回归：行为是否保持、不变式是否连续、状态映射是否自洽。数据侧用 model_datamodel_verify 的 beforeModel / fieldMapping / migrationMappings 做同一件事的数据版。
- 判定与留痕：
report_diff 拿基线报告比对。新增的 error 发现，就是这次重构不接受的理由。报告里的哈希让结论可复算。
它比较的是你给的两份模型，不是两份代码。每份模型是否忠实于对应代码，由第 1、3 步负责，它不代替你做。它也不读 diff、不改代码、不跑你的测试。它回答的是"行为还一样吗"，不是"重构得好不好"。
代码流程审查
先把分支逻辑画成流程，再看这张图到底说了什么：
- 抽流程：把函数或服务里的分支写成
LogicModelV1，或者手画一张 stateDiagram-v2 / PlantUML 图。
- 读回模型：手画的图交给
uml_parse 转成模型。读不动的行会变成警告，不会悄悄跳过。
- 审查：
uml_review 报结构缺陷——不可达状态、死端、分支有歧义或没穷尽、自环没有出口、孤立节点、环——以及文档缺口。
- 落回源码：每条发现都回到代码核验。图画对了，不等于代码写对了。
它审的是你给的那张图和那份模型。图与代码是否一致，由第 1 步的抽取负责。
状态机审查
把状态机建成可执行模型，让引擎去跑，而不是通读代码判断它会不会卡死：
- 建模型：手画的
stateDiagram-v2 或 PlantUML 状态图交给 uml_parse；也可以直接按 schema 写 LogicModelV1。
- 跑检查：
model_verify 找的是不可达状态、吸收环、被静默忽略的事件、没有恢复路径的资源申请、预算超限，以及无法满足的时限。每一项都作为一个带码的发现报出，而码的前缀说明它属于哪一族。
- 写清"永远/绝不"：把这类断言写进
invariants，引擎会在全部可达状态上搜反例，并给出它找到的最短路径。
- 落回源码：报告里的 error 发现逐条回到代码。
并发断言分两半：两个模型都碰同一个共享位置这一类，由我们自己的 model_compose_verify 判（声明 shared 与 accesses 之后的 C3/C4/C5，包括丢更新）；源码级数据竞争、中断延迟、阻塞调用与漏掉的 await 仍路由到 TSan/Helgrind/CBMC/TLA+。硬实时语义（deadline、period）不在它的范围内。
审计一张依赖图
组件图是关于「哪些模块可以依赖哪些」的断言。把它当图读，再问那些边是否被允许：
- 给图：PlantUML 的组件/包/类/部署图源码，或 Mermaid 类图。
uml_structure_verify 把它解析成节点与边。
- 说清什么被允许（如果有规则）：一个含
layers 与 rules 的矩阵，每条规则点名一个 source 并给 allow / deny / require，再用 default 管其余。没有矩阵时，它只报结构缺陷。
- 读发现：孤立节点、从未声明过的端点、带最短路径的环、越过层的边、缺失的必需边，以及——一个节点都没声明时——这份输入没有任何可审的东西。
- 换一种图就换个工具：如果这张图是状态图或活动图，那是
uml_review，不是它。
它审的是图，不是代码。一张自洽的图仍可能画错了系统，所以要和源码侧扫描配对。手画的图报「标签漂移」时，uml_explain_labels 会打印该记号下解析器接受的标签写法。
让设计对自己作出的声明负责
设计会对自己作出断言：这一层在那层之上、这个组件拥有那条依赖、这个接口比它的调用方窄。model_design_review 判定设计是否守住了这些承诺：
- 把设计写成模型：架构（节点与边），加上它声明的——分层、边界、允许与必需的边、带职责的类型、操作、转移、父类型。
- 跑它：
model_design_review 报出设计与自相矛盾的地方，并另外报出它图的形状——环与打断环所需的最少边、承重元素、层级、扇入扇出。
- 读那三个列表：
violations 决定判定；signals 值得一看但不使任何东西失败；facts 是测量，不是发现。checksSkipped 说明哪些原则因为没声明任何可对照的东西而没有检查。
它从不按外部标准评判设计。 它报的是：设计与它自己声明的某件事矛盾，或关于它的图的一个结构事实。问「这个设计好不好」是评审者的问题；这个工具回答的是另一个：它就自己的说法而言，站得住吗。
两台必须互相配合的机器
一台机器不会因为另一台而死锁。当两个组件握手时，真正有意思的失败在组合里：
- 各自建模，然后一起给：
model_compose_verify 收一个模型数组。
- 点名共享事件：如果一个握手只有在双方都就绪时才合法，把它写进
rendezvous。没写进去的事件只推进一台机器，所以等握手的机器可以先走任意多步自己的路。
- 读 C1 与 C2：一个可达节点上没有任何机器能前进、且有机器不是终止态（C1），以及一个永远不会触发的会合（C2）。两者都逐机给出理由，C1 还给最短反例。
模型里没有速率比，也没有公平性约束。单台机器自己的问题——不可达状态、不变式、成本对预算——用 model_verify。
并发声明：挖掘并路由
「线程安全」「lock-free」「ISR 安全」都是需要某个能判定它们的工具的断言，而第一步是把它们找出来：
- 扫文本：
model_interleaving_scan 收文档、计划或笔记，报出风险点——那条声明、共享状态、中断、临界区，以及异步的那些（async、await、promise、事件循环、回调）。每条发现都带 family（threads / synchronization / async / interrupts / shared-state），绝对式断言按 error 报。
- 看每条绝对声明欠着什么：「不可能有数据竞争」这类声明会被报为 error，要求专门的验证，且每条发现都点名能判定它的分析——竞争用 TSan 或 Helgrind，有界证明用 CBMC，协议用 TLA+，中断用 RTOS 感知的分析。
- 去做那个分析：本插件不运行它，也不对并发安全作任何证明。
它读的是文本。它看不见你的线程，而一次干净的扫描不是健康证明——它的含义是没找到声明，这是另一个命题。
一次迁移：前后两份模型
迁移是两份模型，加一个「数据活下来了」的断言。把两份都给出去，这个断言就变成可核查的：
- 两份模型：改动前的 schema 与改动后的 schema，各自是含实体、字段、键与关系的数据模型。
- 说清字段怎么走：
fieldMapping 从旧路径到新路径，加上 migrationMappings——用于来源不是它自己旧名字的字段。
- 跑比对：
model_datamodel_verify 带 beforeModel，检查迁移覆盖、拷贝一致性、回滚对称，以及前后数据回归。
- 读那条警告：新 schema 里声明为
required、却没有任何东西供给它的字段，会报 DS2_REQUIRED_FIELD_UNSOURCED。它是 warning，所以判定停在 pass_with_findings——这是一个要做的决定，不是引擎可以替你宣布的失败。
它比较的是你给的两份模型。任一份是否忠实于它所描述的数据库，是抽取那一步的事，这个工具不做。
图的导入与导出：设计冻结与长期迭代
这里存的是源文件，不是截图：uml_render 写出 Mermaid / PlantUML 源，uml_parse 把源读回模型。一份图因此能当两种东西用：
- 设计冻结的留档：把图源、模型和那一次的验证报告一起提交进仓库，作为某个时间点的设计记录。模型里可以放
_ 前缀的元数据（单据号、日期、负责人、抽取时留下的保留意见），这些键不参与哈希，补档案信息不会改变结论的身份。
- 长期迭代的参考：下一次改动时重新抽出模型、重跑验证，再用
report_diff 与冻结的那份报告比对。新增的 error 是这次改动引入的，消失的说明旧问题已经解决；哈希让"还是不是同一份模型"可判定，不必肉眼比图。
需要交给外部检查器时，同一份模型可以用 model_export 导出成 UPPAAL / TLA+ / PRISM / SPIN 的原生输入。
界线：它保存并比对的是模型与图的源文件，渲染出来的图片只是副产品。图变了模型没变、或模型变了图没变，都会在下一次解析或比对时暴露。
工具
| 工具 | 做什么 |
|---|
uml_render | 模型 → 图源（Mermaid / PlantUML），可指定图族。记号表达不了的视图会被拒绝，并说明理由 |
uml_parse | 图源 → 该图族的模型；不属于状态机/流程的族会按名拒绝，而不是硬当作状态机解析 |
uml_review | 审查建模：结构缺陷、文档缺口、render↔parse 往返一致性；给模型、给图，或两者对照 |
uml_explain_labels | 打印解析器接受的标签与注释契约，不需要图 |
model_verify | 状态机 / 协议的可执行验证（结构检查、对抗性探测、预算、时限、前后回归） |
model_compose_verify | 两台及以上机器的组合检查（死锁、永不发生的会合；声明了共享位置后还有无序写 C4 与非原子更新 C5） |
model_datamodel_verify | 数据模型与迁移验证 |
model_interleaving_scan | 并发 / 同步 / 异步声明的挖掘与路由 |
model_export | 导出到外部检查器（UPPAAL / TLA+ / PRISM / SPIN） |
uml_structure_verify | 依赖图审计（含依赖矩阵与多层级细化） |
model_design_review | 设计审阅：依赖图形状 + 设计自身声明的契约（分层、职责边界、可替换性、接口宽度） |
report_diff | 两份报告比对：新增/消失/变化的发现 |
怎么读报告
工具的产出是一份报告，结论只在 verdict 里：看 verdict，不看 ok。ok 在各族的含义不同——多数族在评审失败时仍是 true，组合族在出现 error 级发现时是 false——所以它不能当判定读；把它当判定读，会得出与报告相反的结论。
| 字段 | 说明 |
|---|
verdict | 判定：pass、pass_with_findings、fail |
verdictReason | 一句话说明为什么是这个判定 |
hashes | hashSpec 与 modelHash；前后回归另带 beforeModelHash、afterModelHash。同一份模型永远得到同一个哈希 |
nextSteps | 引擎建议的下一步 |
schema | 报告的版本化契约，例如 model-everything/verify/v1。要按字段分支，就分支在它上面 |
truncated | 搜索撞到上限就停了。截断不等于通过，是没结论；某个性质没判定出来时，报告里会出现 _UNDECIDED |
默认返回正文。要完整 JSON，传 reportView: "full"。
ok 为 false 时判定也是 fail，但含义不同：工具根本没跑。原因写在 errorCode 里——输入不合法、图族不支持，或声明的 intent 服务不了。这类拒绝的 verdictReason 以 the tool did not run: 开头。
报告怎么读，有一份成体系的说明：skills/model-everything-report-reading/ 讲阅读顺序（先看跑没跑、再看判了什么、最后看该做什么）、发现分别放在哪一层、以及两处最容易读反的地方。结构由一个从真实报告生成的思维导图给出：docs/report-reading/mindmap.mmd，tests/report-reading 会在图与引擎不一致时失败。
uml_render、uml_parse、uml_review 另收一个 intent，用来说明这份产物要做什么：给人看（present）、要被验证引擎读回（verify）、还是要证明渲染与模型一致（fidelity）。服务不了这个用途的视图会被直接拒绝，而不是勉强画出来。
示例
examples/ 里是可以直接跑的样本模型，配 examples/README.md 说明各自的看点和预期结果。它们是文档，不是测试夹具——各测试套件读自己的 tests/<套件>/fixtures/：
examples/order-state-machine.before.json 与 examples/order-state-machine.after.json：订单流程的前后两份模型，用来跑前后回归。examples/control-dispatcher.json：带预算与锁配对的分发状态机，预期零错误。examples/control-dispatcher.overbudget.json：同一个机器换上更慢的看门狗处理，预期报出一条 A12_BUDGET_OVER，并给出最短的超预算路径。examples/ecommerce-data-model.json，以及 examples/user-migration.before.json 与 examples/user-migration.after.json：数据模型，和迁移的前后两份。
model_verify model=examples/control-dispatcher.json
技能
技能按域拆分，讲的是怎么用、按什么判定：
| 技能 | 覆盖 |
|---|
model-everything | 入口：断言清单、核验纪律、深度分级、到各域技能的路由 |
model-everything-uml | UML 图：选哪种视图、标签约定、审查码、往返一致性检查的边界 |
model-everything-structure | 架构与依赖：矩阵怎么写、各条结构检查意味着什么 |
model-everything-datamodel | 数据模型与迁移：不变式（任何时刻都必须成立的约束）、迁移覆盖、回滚对称 |
model-everything-design | 设计自洽：分层是否成立、职责与依赖是否匹配、子类型能否替父类型、接口是否宽于调用方 |
model-everything-interleaving | 并发、同步与异步声明：哪些能证明、用哪个工具证明、哪些只有运行时能看见 |
model-everything-report-reading | 读报告：阅读顺序、发现放在哪一层、容易读反的两处 |
技能描述本身就是路由依据，而它们能写的长度有硬上限（目录行截断在 500 字符，之后的部分模型看不到）。谁负责哪个问题、每行必须携带什么，由一张生成的图记录：docs/routing-map.md，生成器是 docs/tools/generate-routing-map.mjs；tests/routing-map 会在图与目录不一致时失败。
安装（dsh）
本插件以 cordis bundle 形式提供，声明在仓库根 package.json 的 dsh.bundle 与 cordis.patch.yml。
# 从源码目录安装（开发中）
dsh plugin --profile <profile> add "file:$PWD"
# 从 npm 安装（发布版）
dsh plugin --profile <profile> add dsh-model-everything
# 未全局安装 dsh 时
npx -p @deepseek-ai/dsh dsh plugin --profile <profile> add dsh-model-everything
装完重启该 profile，dsh --profile <profile> --dump-config 里应能看到本插件的行。卸载同样走插件管理器，从目标 profile 移除。
技能走 DSH 标准的 filesystem skill provider 注册，工具挂在 ctx.tools 上。另有一条模型可见的状态目录条目，可查注册状态与引擎接受的 schema 版本。
两个组件
| 组件 | 行 id | 做什么 | 默认 |
|---|
dsh-model-everything | dsh-model-everything | 全部工具与技能 | 开 |
| 提示词注入增强 | dsh-model-everything-gate | 会话第一条模型步注入一条路由提示 | 开 |
提示词注入增强是第二个组件，单独开关。它补的是路由的短板：路由靠技能描述文字，而目录行截断在 500 字符；更要紧的是，一次会话如果压根没决定加载技能，就没有任何东西把它路由过去。
它在每个会话注入一条消息（约 3.2k 字符），内容四块：不确定该查哪个时先加载哪个技能、每个技能管什么、每个工具做什么以及它不证明什么、以及怎么读一份报告（verdict 而不是 ok，skip 不是 pass）。那条"先加载技能、别凭记忆回答"的规则在开头说一次、结尾换个说法再说一次——这是量出来的：只说一次时，那种"觉得自己会答"的请求（迁移）既没加载技能也没用工具；首尾各说一次之后它补上了，而对照任务没有被过度触发。
它的形状借了同一个 harness 里另一个插件往系统提示注入的那一节的三招（那套做法在本环境里已有先例）：
- 只广播装得上的东西：技能表按
skills/ 目录里真实存在的技能渲染，所以表里不会出现一个解析不到的技能名；新加技能若还没写行，会退回"see its catalog line"，可以不全，但不会指错。
- 选择表而不是一句话清单：
| 这个请求 | 这个技能 | 两列，路由本来就是在近义项之间排序，表格比散文更像一道选择。
- 反降级规则：工具拒绝时读
errorCode 改输入再试；工具没装就明说并退回通用方法——没有任何东西跑过的检查不是通过的检查。
它怎么工作，四句话：
- 注入点：
agent/pre-step，把消息追加到该会话第一个模型步的决策里，不是 session-start——后者落进 inbox，可能被空会话的 preset 切换清掉；
- 只注入一次：消息带自己的 producer source kind，每一步都按会话历史查一次，见到就不再注入；被清掉的话会在下一个能跑的步重新出现；
- 开关：
enabled 是 live 字段，插件页翻开关对运行中的 host 立刻生效；gateContent 不是 live（一千多字的散文不该进表单），要改写在 profile 的 cordis.patch.yml 里；extraGuidance 是留给部署自己加一句的追加槽；
- 它只路由：不检查任何东西，也不会让技能自己加载。
开关与默认：默认开。这个默认值是量出来的——它补上的是插件唯一接不住的那类请求，而对照任务没有被过度触发。代价是每个会话约 3.2k 字符；要关掉就改 cordis.patch.yml（见下）或翻插件页的开关。想做对照（同一个请求，关一次开一次）也用它。
gateContent 可以整段替换，用来试别的措辞；tests/gate 仍要求它点名每个已发布的技能。
配置
注入组件（默认开）有三个键：
| 键 | 类型 | 默认值 | 说明 |
|---|
enabled | boolean | true | 是否注入。live 字段：插件页翻开关对运行中的 host 立刻生效，不用重启。 |
gateContent | string | 内置文本 | 注入的全文。替换它等于自己写路由规则；tests/gate 仍会要求它点名每个已发布的技能。 |
extraGuidance | string | "" | 追加在消息最后的一段话，留给部署写自己的规则。 |
主行只有一个 interaction（提议调用工具时怎么处置，默认 follow-approval）；关掉主行是关掉那一行本身，不是改配置。
按 row id 写进 profile 的 cordis.patch.yml：
- insert:
- id: dsh-model-everything-gate
name: 'dsh-model-everything/gate'
config:
enabled: false # 关掉注入
边界
- 不拥有你的代码。 只读必要的文件，给出带出处的结论。结论对不对，以源码为准。
- 并发：一半路由，一半判定。
model_interleaving_scan 挖出声明并按 family 路由（线程→TSan/Helgrind/CBMC/TLA+，中断→RTOS 感知分析，异步→TLA+/UPPAAL 加运行时检查）。但共享位置不再只是路由：把 shared 与 accesses 交给 model_compose_verify，它会判定无序写（C4）与非原子更新/丢更新（C5）——那是一个能在模型上给出最短路见证的决定，不是某个检查的名字。源码级竞争、阻塞调用、漏 await 与锁是否跨整个操作持有，仍在路由的另一半。
- 图的审查不等于代码审查。 图与它声称的模型一致，只说明图画对了。代码是不是这样，还得对着源码核验。
环境要求
- 逐版本的安装 / 挂载 / 启动 / 卸载证据在 DSH-COMPATIBILITY.md。
- DeepSeek Harness：准入看
package.json 的 peerDependencies——插件管理器按它决定装不装得下，dsh.compatibility.dshReleases 只是记录实测结论。逐版本兼容性是实测项，没实测过的版本一律标 unknown。
- Node.js：
>=20。
- 无 Python 依赖，无网络调用。
权限与数据
- 运行时只读包内的
skills/ 目录（用于注册技能），不读凭据，也不联网。
- 工具只处理你传进来的模型、图与文件路径。报告里只有它算出的结论与哈希。
- 导出到外部检查器（UPPAAL / TLA+ / PRISM / SPIN）时只写你指定的文件。
故障排查
- 技能不可见：确认 DSH 版本支持
ctx.skills 与 Agent Skills 发现，并在安装后重启 profile。
- 工具不在：先查
enabled（可能是 false），再看插件管理器是否真的装上了（--dump-config 里有没有本插件的行）。
- 插件管理器拒绝安装：确认
@deepseek-ai/* 在 peerDependencies 里，而不是 dependencies。
- 某个图族被拒绝：这是设计行为。UML 2.5 的十四个图族在本构建里都有实现，所以拒绝永远是关于记号的：记号画不出这个视图，或画得出但读不回来。它按名拒绝并说明理由，不会交出错的模型。
开发
npm install
npm run typecheck # tsc --noEmit
npm run build # tsc → lib/（lib/ 必须与 src/ 同步提交）
npm run test:engine # 全部回归套件，含记忆门禁
npm run test:full # 端到端合并套件
npm run lint:md # markdownlint，与 CI 同一个版本
npm run bump -- <x.y.z> # 同步声明版本
npm run bump -- --check # 版本一致性
npm run bump -- --audit # 版本引用审计
外部检查器往返（tests/external/run.mjs）会调用真实的 spin 与 gcc 跑一遍导出结果。工具不在 PATH 上时整组自动跳过——跳过不算通过。要指向别处的可执行文件，用两个环境变量：
MODEL_EVERYTHING_SPIN=/path/to/spin MODEL_EVERYTHING_GCC=/path/to/gcc npm run test:engine
插件自己不调用 spin、gcc、UPPAAL、TLA+ 或 PRISM：model_export 只写出它们能读的输入。
约定、目录地图与硬约束见 AGENTS.md。项目记忆（调研结论、架构决定、交接）的入口在 .github/memory/MEMORY.md。
想参与：两种来件的结构不同——有出处的改进（要引用方法、点名改哪个码、说明是改判定还是加信号，并附最邻近反例与一条能红的变异）与运行中遇到的问题（要原样引用报告、给最小复现），分别见 CONTRIBUTING.md 与 .github/ISSUE_TEMPLATE/。
参考文献
各条检查背后的已发表工作——以及哪些检查没有已发表来源——收在 docs/references.md。每一条都从仓库里 Provenance 表逐字提取（生成器 docs/references/generate.mjs），并标注它在哪个文件里被引用。这份清单存在的意义是把「已发表方法」与「本仓库自己的约定」分开：多数检查是后者，而把约定当成引用写出来，比说明它是约定更糟。
许可证与安全
MIT，见 LICENSE。安全策略见 SECURITY.md。
