rei-checker-mcp

Comprobador de verificación formal MCP v0.1.0a1 — recibe una línea y devuelve verdadero o falso. Ni más ni menos.

Veredicto de tres valores (VALID / INVALID / UNDECIDED). Sin LLM en la ruta de juicio. Cada UNDECIDED lleva un código de razón y se registra en un libro de refutación de solo anexión.

Licencia: AGPL-3.0-or-later Especificación: CHECKER_SPEC_v0.md Invariantes de diseño: CLAUDE.md

Ponerlo en marcha en 5 minutos

Con Python 3.9+ es suficiente. Sin dependencias externas (solo stdlib).

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

Salida esperada:

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

Las entradas no decidibles devuelven «no se puede decidir» (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"
}

código de salida: 0 = decisivo (VALID/INVALID), 2 = UNDECIDED. En un script de shell se puede ramificar directamente según «se pudo decidir o no».

Related MCP server: Chiasmus

Acumulación del ledger y estadísticas

Toda llamada a verify se anexa como una línea en 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 es el único indicador (spec §3). No importa que el valor inicial sea 0.1 — la condición de éxito es llegar a un estado medible.

La ubicación del ledger se puede sobrescribir con la variable de entorno $REI_CHECKER_LEDGER. Por defecto = ledger.jsonl en el directorio actual.

Uso como servidor MCP

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

Las herramientas MCP son solo 2 (spec §2, mínimo intencional):

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

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

Qué «no está construido» (explícito en spec §2)

Lo siguiente son no objetivos de v0. Si intentas implementarlo, detente y verifica:

• UI / frontend web

• Registro de usuarios, autenticación, facturación

• Gamificación, gestión de progreso, historial de aprendizaje

• Diálogo en lenguaje natural / generación de explicaciones

• Soporte de múltiples backends (solo Lean 4; el spike de v0 funciona con el backend Mock)

• Dependencia de funciones específicas de Claude

Estado de v0 (alcance honesto, spike 2026-08-22)

• ✅ Esquema (3 valores + 6 códigos de razón) completamente implementado

• ✅ Backend Mock (tabla de verdad para pruebas + activación de todos los códigos de razón)

• ✅ Ledger (JSONL de solo anexión, UTF-8, omisión de filas malformadas)

• ✅ Agregado de stats() (decision_rate + reason_breakdown)

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

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

• ⚠ El backend Lean 4 es un stub (candidato para v0.2, implementación prevista en el directorio lean_backend/)

• ⚠ La aplicación de timeout es suave (monitoreo de elapsed; el kill duro de procesos es para v0.2)

«Que se use primero» es la prioridad (spec §1.3, §6.6). Una vez completado el harness de Lean 4, basta con sustituir el backend para que funcione la verificación real. La superficie de API no cambia.

Fase 2 (no abordar hasta completar v0)

Estructura de tres capas definida en spec §9-13:

• Capa 1 checker (verify / stats) ← v0, esto

• Capa 2 education (locate_first_error / boundary_report / escalate)

• Capa 3 harness (calibration / regression / transfer)

Orden de implementación: capa 1 → capa 3② harness de calibración → capa 2. Detalles en spec §9-13.

Pruebas

python -m unittest tests.test_all -v

Según spec §7, priorizar las pruebas de los casos que deben devolver UNDECIDED (test individual de cada reason_code + happy path de VALID/INVALID).

Relación con el stack Rei (evitar confusiones)

Este repo es intencionalmente independiente. Distinción de las herramientas adyacentes:

• rei-verify (PyPI 0.1.0a1) = máquina de refutación con veredicto de 4 valores, eje principal refutation-first. Este repo es verification-first de 3 valores — filosofía de diseño distinta.

• grounded-check = verificación de grounding de citas en salidas de LLM, otro dominio.

• rei-preregister = sello SHA256 predictivo, herramienta de preregistro.

• discovery-worker = cazador de contraejemplos, otra capa.

No hay integración en este momento porque contravendría la spec §5 «soporte de múltiples backends: no objetivo».

Contribución / informes

Cumple los 4 principios de la spec §8:

1. Si dudas en añadir una función, no la añadas

2. Si dudas en devolver «probablemente correcto», devuelve UNDECIDED

3. Si dudas en exponer teoría en la API, no la expongas

4. Sin prisa, despacio

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