dsh-logicprobe

dsh plugin --profile web add dsh-logicprobe

逻辑探针 (Logic Probe)

<p align="center"><a href="README.en-US.md">English</a> · <strong>中文</strong></p>

<p align="center">

<a href="https://github.com/AmethystLuna/logicprobe/actions/workflows/dsh-bundle.yml"><img src="https://github.com/AmethystLuna/logicprobe/actions/workflows/dsh-bundle.yml/badge.svg" alt="CI"></a>

<a href="LICENSE"><img src="https://img.shields.io/badge/license-MIT-blue.svg" alt="License: MIT"></a>

<a href="https://nodejs.org/"><img src="https://img.shields.io/badge/node-%3E%3D20-blue.svg" alt="Node 20+"></a>

<a href="https://github.com/hashgraph-online/hol-guard"><img src="https://img.shields.io/badge/HOL%20Guard-passing-00a67e" alt="HOL Guard"></a>

<a href="https://afdian.com/a/amethystluna"><img src="https://img.shields.io/badge/%E7%88%B1%E5%8F%91%E7%94%B5-Afdian-946CE6" alt="在爱发电上赞助"></a>

</p>

状态：本插件核验设计、代码与计划中的声称。它继续以 dsh-model-everything

的形式发展，同样覆盖声称、行为、结构、UML、数据模型、并发、导出与报告对比，

并加上设计原则审查（分层、边界、可替换性、接口宽度、图形状）、报告阅读技能、

标签口径解释和可选的会话启动路由。它不是本插件的 API 镜像：UML 能力拆在多个

工具里，本插件只有一个 logicprobe_uml。它已发布为

dsh-model-everything

（npm）。现有安装继续可用。

0.2.2-rc.1 与 0.2.2-alpha.3 上已实测安装、挂载、启动、工具调用与卸载；逐版本证据见

[DSH-COMPATIBILITY.md](DSH-COMPATIBILITY.md)。

没验证过的设计，翻车只是时间问题；再复杂的代码，建模再跑就清楚了。

logicprobe 核验声称与实物是否一致。事实类对着源码查。行为类跑模型：状态机、协议、组合、数据模型、迁移。图按依赖图读，单层或多层。改动前后用基线对比。验不了的维度明说，并指出该用哪个工具。

跨平台：支持 Claude Code、Codex CLI、Cursor、Kimi CLI、OpenCode、ZCode。技能基于 Agent Skills 开放标准。

用例图与其它 UML 图族：本插件只建模状态机与流程。用例图（:Actor: --> (UseCase)）、类图、

组件图、部署图等会被按名拒绝，不会被误读成状态机。需要完整 14 类 UML 2.5 图族的

render/parse/review 时，用 dsh-model-everything：

它承接了本插件的全部图能力（记号语法引擎、能力矩阵、用例与结构族模块）。

功能

阶段 · 内容

Phase 1-2 · 枚举每个可验证声称：API 名、文件路径、枚举值、数量、机制可行性。逐条对照代码库给出证据。

Phase 2a · 对提取的状态机模型执行 8 项结构检查（S1-S8）：S1 可达性、S2 死锁、S3 活性、S4 确定性、S5 事件完备性、S6 守卫完备性、S7 不变量有效性、S8 单调变量。

Phase 2b · 14 项对抗探针（A1-A14）：意外事件、竞态交错、顺序置换、配对对称（lock/unlock，含 onEntry/onExit 隐式配对）、边界轰炸、资源注入、最小反例、幂等重放、必达、顺序、原子性、预算（A12 最坏路径代价，含正成本环检测）、概率可达（A13）、期限（A14）。

重构模式 · 对比前后模型：行为保持、不变量连续性、死锁回归、复杂度声称。

数据模型模式 · 验证 DataModelV1 数据模型（DS/DA/DD）：迁移覆盖、copy 一致性、before/after 破坏性变更回归。

UML 建模与审查 · 用 UML 画出代码流程，再审查这份建模本身：结构缺陷、文档缺口、图与模型的往返保真度。

并发风险挖掘 · 扫描文档与计划中的并发安全声称（thread-safe、lock-free、race condition、中断安全等），标记出来交给专用验证。

输出 · 结构化发现：精确 file:line 证据、严重性分级、修正方向。核查过程中绝不直接改代码。报告附带 coverageNotes，把时序、抢占、混合控制、概率等词汇路由到外部工具（UPPAAL、TSan、CBMC、TLA+、SpaceEx、PRISM 等），见 skills/logicprobe/references/gap-routing-guide.md。模型可携带自然语言 narrative（状态、事件、场景注释），报告原样回显。

模型永远先以转换表形式展示，经用户确认后才运行。模型提取错误是验证的头号失败模式。

工具与报告

下面两份清单（原生工具清单，以及怎么读它们的报告）与安装方式无关：dsh 走原生工具，Claude Code / Codex / Cursor / 终端 / CI 走同一套技能与 Python CLI 引擎（见「使用」）。

工具清单：

工具 · 作用

logicprobe_verify · 状态机验证：S1-S8 结构检查 + A1-A14 对抗探针。传 beforeModel 与 stateMapping 可加做 D1-D4 前后回归。

logicprobe_datamodel_verify · 数据模型验证：DataModelV1、迁移覆盖、copy 一致性、DD1-DD4 数据回归。

logicprobe_concurrency_scan · 扫描并发风险声称（thread-safe、lock-free、race condition、mutex 等），标注需要专用验证。

logicprobe_compose_verify · 两台及以上状态机组合验证（握手 rendezvous 语义）：C1 组合死锁、C2 握手永不触发。

logicprobe_export · 导出外部工具原生输入：UPPAAL（.xta + queries）、TLA+（TLC 模块）、PRISM（DTMC .pm + .pctl）、SPIN（Promela + ltl）。

logicprobe_uml · 用 UML 建模代码流程，并审查这份建模。见下方「UML 建模与审查」。

logicprobe_structure_verify · 把组件/包/类/部署图当依赖图审查（UML020-UML026）：孤立节点、悬空端点、依赖环、违反允许依赖矩阵的边、跨层反向依赖、矩阵要求却缺失的边；每条被判定的边都会报出命中的规则 id。它审的是图，代码侧要用 include/依赖扫描对账。

logicprobe_report_diff · 对比两份同族报告（baseline vs current），给出新增/消除/变化的发现与增量判定：按 检查 id + code + 机器可读定位（evidence/path） 匹配，改措辞只会算作 changed；新增 error 判 fail，而 currentVerdict 仍保留本次运行的绝对结论。"违规不增"的验收判据，算出来而不是看出来的。

迁移代价用 cost（缺省 1），配 budget 不变量即由 A12 检查最坏路径代价，正成本环会被判为无界。迁移权重用 weight（缺省 1），配 probability 不变量即由 A13 计算概率可达。状态上的 onEntry/onExit 动作由 A4 自动纳入配对检查，maxTicks 加 tickEvents 由 A14 检查期限。

怎么读报告（ok 不是结论）

所有报告都同时给「工具跑成功」与「审查通过」两件事：

字段 · 含义

schema · 版本化报告契约（logicprobe/verify/v1、logicprobe/uml/review/v1…），消费方按它分支而不是猜字段。

ok · 引擎产出了报告。对 verify 只在模型校验失败时为 false；它不是结论。

ran · 工具确实执行了。仅在工具层拒绝请求（带 errorCode/error）时为 false。

verdict · pass / pass_with_findings / fail。任何 severity: "error" 的发现、或校验失败，都会是 fail。

verdictReason · 一行说明，例如 1 error finding(s) (first: S2_NO_TRANSITIONS)。

hashSpec · modelHash 依据的已发布规范（见 [hash-spec.md](skills/logicprobe/references/hash-spec.md)）。

hashes · 本次报告涉及的全部哈希集中一处（模型哈希、图/矩阵哈希、前后模型哈希）。

metadataKeys · 输入里带 _ 前缀的注记键路径（仅当存在时出现）。

narrativeCoverage · {states: "5/5", events: "3/9", scenarios: "0/12"}：narrative 允许部分覆盖，这里报告还差多少；缺口同时是一条 NARRATIVE_PARTIAL（info）发现，门禁不必去解析 nextSteps 文本。

nextSteps · 由发现推导的下一步，永不为空，同一输入两次运行逐字一致。

只看 ok 会把「有死锁」的模型读成通过——判据是 verdict。非 DSH 的 Python CLI 退出码跟随 verdict：pass/pass_with_findings → 0，fail 或拒绝 → 2。

工具打印的是报告正文，不是 JSON。 结构化报告本身没有变（schema/verdict/hashes/检查项 id/code/evidence/path 都在），变的只是给模型看的那份文本：

• 通过的检查只出现在 CHECKS 清单行里，不再展开正文（通过的检查没有可行动内容）；
• 同一个事实被多个检查各报一遍时（例如 S5 与 A1 报同一批 (state, event) 对），只在先出现的检查里列出，后出现的检查写明「与上面重复」，不再重印；
• 同一检查内逐字相同的发现折叠成一行并标注 (xN)；
• 只有 error 级发现内联 evidence，warning 级不内联——那是机器字段，不是阅读材料。

需要结构化报告本体时传 reportView: "full"（例如要把它交给 logicprobe_report_diff，它按 check + code + evidence 匹配身份，正文替代不了对象）。非 dsh 宿主走 CLI，它直接打印报告 JSON：那份正文是 dsh 工具的呈现层。

模型自带的归档记录（_ 前缀键）

任何以 _ 开头的键（任意层级，如 _source、_verified、_extraction_caveats、states[0]._note）都是注记元数据：schema 跳过、modelHash 排除、报告以 metadataKeys 回显。这样来源与验证快照可以跟模型放在同一个文件里，不必再维护一个会漂移的 sidecar，而模型的哈希身份不变。其余键仍然闭合——拼错的 sttes 依旧报错。用 verify model.json --hash-check <hex> 可回答某个历史哈希是否属于任何已发布规范。

UML 建模与审查

…(truncated)