rei-checker-mcp

형식 검증 체커 MCP v0.1.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 Design invariants: CLAUDE.md

5분 만에 실행

Python 3.9+만 있으면 충분하다. 외부 dependency 없음 (stdlib only).

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"
}

exit code: 0 = decisive (VALID/INVALID), 2 = UNDECIDED. shell script에서 「판정되었는지」를 직접 분기할 수 있다.

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 env var로 덮어쓸 수 있다. default = 현재 디렉터리의 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의 상태 (honest scope, 2026-08-22 spike)

• ✅ Schema (3값 + reason code 6종) 완전 구현

• ✅ Mock backend (test용 truth table + 전체 reason code 트리거)

• ✅ 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)

• ⚠ Lean 4 backend는 stub (v0.2 후보, lean_backend/ 디렉터리에서 구현 예정)

• ⚠ Timeout enforcement는 soft (elapsed 모니터링, hard process kill은 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 / explain_difference)

• 제3층 harness (calibration / static (regular) / transfer)

구현 순서: 제1층 → 제3층② calibration harness → 제2층. 자세한 내용은 spec §9-13.

테스트

python -m unittest tests.test_all -v

Spec §7에 따라, UNDECIDED를 반환해야 하는 케이스의 테스트를 우선 (전체 reason_code 개별 test + VALID/INVALID happy path).

Rei stack과의 관계 (혼동 방지)

본 repo는 의도적으로 독립적이다. 인접 도구와의 구분:

• 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