본문으로 건너뛰기
A

logicprobe

amethystluna/logicprobe

설계 문서와 계획을 코드베이스 사실과 대조하는 주장 검증 스킬. 행위 관련 주장은 상태 머신과 데이터 모델을 위한 실행 가능한 로직 프리미티브 검증으로 에스컬레이션하며, 전후 회귀, 도메인 제약, 동시성 리스크 마이닝을 제공합니다.

설치

dsh plugin --profile web add github:amethystluna/logicprobe

README

逻辑探针 (Logic Probe)

English · 中文

文档不是事实，代码才是。本技能逐条核验设计文档、架构规格与重构计划里的可验证声称，再把每一条对照到代码库的真实实现。遇到行为类声称时，它升级为可执行模型验证。

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

功能

阶段内容
Phase 1-2枚举每个可验证声称：API 名、文件路径、枚举值、数量、机制可行性。逐条对照代码库给出证据。
Phase 2a对提取的状态机模型执行 8 项结构检查（S1-S8）：S1 可达性、S2 死锁、S3 活性、S4 确定性、S5 事件完备性、S6 守卫完备性、S7 不变量有效性、S8 单调变量。
Phase 2b14 项对抗探针（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（状态、事件、场景注释），报告原样回显。

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

安装

Claude Code 安装（推荐）

在 Claude Code 的 ~/.claude/settings.json 中添加 marketplace：

{
  "extraKnownMarketplaces": {
    "logicprobe": {
      "source": { "source": "github", "repo": "AmethystLuna/logicprobe" }
    }
  }
}

然后通过 CLI 安装：

claude plugin install logicprobe@logicprobe

Claude Code 手动安装

git clone https://github.com/AmethystLuna/logicprobe.git ~/.claude/plugins/dev/logicprobe

然后在 ~/.claude/settings.json 中启用：

{
  "enabledPlugins": {
    "logicprobe@dev": true
  }
}

DeepSeek Harness (dsh)

原生 dsh 支持以 cordis 插件 bundle 的形式提供，位于仓库根，由根 package.json 的 dsh.bundle 声明。

这个 bundle 做三件事：

  1. 注册技能。 技能遵循 Agent Skills 开放标准，由 dsh 的 skill-filesystem provider 原样发现，不需要额外代码。
  2. 注入门禁文本。 每个会话的第一个模型步骤会收到 claim 验证门禁（1% Rule / Red Flags / 主动建议）。这是 Claude SessionStart hook 在 dsh 上的对应物。
  3. 注册原生工具与上下文。 工具挂在 ctx.tools 上，另有一条策略感知上下文 logicprobe:mode（ctx.systemPrompt），以及模型可见目录条目（cordis_inspect）。

工具清单：

工具作用
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 建模与审查」。

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

安装（原生 bundle，推荐）：

# 从 npm 安装（包名 dsh-logicprobe）
dsh plugin --profile web add dsh-logicprobe
# 或从 GitHub 源码安装
dsh plugin --profile web add "github:AmethystLuna/logicprobe"
# 未全局安装 dsh 时可用 npx
npx -p @deepseek-ai/dsh dsh plugin --profile web add dsh-logicprobe

装完重启 profile。运行 dsh --profile web --dump-config 应看到 id: logicprobe 且 enabled: true。更多方式（纯技能拷贝、项目级等）见 .dsh/INSTALL.md。

pnpm 11 有一个发布年龄闸门。它挡住发布不满一天的新版本（minimumReleaseAge，默认 1440 分钟），而且默认是非严格模式，所以裸名安装会静默装到上一个版本，profile 看起来像这次发版没发生。发版后约 24 小时内要装最新版，请带上版本号：

dsh plugin --profile web add dsh-logicprobe@<version>

pnpm 会把该版本写进 profile 的 pnpm-workspace.yaml 的 minimumReleaseAgeExclude 条目。那是它官方的豁免方式。

注意包名。npm 包名是 dsh-logicprobe，没有 scope。在 web profile 的 package.json 中，依赖键与 dsh.profile.bundles 必须都写 dsh-logicprobe。写错时 dsh 加载器找不到 node_modules/dsh-logicprobe，启动会失败。

UML 建模与审查

logicprobe_uml 把一份 LogicModelV1 画成 UML，也可以把手绘的 UML 读回模型，还可以审查建模本身。它有 3 个动作：

  • render：模型 → 图。Mermaid 支持状态图、活动流程图、时序图；PlantUML 支持状态图与时序图。notation 表达不了的构造会变成 warning，不会被悄悄丢掉。PlantUML 活动图直接拒绝，因为它的语法无法忠实承载带合流或环的图。
  • parse：图 → 模型。支持 Mermaid 与 PlantUML 的状态图、活动图，因此手绘的图也能送进 logicprobe_verify 验证。时序图是迹而不是机，解析会被拒绝。
  • review：审查建模。它报告两类问题。结构缺陷包括不可达状态、死端、歧义分支、无出口自环、重复迁移。文档缺口包括缺 narrative、变量无界、状态无可读标注、图与 narrative 标签漂移。它还会做保真度检查：把图重新解析回模型，任何结构性差异都报出来。

保真度是这套功能的核心。生成的图带有 logicprobe: 注释指令（init、终态、别名、变量类型），Mermaid 与 PlantUML 会忽略它们，而解析器会读取它们。因此「图 ↔ 模型」的比较是精确的。

审查只覆盖建模，不覆盖行为。每条发现都会指明应该跑哪一项引擎检查。完整清单（UML001-UML019）、指令格式、示例与各视图局限见 skills/logicprobe/references/uml-modeling-guide.md。

使用

插件在会话首个模型步骤自动注入能力通知。任务匹配技能的 Use when 描述时技能生效：

  • 设计文档 / 计划审查 — "Review this design document" → 声称枚举与代码库核查
  • 行为类问题 — "could this state machine deadlock"、"is this retry limit safe" → 主动建议（不自动加载）作为可选验证
  • 重构计划 — 对比前后模型，标记计划未声明的行为变化
  • 数据模型 / 迁移审查 — "is this migration non-breaking" → 使用 logicprobe-datamodel 技能
  • 代码流程建模 — "把这个状态机画出来"、"这份 UML 图对吗" → 用 logicprobe_uml 出图并审查建模，随后仍用 logicprobe_verify 验证行为

技能在 Phase 0 依据计划特征自动分级（LIGHTWEIGHT / STANDARD / ESCALATED），并在计划文件追加 ## Plan Verification 摘要块作为审计痕迹。

Python 可选。已有 LogicModelV1 JSON 时，可直接运行独立引擎 skills/logicprobe/references/logicprobe-engine.py：

  • verify 跑 S1-S8 / A1-A14 / D1-D4
  • compose 跑 C1 / C2 组合
  • export 生成 UPPAAL、TLA+、PRISM、SPIN 输入
  • uml-render、uml-parse、uml-review 覆盖 UML 前端

它与 dsh 工具逐字节一致，对照见 tests/python/run.mjs。模型只有抽取出的状态表时，填充模板 skills/logicprobe/references/verification-harness.py。数据模型验证使用 skills/logicprobe-datamodel/references/data-model-harness.py。Python 不可用（例如离线开发机）时，对应 guide 提供手动验证模式。

示例模型见 examples/：订单状态机 before/after、电商数据模型、User 字段迁移。

Codex CLI

本插件同样支持 OpenAI Codex CLI。技能遵循 Agent Skills 标准，两个平台行为一致。

Codex 安装

# 添加 marketplace
codex plugin marketplace add AmethystLuna/logicprobe

# 安装
codex plugin install logicprobe

或手动：

git clone https://github.com/AmethystLuna/logicprobe.git ~/.codex/plugins/logicprobe

技能通过 $logicprobe 调用，或由 Codex 根据任务上下文自动选择。

Cursor

Cursor 2.5+ 内置插件支持。

Cursor 安装

# 克隆到 Cursor 插件目录
git clone https://github.com/AmethystLuna/logicprobe.git ~/.cursor/plugins/logicprobe

或通过 Cursor 插件市场 UI 安装：/add-plugin AmethystLuna/logicprobe

Kimi CLI

Kimi CLI 自动从 .claude/skills/ 路径发现技能。.kimi-plugin/plugin.json 清单向 Kimi 插件管理器注册本插件。

Kimi 安装

# 通过 Kimi 插件管理器
/plugins install https://github.com/AmethystLuna/logicprobe.git

# 或手动克隆
git clone https://github.com/AmethystLuna/logicprobe.git ~/.kimi/plugins/logicprobe

技能通过 /skill:logicprobe 调用。

OpenCode

技能自动从 .claude/skills/ 和 .codex/skills/ 路径发现。在 opencode.json 中添加：

{
  "plugin": ["logicprobe@git+https://github.com/AmethystLuna/logicprobe.git"]
}

或通过 skop 安装（消费 Claude marketplace 清单）。详见 .opencode/INSTALL.md。

ZCode (Z.AI)

ZCode 3.0+ 遵循 Agent Skills 标准。它没有插件市场，手动把技能复制过去：

git clone https://github.com/AmethystLuna/logicprobe.git
cp -r logicprobe/skills/* .zcode/skills/

技能通过 $logicprobe 调用。详见 .zcode/INSTALL.md。

环境要求

  • 宿主：Claude Code v2.1+ / Codex CLI 最新 / Cursor 2.5+ / Kimi CLI 最新 / OpenCode 最新 / ZCode 3.0+
  • DeepSeek Harness (dsh)：dev preview，声明支持 >= 0.1.0-rc.7。最新一轮在 0.2.1-alpha.1 上实测了安装、挂载、启动与卸载；更早一轮实测覆盖 0.1.5-rc.2 到 0.2.0-rc.2。逐版本证据见 DSH-COMPATIBILITY.md。
  • Web 端的「Gate 注入」开关需要 dsh ≥ 0.1.7-alpha.1，因为设置服务必须能投影即时字段。更早的 dsh 上插件照常加载、照常注入，只是开关不出现，也不报错。
  • Python 3.6+ 可选，仅自动验证工具需要。手动兜底模式不需要任何依赖。

配置

在 DeepSeek Harness 中，bundle 支持以下配置：

键类型默认值说明
enabledbooleantrue设为 false 可关闭首步 Gate 注入。
gateContentstring内置 gate 文本覆盖注入到首轮模型上下文中的文本。
interactionask | auto | follow-approvalfollow-approval模型确认策略。follow-approval 在会话 approval policy 为 never 时解析为 auto。

在 dsh Web GUI 里可以直接改这个开关：侧边栏 插件 → 本插件卡片 → 「Gate 注入」。它实时生效，不必重启 profile。它只管注入的那段文本：关掉后 skills 与验证工具照常注册。同一张卡片上还有一个更粗粒度的行开关，关掉它会整行卸载插件，技能、工具和这个开关一起消失。要持久化覆盖，仍按下面的 profile patch 写。

在 profile 的 cordis.patch.yml 中按 row id 覆盖：

- insert:
    - id: logicprobe
      name: 'dsh-logicprobe'
      config:
        enabled: true
        interaction: follow-approval
        gateContent: |
          ...

卸载

  • 通过 DSH 插件管理器安装的，用同一管理器从目标 profile 中移除 logicprobe。
  • 手动复制过 skills/* 的，删除 ~/.agents/skills/ 或项目 .dsh/skills/ 下的对应目录。
  • 通过 cordis.patch.yml 添加的，删除 profile patch 中 id: logicprobe 的行，并重启 DSH。

权限与数据

  • 插件运行时只读取包内自带的 skills/ 目录，用于通过 DSH 标准 filesystem skill provider 注册技能。
  • 它会在会话首轮向模型上下文注入配置好的 gate 文本。
  • 它不读取凭据，不发起网络连接，也不访问 DSH 会话上下文之外的用户数据。
  • 实际使用技能时，模型会像使用其他编码技能一样，按用户指示读取项目文件。

故障排查

  • 技能在 DSH 中不可见：确认 DSH 版本支持 ctx.skills 与 Agent Skills 发现，并在安装后重启 profile。
  • Gate 未注入：检查 enabled 是否为 false，以及 profile patch 中是否存在 id: logicprobe 的行。
  • 插件管理器拒绝安装：确认 @deepseek-ai/* 包声明在 peerDependencies 中，而不是 dependencies。
  • 手动复制后 DSH 仍看不到技能：改用原生 bundle 安装（dsh plugin add "github:AmethystLuna/logicprobe"）。

开发

npm install
npm run typecheck
npm run build

测试链：

命令内容
npm run test:engine状态机与数据模型引擎回归（tests/engine、tests/data-engine、tests/concurrency、tests/uml、tests/apply-smoke、tests/dsh-client-half、tests/exporters、tests/external），再加 Python 逐字节一致性对照。对照脚本是 tests/python/run.mjs，它把同一批 fixture 在 TS 引擎与 skills/logicprobe/references/logicprobe-engine.py 之间比对报告、组合与导出产物。无 Python 时自动 SKIP。
npm run test:fulltests/full-suite.mjs 端到端合并套件
npm run test:python仅 Python parity（构建 + tests/python/run.mjs）
bash tests/skill-triggering/run-all.sh触发测试，位于 tests/skill-triggering/

许可证与安全

本项目使用 MIT 许可证，见 LICENSE。

如发现安全漏洞，请不要公开创建 issue，应使用 GitHub Security Advisory 或 SECURITY.md 中的联系方式私下报告。

关联插件

插件说明
embedded-workbench嵌入式 C/C++ 工具箱，其 Plan Verification Gate 依赖本技能。本插件由 embedded-workbench 拆分而来。

致谢

声称核查方法论（逻辑原语、对抗探测、重构前后对比）与触发测试框架（tests/skill-triggering/）遵循 Superpowers（Jesse Vincent，MIT License）的约定，经 embedded-workbench 插件改编而来。

관련 플러그인

W

auto-claude-code-research-in-sleep

wanshuiyin/auto-claude-code-research-in-sleep

15k2개월 전스킬MIT
T

archify

tt-a1i/archify

12.5k2개월 전스킬MIT
Z

dsh-web (dsh-skill-explorer)

zhu1090093659/dsh-web

8.4k3일 전스킬Apache-2.0
Z

dsh-web-ui (dsh-skill-explorer)

zhu1090093659/dsh-web-ui

6.3k지난달스킬Apache-2.0