rei-checker-mcp

Formaler Verifikations-Checker MCP v0.1.0a1 — Nimmt eine Zeile entgegen, gibt wahr/falsch zurück. Nicht mehr und nicht weniger.

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

In 5 Minuten zum Laufen

Python 3.9+ genügt. Keine externen Abhängigkeiten (nur stdlib).

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

Erwartete Ausgabe:

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

Bei unentscheidbarer Eingabe wird „nicht entscheidbar" zurückgegeben (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 = entscheidend (VALID/INVALID), 2 = UNDECIDED. In Shell-Skripten kann direkt darauf verzweigt werden, ob eine Entscheidung möglich war.

Related MCP server: Chiasmus

Ledger-Akkumulation und Stats

Jeder verify-Aufruf wird als eine Zeile an ledger.jsonl angehängt (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 ist die einzige Kennzahl (Spec §3). Ein Anfangswert von 0,1 ist in Ordnung — messbar zu werden ist die Erfolgsbedingung.

Der Speicherort des Ledgers kann über die Umgebungsvariable $REI_CHECKER_LEDGER überschrieben werden. Standard = ledger.jsonl im aktuellen Verzeichnis.

Als MCP-Server verwenden

In Claude Desktop registrieren:

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

Es gibt nur zwei MCP-Tools (Spec §2, bewusst minimal):

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

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

Was „nicht gebaut" ist (Spec §2, explizit)

Folgendes sind Nicht-Ziele von v0. Wenn du versuchst, es zu implementieren, halte inne und prüfe:

• UI / Web-Frontend

• Benutzerregistrierung, Authentifizierung, Abrechnung

• Gamification, Fortschrittsverwaltung, Lernverlauf

• Dialog- und Erklärungsgenerierung in natürlicher Sprache

• Unterstützung mehrerer Backends (nur Lean 4; der v0-Spike läuft mit Mock-Backend)

• Abhängigkeit von Claude-spezifischen Funktionen

Status von v0 (ehrlicher Umfang, Spike vom 2026-08-22)

• ✅ Schema (3 Werte + 6 Reason-Codes) vollständig implementiert

• ✅ Mock-Backend (Wahrheitstabelle für Tests + alle Reason-Code-Trigger)

• ✅ Ledger (append-only JSONL, UTF-8, Überspringen fehlerhafter Zeilen)

• ✅ stats()-Aggregat (decision_rate + reason_breakdown)

• ✅ MCP-stdio-Server (initialize + tools/list + tools/call)

• ✅ CLI (Unterbefehle verify / stats / mcp / version)

• ⚠ Lean-4-Backend ist ein Stub (Kandidat für v0.2, Implementierung in lean_backend/ geplant)

• ⚠ Timeout-Durchsetzung ist soft (Überwachung der verstrichenen Zeit; harter Prozess-Kill in v0.2)

„Zuerst genutzt werden" hat Priorität (Spec §1.3, §6.6). Nach Fertigstellung des Lean-4-Harness kann das Backend ausgetauscht werden und die echte Verifikation läuft. Die API-Oberfläche ändert sich nicht.

Phase 2 (nicht beginnen, bis v0 abgeschlossen ist)

Die in Spec §9–13 definierte dreischichtige Struktur:

• Schicht 1: Checker (verify / stats) ← v0, das hier

• Schicht 2: Education (locate_first_error / boundary_report / escalate)

• Schicht 3: Harness (calibration / regression / transfer)

Implementierungsreihenfolge: Schicht 1 → Schicht 3② Calibration-Harness → Schicht 2. Details in Spec §9–13.

Tests

python -m unittest tests.test_all -v

Gemäß Spec §7 haben Tests für Fälle, die UNDECIDED zurückgeben sollen, Priorität (einzelne Tests für alle reason_codes + Happy Path für VALID/INVALID).

Beziehung zum Rei-Stack (Vermeidung von Verwechslungen)

Dieses Repo ist bewusst unabhängig. Abgrenzung zu benachbarten Tools:

• rei-verify (PyPI 0.1.0a1) = Widerlegungsmaschine mit 4-Werte-Verdikt, refutation-first als Hauptachse. Dieses Repo ist 3-Werte verification-first — eine andere Designphilosophie.

• grounded-check = Zitier-Grounding-Check für LLM-Ausgaben, andere Domäne.

• rei-preregister = SHA256-Siegel für Vorhersagen, Vorregistrierungs-Tool.

• discovery-worker = Gegenbeispiel-Jäger, andere Schicht.

Eine Integration gibt es derzeit nicht, da sie Spec §5 („Unterstützung mehrerer Backends ist kein Ziel") widersprechen würde.

Beiträge / Meldungen

Bitte befolge die 4 Prinzipien aus Spec §8:

1. Wenn du unsicher bist, ob du eine Funktion hinzufügen sollst: füge sie nicht hinzu

2. Wenn du unsicher bist, ob du „wahrscheinlich richtig" zurückgeben sollst: gib UNDECIDED zurück

3. Wenn du unsicher bist, ob du Theorie in die API aufnehmen sollst: nimm sie nicht auf

4. Nicht hetzen, langsam vorgehen

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