rei-checker-mcp

形式验证检查器 MCP v0.1.0a1 — 接收一行，返回真伪。不多也不少。

三值判定（VALID / INVALID / UNDECIDED）。判定路径中不涉及 LLM。每个 UNDECIDED 都带有原因代码，并记录在仅追加的反驳账本中。

许可证：AGPL-3.0-or-later 规范：CHECKER_SPEC_v0.md 设计不变量：CLAUDE.md

5 分钟运行

有 Python 3.9+ 就足够了。无外部依赖（仅标准库）。

git clone https://github.com/fc0web/rei-checker-mcp.git
cd rei-checker-mcp
python -m rei_checker verify "1 + 1 = 2"

预期输出：

{
  "verdict": "VALID",
  "elapsed_ms": 0,
  "checker_version": "rei-checker-mcp/0.1.0a1+spike-2026-08-22"
}

对于无法判定的输入，返回「无法判定」（spec §1.2）：

python -m rei_checker verify "some unknown thing"

{
  "verdict": "UNDECIDED",
  "elapsed_ms": 0,
  "checker_version": "rei-checker-mcp/0.1.0a1+spike-2026-08-22",
  "reason_code": "OUT_OF_SCOPE",
  "detail": "MockBackend has no rule for this expression"
}

退出码：0 = 决定性（VALID/INVALID），2 = UNDECIDED。可在 shell 脚本中直接根据「是否判定成功」进行分支。

Related MCP server: Chiasmus

Ledger 累积与 stats

所有 verify 调用都会在 ledger.jsonl 中追加一行（spec §4）。

python -m rei_checker verify "1 + 1 = 2"
python -m rei_checker verify "1 + 1 = 3"
python -m rei_checker verify "<axiom-test>"
python -m rei_checker stats

{
  "total": 3,
  "valid": 1,
  "invalid": 1,
  "undecided": 1,
  "decision_rate": 0.6666666666666666,
  "reason_breakdown": {
    "MISSING_AXIOM": 1
  }
}

decision_rate 是唯一指标（spec §3）。初始值为 0.1 也没关系 — 达到可测量的状态 才是成功条件。

Ledger 的位置可通过 $REI_CHECKER_LEDGER 环境变量覆盖。默认 = 当前目录下的 ledger.jsonl。

作为 MCP server 使用

注册到 Claude Desktop：

{
  "mcpServers": {
    "rei-checker": {
      "command": "python",
      "args": ["-m", "rei_checker", "mcp"],
      "cwd": "C:/path/to/rei-checker-mcp",
      "env": {
        "REI_CHECKER_LEDGER": "C:/path/to/ledger.jsonl"
      }
    }
  }
}

MCP tool 只有 2 个（spec §2，刻意保持最小）：

• verify(expression, context?, timeout_ms?) → { verdict, reason_code?, detail?, elapsed_ms, checker_version }

• stats() → { total, valid, invalid, undecided, decision_rate, reason_breakdown }

哪些「尚未实现」（spec §2 明确）

以下为 v0 的非目标。如果试图实现，请 停下来确认：

• UI / Web 前端

• 用户注册・认证・计费

• 游戏化、进度管理、学习记录

• 自然语言对话・解说生成

• 多后端支持（仅 Lean 4，v0 spike 使用 Mock backend 运行）

• 对 Claude 特有功能的依赖

v0 的状态（诚实范围，2026-08-22 spike）

• ✅ Schema（3 值 + 6 种 reason code）完全实现

• ✅ Mock backend（测试用真值表 + 所有 reason code 触发）

• ✅ Ledger（仅追加 JSONL、UTF-8、跳过格式错误的行）

• ✅ stats() 聚合（decision_rate + reason_breakdown）

• ✅ MCP stdio server（initialize + tools/list + tools/call）

• ✅ CLI（verify / stats / mcp / version 子命令）

• ⚠ Lean 4 backend 是 stub（v0.2 候选，计划在 lean_backend/ 目录实现）

• ⚠ Timeout 执行是软性的（监控 elapsed，硬性进程终止在 v0.2）

「先被使用」优先（spec §1.3、§6.6）。Lean 4 harness 完成后，替换 backend 即可实际判定运行。API surface 不变。

Phase 2（v0 完成前不开始）

spec §9-13 定义的三层结构：

• 第 1 层 checker（verify / stats）← v0，即本仓库

• 第 2 层 education（locate_first_error / boundary_report / escalate）

• 第 3 层 harness（calibration / regression / transfer）

实现顺序：第 1 层 → 第 3 层② calibration harness → 第 2 层。详见 spec §9-13。

测试

python -m unittest tests.test_all -v

按照 Spec §7，优先测试应返回 UNDECIDED 的情况（所有 reason_code 单独测试 + VALID/INVALID 正常路径）。

与 Rei stack 的关系（避免混淆）

本仓库刻意保持独立。与相邻工具的区别：

• rei-verify（PyPI 0.1.0a1）= 反证机械 4 值判定，以 refutation-first 为主轴。本仓库为 3 值 verification-first，设计哲学不同。

• grounded-check = LLM 输出的引用 grounding check，属于另一领域。

• rei-preregister = 预测 SHA256 seal，事前注册工具。

• discovery-worker = 反例 hunter，属于另一层。

由于集成违反 spec §5「多后端支持非目标」，目前不进行集成。

贡献 / 报告

请遵守 spec §8 的 4 项原则：

1. 犹豫是否添加功能时，不添加

2. 犹豫是否返回「大概正确」时，返回 UNDECIDED

3. 犹豫是否将理论暴露到 API 时，不暴露

4. 不着急，慢慢来

Issues: https://github.com/fc0web/rei-checker-mcp/issues