# rei-checker-mcp

**形式検証チェッカー MCP v0.3.0a1** — 一行を受け取り、真偽を返す。 それ以上でも それ以下でもない。

Three-valued verdict (`VALID` / `INVALID` / `UNDECIDED`). No LLM in the judgment path. Every UNDECIDED carries a reason code and lands in an append-only refutation ledger.

**License**: AGPL-3.0-or-later
**Spec**: [CHECKER_SPEC_v0.md](./docs/CHECKER_SPEC_v0.md) (JP, authoritative for intent) · [English translation](./docs/CHECKER_SPEC_v0_en.md) (RFC 2119 wording for implementors). Spec text is CC BY-NC-SA 4.0; implementation is AGPL-3.0-or-later.
**Design invariants**: [CLAUDE.md](./CLAUDE.md)

## 5 分で 動かす

Python 3.9+ が あれば 十分。 外部 dependency なし (stdlib only)。

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

期待出力:

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

判定不能な入力は 「判定できない」 を 返す (spec §1.2):

```bash
python -m rei_checker verify "some unknown thing"
```

```json
{
  "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"
}
```

exit code: `0` = decisive (VALID/INVALID), `2` = UNDECIDED。 shell script で 「判定できたか」 を 直接分岐可。

## Ledger 蓄積 と stats

すべての `verify` 呼び出しは `ledger.jsonl` に一行追記される (spec §4)。

```bash
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
```

```json
{
  "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` env var で 上書き可能。 default = カレントディレクトリの `ledger.jsonl`。

## MCP server として 使う

Claude Desktop に 登録:

```json
{
  "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.3.0a1 の 状態 (2026-08-24 STEP 1401)

- ✅ Schema (3 値 + reason code 7 種) 完全実装
- ✅ Mock backend (test 用 truth table + 全 reason code trigger)
- ✅ Ledger (append-only JSONL、 UTF-8、 malformed row skip)
- ✅ stats() aggregate (decision_rate + reason_breakdown)
- ✅ MCP stdio server (initialize + tools/list + tools/call)
- ✅ CLI (verify / stats / mcp / version subcommand)
- ✅ **LeanBackend Stage 1 wired** (v0.3、 lean_checker_repl.exe persistent JSON REPL、 warm ~1.5ms)
- ✅ **Timeout hard-kill** (v0.3、 background thread + Queue、 hanging Lean process kill on timeout)
- ✅ **D-FUMT₈ 内部 projection** (v0.3、 ledger 層のみ、 spec §1.3 preserve)
- ⚠ Lean 4 Stage 2 (real elaboration) は 未実装 (Stage 1 hardcoded truth table のみ、 次 v0.4 spike)

**「まず 使われる」 が 優先** (spec §1.3、 §6.6)。 Lean 4 Stage 2 (real Lean.Elab dispatch) 完成後、 LeanBackend 自体は 変更不要 (harness 側のみ upgrade)。 API surface は 変わらない。

### D-FUMT₈ ledger annotation (v0.3)

各 verify() 呼び出し で ledger row に `d_fumt8` field が 追加される (spec §1.3 保護、 verify() 応答 の API surface には **出さない**)。 mapping:

| verdict / reason_code | D-FUMT₈ | 根拠 |
|---|---|---|
| VALID | TRUE (⊤) | 証明済 |
| INVALID | FALSE (⊥) | 反証済 |
| UNDECIDED / TIMEOUT | NEITHER (〜) | chat-Claude 「便りが来ない」 |
| UNDECIDED / PARSE_FAILURE | ZERO (〇) | まだ問われていない |
| UNDECIDED / DEPTH_LIMIT | INFINITY (∞) | 上限 hit |
| UNDECIDED / (他 4 種) | NEITHER (〜) | 判定不能 |

集計 (opt-in):

```python
from rei_checker.stats import stats
result = stats(include_d_fumt8=True)
# result.d_fumt8_breakdown → {"TRUE": N, "FALSE": M, "NEITHER": K, ...}
```

`stats()` default (opt-in flag なし) は 従来 3-value output のみ = **spec §1.3 preserved**。

## 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。

## テスト

```bash
python -m unittest tests.test_all -v
```

Spec §7 に従い、 **UNDECIDED を 返すべき ケースの テスト を 優先** (全 reason_code 個別 test + VALID/INVALID happy path)。

## Rei stack との 関係 (混同回避)

本 repo は 意図的に 独立。 隣接 tool との 区別:

- **rei-verify** (PyPI 0.1.0a1) = 反証機械 4-value verdict、 refutation-first 主軸。 本 repo は 3-value verification-first で **設計哲学が 別**。
- **grounded-check** = LLM 出力の 引用 grounding check、 別 domain。
- **rei-preregister** = 予測 SHA256 seal、 事前登録 tool。
- **discovery-worker** = 反例 hunter、 別 layer。

統合は spec §5 「複数バックエンド対応 非目標」 に反するため 現時点 なし。

## 貢献 / 報告

spec §8 の 4 原則を 遵守してください:

1. 機能を 足すか 迷ったら、 足さない
2. 「たぶん 正しい」 を 返すか 迷ったら、 UNDECIDED を 返す
3. 理論を API に 出すか 迷ったら、 出さない
4. 急がず、 ゆっくりと

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