rei-checker-mcp

Formal verification checker MCP v0.1.0a1 — Takes one line, returns true/false. Nothing more, nothing less.

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

Run in 5 minutes

Python 3.9+ is all you need. No external dependencies (stdlib only).

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

Expected output:

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

Inputs that cannot be decided return "cannot decide" (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. You can branch directly in shell scripts on whether a decision was reached.

Related MCP server: rei-verify

Ledger accumulation and stats

Every verify call appends one line to 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 is the only metric (spec §3). An initial value of 0.1 is fine — being in a measurable state is the success condition.

The ledger location can be overridden with the $REI_CHECKER_LEDGER env var. Default = ledger.jsonl in the current directory.

Using as an MCP server

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

There are only 2 MCP tools (spec §2, intentionally minimal):

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

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

What is "not built" (explicit in spec §2)

The following are non-goals for v0. If you're tempted to implement any of them, stop and confirm first:

• UI / web frontend

• User registration, authentication, billing

• Gamification, progress tracking, learning history

• Natural language dialogue / explanation generation

• Multi-backend support (Lean 4 only; v0 spike runs on Mock backend)

• Dependence on Claude-specific features

v0 status (honest scope, 2026-08-22 spike)

• ✅ Schema (3 values + 6 reason codes) fully implemented

• ✅ Mock backend (truth table for tests + all reason code triggers)

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

• ⚠ Lean 4 backend is a stub (v0.2 candidate, planned for lean_backend/ dir)

• ⚠ Timeout enforcement is soft (elapsed monitoring; hard process kill in v0.2)

"Being used first" is the priority (spec §1.3, §6.6). Once the Lean 4 harness is complete, swapping in the backend enables real verification. The API surface does not change.

Phase 2 (do not start until v0 is complete)

Three-layer structure defined in spec §9-13:

• Layer 1 checker (verify / stats) ← v0, this

• Layer 2 education (locate_first_error / boundary_report / escalate)

• Layer 3 harness (calibration / regression / transfer)

Implementation order: Layer 1 → Layer 3② calibration harness → Layer 2. Details in spec §9-13.

Testing

python -m unittest tests.test_all -v

Per spec §7, prioritize tests for cases that should return UNDECIDED (individual tests for all reason_codes + VALID/INVALID happy paths).

Relationship to the Rei stack (avoiding confusion)

This repo is intentionally independent. Distinctions from adjacent tools:

• rei-verify (PyPI 0.1.0a1) = refutation machine, 4-value verdict, refutation-first focus. This repo is 3-value verification-first — different design philosophy.

• grounded-check = citation grounding check for LLM output, different domain.

• rei-preregister = predictive SHA256 seal, pre-registration tool.

• discovery-worker = counterexample hunter, different layer.

No integration at this time, as it would violate spec §5 "multi-backend support is a non-goal".

Contributing / Reporting

Please follow the 4 principles of spec §8:

1. If you're unsure whether to add a feature, don't add it

2. If you're unsure whether to return "probably correct", return UNDECIDED

3. If you're unsure whether to expose theory in the API, don't

4. Don't rush; go slowly

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