# 逻辑探针 (Logic Probe)

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

文档不是事实——代码才是。一个声称核查技能：逐条核验设计文档、架构规格、重构计划中每一个可验证的声称与代码库实际是否一致；遇到行为类声称时升级为可执行模型验证。

**跨平台** — 支持 Claude Code、Codex CLI、Cursor、Kimi CLI、OpenCode、ZCode。基于 [Agent Skills](https://agentskills.io) 开放标准构建。

## 功能

| 阶段 | 内容 |
|------|------|
| 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，P(击中) 满足下界）、期限（A14，maxTicks + tickEvents） |
| 重构模式 | 前后模型对比——行为保持、不变量连续性、死锁回归、复杂度声称 |
| 数据模型模式 | DataModelV1 数据模型验证——DS/DA/DD 检查，迁移覆盖、copy 一致性、before/after 破坏性变更回归 |
| 并发风险挖掘 | 扫描文档/计划中的并发安全声称（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：

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

然后通过 CLI 安装：

```bash
claude plugin install logicprobe@logicprobe
```

### Claude Code 手动安装

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

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

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

## DeepSeek Harness (dsh)

原生 dsh 支持以 cordis 插件 bundle 的形式提供，位于**仓库根**（根 `package.json` 声明了 `dsh.bundle`）：

- 技能遵循 Agent Skills 开放标准，被 dsh 的 `skill-filesystem` provider 原样发现——零代码。
- bundle 将 claim 验证门禁（1% Rule / Red Flags / 主动建议）注入每个 agent 会话的第一个模型步骤——是 Claude `SessionStart` hook 在 dsh 的原生对应物，并注册模型可见目录条目（`cordis_inspect`）、原生工具 `logicprobe_verify`（`ctx.tools`）以及策略感知上下文 `logicprobe:mode`（`ctx.systemPrompt`）。
- `logicprobe_verify` 支持 `beforeModel` + `stateMapping` 的 BEFORE/AFTER 对比（D1-D4），可直接验证重构/迁移的行为保持、不变量连续性、回归增量和死锁/活性回归。
- `logicprobe_verify` 还支持：迁移/处理器代价 `cost`（缺省 1）与 `budget` 不变量（A12 最坏路径代价检查，含正成本环检测）、迁移权重 `weight` 与 `probability` 不变量（A13 概率可达）。
- 状态 `onEntry`/`onExit` 动作（A4 自动纳入配对检查）；`maxTicks`+`tickEvents` 期限（A14）；报告 `coverageNotes`（时序/抢占/混合/概率词汇 → UPPAAL/TSan/CBMC/TLA+/SpaceEx/PRISM 等外部工具路由）。
- 引擎共运行 **22 项检查（S1-S8 结构 + A1-A14 对抗）**；模型可带自然语言 `narrative`（状态/事件/场景注释），报告原样回显。
- `logicprobe_compose_verify`：两台及以上状态机组合验证（握手 rendezvous 语义），报 C1 组合死锁 / C2 握手永不触发。
- `logicprobe_export`：把 LogicModelV1 导出为外部工具原生输入——UPPAAL（XML `.xta` + queries）、TLA+（TLC 模块）、PRISM（DTMC `.pm` + `.pctl`）、SPIN（Promela + ltl）——与 `coverageNotes`/gap-routing 的维度对应；导出严格遵循各工具官方语法，生成文件可直接提交给对应检查器（SPIN 已做真实端到端验证）。
- `logicprobe_datamodel_verify` 新增数据模型验证：DataModelV1、迁移覆盖、copy 一致性、DD1-DD4 before/after 数据回归。
- `logicprobe_concurrency_scan` 扫描文档/计划中的并发风险声称（thread-safe、lock-free、race condition、mutex 等），标记需要专用并发验证。
- 与 embedded-workbench bundle 的 Plan Verification Gate 配合，在 dsh 中闭环了 claim 验证链路。

安装（原生 bundle，推荐）：

```bash
# 从 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`](.dsh/INSTALL.md)。

> DSH 安装注意：npm 包名为 `dsh-logicprobe`（无 scope）。在 web profile 的 `package.json` 中，依赖键与 `dsh.profile.bundles` 必须写 `dsh-logicprobe`；否则 dsh 加载器会因找不到 `node_modules/dsh-logicprobe` 而启动失败。

## 使用

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

- **设计文档 / 计划审查** — "Review this design document" → 声称枚举与代码库核查
- **行为类问题** — "could this state machine deadlock"、"is this retry limit safe"、"check this timing for bugs" → 主动建议（不自动加载）作为可选验证
- **重构计划** — 管线对比前后模型，标记计划未声明的行为变化
- **数据模型/迁移审查** — "is this migration non-breaking"、"does this copy cover all required fields" → 使用 `logicprobe-datamodel` 技能

技能在 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 输入——与 dsh 工具逐字节一致，见 tests/python/run.mjs）；模型仅为抽取出的状态表时，填充模板 `skills/logicprobe/references/verification-harness.py`；数据模型验证使用 `skills/logicprobe-datamodel/references/data-model-harness.py`；不可用（如离线开发机）时，对应 guide 提供手动验证模式。

示例模型见 [`examples/`](examples/README.md)：订单状态机 before/after、电商数据模型、User 字段迁移。

## Codex CLI

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

### Codex 安装

```bash
# 添加 marketplace
codex plugin marketplace add AmethystLuna/logicprobe

# 安装
codex plugin install logicprobe
```

或手动：

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

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

## Cursor

Cursor 2.5+ 内置插件支持。

### Cursor 安装

```bash
# 克隆到 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 安装

```bash
# 通过 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` 中添加：

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

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

## ZCode (Z.AI)

ZCode 3.0+ 遵循 Agent Skills 标准。无插件市场——手动复制技能到 `.zcode/skills/`：

```bash
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 — 已实测 mainline 2026-08-14（gate bundle 加载并注入会话成功）
- Python 3.6+ 可选（仅自动验证工具需要；手动兜底模式无需任何依赖）

## 配置

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

| 键 | 类型 | 默认值 | 说明 |
|---|---|---|---|
| `enabled` | boolean | `true` | 设为 `false` 可关闭首步 Gate 注入。 |
| `gateContent` | string | 内置 gate 文本 | 覆盖注入到首轮模型上下文中的文本。 |
| `interaction` | `ask` \| `auto` \| `follow-approval` | `follow-approval` | 模型确认策略；`follow-approval` 在会话 approval policy 为 `never` 时解析为 `auto`。 |

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

```yaml
- 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"`）。

## 开发

```bash
npm install
npm run typecheck
npm run build
```

测试链：

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

## 许可证与安全

本项目使用 MIT 许可证，见 [LICENSE](LICENSE)。

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

## 关联插件

| 插件 | 说明 |
|------|------|
| [embedded-workbench](https://github.com/AmethystLuna/embedded-workbench) | 嵌入式 C/C++ 工具箱，其 Plan Verification Gate 依赖本技能。本插件已从 embedded-workbench 拆分而来。 |

## 致谢

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