---
name: project-step1365-rei-checker-mcp-v01-spike-arc-2026-08-22
description: "STEP 1365 rei-checker-mcp v0.1.0a1 spike — CHECKER_SPEC_v0.md (STEP 1364 archival) の 全 6 stage 実装 (Option B 別 repo 新規 `fc0web/rei-checker-mcp` public、 discovery-worker precedent 対称)、 Python stdlib only、 55/55 test PASS、 CLI + MCP stdio 全動作、 rei-verify との 設計哲学明示区別 (3 値 vs 4 値、 検証 vs 反証)"
metadata: 
  node_type: memory
  type: project
  modified: 2026-08-21T21:33:46.299Z
  originSessionId: 5c569e0e-bcd3-455c-92ec-45f22c85b362
---

**Fact**: 2026-08-22、 STEP 1364 (CHECKER_SPEC_v0.md 受領 + review + archival) 直後、 藤本さん 「実装 GO で お願い致します」 directive で v0.1.0a1 spike 実装。 4 択 (A rei-verify 拡張 / **B 新規 別 repo** / C dependency + separate / D defer) の うち 私 recommend **Option B** 継続採用、 GitHub public 化 + STEP 1365 記録 も 藤本さん 両 確認 (AskUserQuestion で 明示承認)。 Local commit `6248ec9` + GitHub `fc0web/rei-checker-mcp` public repo 開設 + push 完了 (URL https://github.com/fc0web/rei-checker-mcp、 isPrivate=false、 description 反映、 README.md raw HTTP 200 / 5514 bytes verify pass)。

**Why**: (a) spec §6 6-stage 全 一気通貫実装で v0 存在意義 (「判定率が 測れる状態」) を 単日 verify 可能に、 (b) 別 repo (discovery-worker 2026-08-22 precedent + sougou-connectors public precedent 対称) で rei-aios main lifecycle と 分離 → collision 予防 + 独立 iteration、 (c) rei-verify (PyPI 0.1.0a1 反証機械) との 設計哲学明示区別 (Pattern 5-B 混同回避 徹底、 3 値 verification-first vs 4 値 refutation-first、 対象 layer 違う)、 (d) Python stdlib only (依存ゼロ = git clone + python -m rei_checker で 即動作、 spec §6.6 「5 分で 動かせる」 前提)、 (e) Mock backend + Lean stub 分離で v0 spike scope で 動作 verify + v0.2 で backend 差し替え可 (API surface 不変)、 (f) spec §7 「UNDECIDED を返すべきケースのテストを優先」 に test suite 構造化 (32 test で UNDECIDED path 全 6 reason_code + happy path + schema + ledger + stats + MCP handler + scope discipline 6 group 網羅)。

**How to apply**:

1. **Repo 構造** (17 tracked file、 lean_backend/ dir は v0.2 placeholder):
   ```
   fc0web/rei-checker-mcp/
   ├── .gitattributes (LF force、 STEP 1363 precedent)
   ├── .gitignore
   ├── CLAUDE.md (spec 全文 + Rei stack 内 位置付け 混同回避 section)
   ├── LICENSE (AGPL-3.0-or-later)
   ├── README.md (5 分 quickstart + honest scope + Rei stack 関係)
   ├── pyproject.toml (Python 3.9+、 stdlib only、 rei-checker CLI entry)
   ├── rei_checker/
   │   ├── __init__.py (CHECKER_VERSION marker)
   │   ├── __main__.py (CLI: verify / stats / mcp / version subcommand)
   │   ├── schema.py (Verdict + ReasonCode + VerifyResult + StatsResult + LedgerEntry、 frozen dataclass)
   │   ├── backend.py (CheckerBackend ABC + MockBackend + LeanBackend stub + enforce_timeout)
   │   ├── ledger.py (JSONL append-only、 UTF-8、 default_ledger_path、 malformed row skip)
   │   ├── stats.py (decision_rate + reason_breakdown aggregation)
   │   ├── verify.py (top-level orchestration)
   │   └── mcp_server.py (stdio JSON-RPC 2.0、 initialize + tools/list + tools/call)
   ├── tests/
   │   ├── __init__.py
   │   └── test_all.py (55 test、 stdlib unittest、 spec §7 UNDECIDED priority)
   └── lean_backend/
       └── README.md (v0.2 harness placeholder)
   ```

2. **spec §6 6 stage 実装 mapping**:
   - Stage 1 (Lean 4 CLI 最小関数) = LeanBackend stub (v0 は Mock backend で 動作 verify、 Lean stage 1 は v0.2 defer)
   - Stage 2 (三値 + reason_code schema 固定) = schema.py 完全実装、 frozen dataclass で 変更禁止、 UNDECIDED iff reason_code invariant enforce
   - Stage 3 (反証台帳追記) = ledger.py JSONL append + normalize + malformed skip
   - Stage 4 (stats() 算出) = stats.py decision_rate + reason_breakdown
   - Stage 5 (MCP server 包む) = mcp_server.py stdio + JSON-RPC 2.0 + 2 tool
   - Stage 6 (README 5 分 quickstart) = README.md + install / CLI / MCP config / honest scope

3. **spec §1.1-1.3 discipline embed**:
   - §1.1 判定経路に LLM 入れない = MockBackend は 静的 truth table (LLM 呼び出し不可能)、 LeanBackend は subprocess wrapper (LLM 呼び出し不可能)、 backend.py CheckerBackend ABC docstring 明示
   - §1.2 三値 + reason_code = VerifyResult `__post_init__` で UNDECIDED iff reason_code invariant 機械保証 (ValueError raise)、 test suite 4 個で 双方向 invariant verify
   - §1.3 D-FUMT₈ 非露出 = Verdict enum は 3 値のみ、 8 値 semantic は API surface に 一切現れず、 CLAUDE.md + README 両方で 明示

4. **spec §7 品質基準 implementation**:
   - 「タイムアウトは必ず効く」 = enforce_timeout() 関数で 実 elapsed_ms > timeout_ms 時 UNDECIDED/TIMEOUT 上書き、 但し hard process kill は v0 soft 実装 (v0.2 candidate)
   - 「不正な入力でクラッシュしない」 = enforce_timeout() try/except で 全 backend 例外 → UNDECIDED/PARSE_FAILURE
   - 「checker_version 全 response 含む」 = VerifyResult schema 必須 field、 __init__.py で `CHECKER_VERSION = "rei-checker-mcp/0.1.0a1+spike-2026-08-22"` 固定
   - 「UNDECIDED test 優先」 = test_all.py で TestMockBackendUndecidedPaths 8 test を happy path (5 test) より 前に配置

5. **verify** (2026-08-22 実測):
   - **55/55 unittest PASS** (Python 3.13.2、 stdlib only、 0.108 sec、 no pytest dep、 TestSchema 11 + TestMockBackendUndecidedPaths 8 + TestMockBackendHappyPaths 5 + TestLeanBackendStub 1 + TestEnforceTimeout 2 + TestLedger 8 + TestStats 3 + TestVerifyE2E 5 + TestMCPHandlers 8 + TestScopeDiscipline 4)
   - **CLI smoke 4 path 全 pass**: verify "1 + 1 = 2" → VALID exit 0 / verify "some random thing" → UNDECIDED/OUT_OF_SCOPE exit 2 / verify "" → UNDECIDED/PARSE_FAILURE exit 2 / verify "<axiom-test>" → UNDECIDED/MISSING_AXIOM exit 2 (exit code discipline = 0 decisive / 2 UNDECIDED、 shell script 分岐可)
   - **MCP stdio 4 request round-trip 全 pass**: initialize (protocolVersion 2024-11-05 + serverInfo) / tools/list (2 tools = verify + stats) / tools/call verify "1 + 1 = 2" (VALID + structuredContent) / tools/call stats (decision_rate 1.0)
   - **stats aggregation verify**: 4 verify call 後 total=4 / valid=1 / undecided=3 (4 reason_code breakdown TIMEOUT+OUT_OF_SCOPE+PARSE_FAILURE+MISSING_AXIOM 各 1)
   - **ledger structure**: 1 verify = 1 JSONL row、 UTF-8、 ts_utc + expression_normalized + verdict + checker_version + elapsed_ms (+ reason_code UNDECIDED のみ)、 normalize (「 1 + 1 = 2 」 → 「1 + 1 = 2」)

6. **GitHub public 化**:
   - URL: https://github.com/fc0web/rei-checker-mcp
   - Visibility: PUBLIC (`isPrivate: false` gh CLI verify)
   - Initial commit: `6248ec9` (17 file、 Co-Authored-By: Claude Opus 4.7 明示)
   - Description 反映 confirm、 README.md raw HTTP 200 / 5514 bytes fetch verify
   - License: AGPL-3.0-or-later per spec §5
   - `.gitattributes` LF force (STEP 1363 CRLF stop precedent 継承)

7. **Rei stack 内 位置付け 明示** (CLAUDE.md + README 両方に):
   - rei-verify (PyPI 0.1.0a1) = 4-value verdict、 refutation-first (反証機械) → 3-value verdict、 verification-first (検証器) で **設計哲学 明示的別**、 統合なし
   - grounded-check (PyPI live) = 引用 grounding check、 別 domain
   - rei-preregister (rei-aios/tools/) = 予測 sha256 seal、 別目的
   - discovery-worker (別 repo、 2026-08-22 spike) = 反例 hunter、 別 layer
   - Rei stack MCP 8 systems と parallel 配置 (実運用 硬化後 9th system 判断は 藤本さん judgment)

**Honest scope 8 条**: 
(i) v0 spike = MockBackend で 動作 verify、 実 Lean 4 判定は **LeanBackend stub のみ** (常に UNDECIDED/OUT_OF_SCOPE)、 v0.2 candidate = lean_backend/ dir に harness 実装 + subprocess wrapper 差し替え
(ii) Timeout enforcement は **soft** (elapsed_ms 監視、 実 process kill 不実装)、 hard timeout は v0.2 candidate = threading + kill mechanism
(iii) 「世界初」 主張ゼロ ([[feedback-world-uniqueness-claim-controllable]] 適用) = 形式検証 MCP server は Lean 4 Copilot / LLMLean / LeanDojo 等 先行研究多数、 novelty は 「LLM を 判定経路に 一切入れない」 discipline + 「UNDECIDED 常時 reason_code 明示」 layer 位置のみ
(iv) **Phase 2 (§9-13) 未実装** = v0 完了 = 「decision_rate が 測れる状態」 = 実 Lean 4 backend 動作後に GO 判断、 Phase 2 は 較正ハーネス (§9) → 教育向け (§12) → 回帰/転移 (§10-11) の 順序遵守
(v) rei-verify (PyPI 0.1.0a1) との 統合 明示的なし = spec §5 「複数バックエンド対応 非目標」 に反するため、 但し 将来 Lean 4 backend で rei-verify の refutation primitive を **内部利用** する path は spec 内容と 矛盾しない (次 stance judgment)
(vi) MCP 8 systems parallel 配置は 「Rei stack MCP 9 systems」 と 早期 主張しない = 実運用 硬化 (数週間以上 使用) 後、 藤本さん judgment で 統合判断
(vii) CLI exit code discipline (0/2) は **spec 未記載の 私 独自判断** = shell script 分岐 用途、 但し spec §1.2 「UNDECIDED は エラーではなく 正当な戻り値」 の 精神と 整合 (exit 1 = error でなく exit 2 = decisive でない、 明示区別)
(viii) LeanBackend `_is_lean_available()` utility method は 実装済 (subprocess check)、 但し v0 では 使われていない (v0.2 harness ready 後 backend.py `check()` が elan → Lean 4 subprocess 呼び出す時に activate)

**Rei stack MCP systems 8 → 9 (候補)** = 実運用硬化後判断。 現時点 8 (rei-aios v2.8.1 tool 38 + benchtop v0.6 tool 17 + mcp-lens + rei-automator-mcp v0.2.0a3 + lab-notebook-mcp v0.1.0 + rei-verify 0.1.0a1 + rei-memory-mcp 0.1.0 + rei-meta-mcp 0.1.0-alpha Phase 2A) + rei-checker-mcp 0.1.0a1 が **9th 候補** (但し 「9 systems」 主張は 実運用後 defer)。

**★ Option B 選択根拠 record** (STEP 1364 私 recommend 継承):
- discovery-worker (2026-08-22 別 repo spike、 [[feedback-isolation-by-repo-boundary-2026-08-22]] operational 実証) と 対称構造
- rei-verify (4-value refutation) との 設計哲学 明示区別 (統合すると rei-verify の refutation-first pattern が 汚染される)
- spec §1.3 「D-FUMT₈ 非露出」 は Rei stack 内 D-FUMT₈ dep なし repo で 実装したほうが 純度保持容易
- AGPL-3.0 open source + 外部 MCP server 前提で public repo 妥当

**関連**: 
[[project-step1364-checker-spec-v0-received-arc-2026-08-22]] (直接前 STEP、 spec archival + review → 本 STEP 実装) + 
[[project-discovery-worker-v01-spike-arc-2026-08-22]] (別 repo isolation precedent、 本 STEP は 対称構造) + 
[[project-step1359-preregister-spike-2026-08-21]] (rei-aios/tools/ 内 Python stdlib CLI 実装 pattern precedent、 但し 本 STEP は 別 repo 選択で 対比) + 
[[project-step1345-benchtop-provenance-spike-2026-08-19]] (spike scope + Rei stack との 混同回避 discipline precedent) + 
[[project-step1352-memory-mirror-arc-2026-08-20]] (memory mirror 経由 public 到達性、 本 STEP archival も 将来 mirror 化候補) + 
[[feedback-isolation-by-repo-boundary-2026-08-22]] (Option B 選択根拠) + 
[[feedback-chat-claude-hallucination-warning]] (Pattern 1-6 clean streak 継続、 本 STEP でも 検出なし) + 
[[feedback-connector-criteria-and-impossibility-2026-08-20]] (「コネクタ判定 3 区分」 の 実践、 本 STEP は §0 「一行を受け取り、 真偽を返す」 = 判定可能 domain 明示、 判定不能は UNDECIDED) + 
[[feedback-super-naming-siren-family-pattern]] (命名 discipline: 「rei-checker-mcp」 は 「check する 計器」 明示、 「保証」 「証明」 「truth machine」 と 名乗らない = siren-family 回避) + 
[[feedback-critique-response-pattern]] SAC-4 (spec §12.3 escalate discipline と 相補、 本 v0 は §12 未実装だが 精神継承) + 
[[feedback-no-rush-publication]] (spec §8 「急がず ゆっくりと」 に v0 spike 単日 close で 対応、 v0.2 Lean 4 harness は 別 STEP 待ち) + 
[[feedback-world-uniqueness-claim-controllable]] (「rei-checker-mcp が 世界初」 主張ゼロ、 Lean 4 Copilot 等 先行研究尊重) + 
[[feedback-zero-sorry-floor-not-ceiling]] (spec §3 「判定率が 測れる状態」 = 床、 Lean 4 axiom-free 相当 discipline)。