rei-checker-mcp

Формальный верификационный чекер MCP v0.1.0a1 — принимает одну строку, возвращает истину или ложь. Не больше и не меньше.

Трёхзначный вердикт (VALID / INVALID / UNDECIDED). Никакой LLM в пути принятия решения. Каждый UNDECIDED сопровождается кодом причины и попадает в журнал опровержений, доступный только для добавления.

Лицензия: AGPL-3.0-or-later Спецификация: CHECKER_SPEC_v0.md Инварианты дизайна: CLAUDE.md

Запуск за 5 минут

Достаточно Python 3.9+. Внешних зависимостей нет (только stdlib).

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

Для неразрешимого ввода возвращается «не могу определить» (спец. §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"
}

код выхода: 0 = определённый (VALID/INVALID), 2 = UNDECIDED. В shell-скрипте можно напрямую ветвиться по условию «удалось ли определить».

Related MCP server: Chiasmus

Накопление журнала и статистика

Каждый вызов verify дописывается одной строкой в ledger.jsonl (спец. §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 — единственный показатель (спец. §3). Даже если начальное значение 0.1 — неважно, условие успеха — перейти в состояние, которое можно измерять.

Расположение журнала можно переопределить через переменную окружения $REI_CHECKER_LEDGER. По умолчанию — ledger.jsonl в текущем каталоге.

Использование в качестве MCP-сервера

Регистрация в 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-инструментов ровно два (спец. §2, намеренный минимум):

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

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

Что «не создано» (явно указано в спец. §2)

Ниже — не-цели v0. Если захотите реализовать — остановитесь и уточните:

• UI / веб-фронтенд

• Регистрация пользователей, аутентификация, биллинг

• Геймификация, управление прогрессом, история обучения

• Диалог на естественном языке, генерация пояснений

• Поддержка нескольких бэкендов (только Lean 4, v0 spike работает на Mock backend)

• Зависимость от функций, специфичных для Claude

Состояние v0 (честный объём, spike от 2026-08-22)

• ✅ Схема (3 значения + 6 кодов причин) полностью реализована

• ✅ Mock backend (таблица истинности для тестов + триггеры всех кодов причин)

• ✅ Журнал (append-only JSONL, UTF-8, пропуск повреждённых строк)

• ✅ Агрегация stats() (decision_rate + reason_breakdown)

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

• ✅ CLI (подкоманды verify / stats / mcp / version)

• ⚠ Бэкенд Lean 4 — заглушка (кандидат на v0.2, планируется реализация в lean_backend/)

• ⚠ Принудительный таймаут — мягкий (мониторинг elapsed, жёсткое завершение процесса — в v0.2)

Приоритет — «чтобы начали использовать» (спец. §1.3, §6.6). После завершения harness для Lean 4 замена бэкенда запустит реальную проверку. API-поверхность не изменится.

Phase 2 (не начинать до завершения v0)

Трёхуровневая структура, определённая в спец. §9-13:

• Уровень 1: checker (verify / stats) ← v0, это

• Уровень 2: education (locate_first_error / boundary_report / escalate)

• Уровень 3: harness (calibration / regression / transfer)

Порядок реализации: уровень 1 → уровень 3② calibration harness → уровень 2. Подробности в спец. §9-13.

Тестирование

python -m unittest tests.test_all -v

Согласно спец. §7, приоритет — тесты случаев, которые должны возвращать UNDECIDED (отдельный тест для каждого reason_code + happy path для VALID/INVALID).

Отношение к стеку Rei (во избежание путаницы)

Этот репозиторий намеренно независим. Отличия от смежных инструментов:

• rei-verify (PyPI 0.1.0a1) = машина опровержения, 4-значный вердикт, основная ось — опровержение-вперёд. Этот репозиторий — 3-значный verification-first, философия дизайна иная.

• grounded-check = проверка цитирования/обоснованности выходных данных LLM, другая область.

• rei-preregister = предварительная регистрация с SHA256-печатью, инструмент предварительной регистрации.

• discovery-worker = охотник за контрпримерами, другой уровень.

Интеграции на данный момент нет, так как это противоречит спец. §5 «поддержка нескольких бэкендов — не-цель».

Вклад / сообщения об ошибках

Пожалуйста, соблюдайте 4 принципа из спец. §8:

1. Если сомневаетесь, добавлять ли функцию, — не добавляйте

2. Если сомневаетесь, возвращать ли «возможно, верно», — возвращайте UNDECIDED

3. Если сомневаетесь, выносить ли теорию в API, — не выносите

4. Не спешите, двигайтесь медленно

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