AmethystLuna/logicprobe

逻辑探针 (Logic Probe)

English · 中文

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

跨平台 — 支持 Claude Code、Codex CLI、Cursor、Kimi CLI、OpenCode、ZCode。基于 Agent Skills 开放标准构建。

功能

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

安装

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）：

• 技能遵循 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 验证链路。