minicheck-mcp

Модель-чекер как MCP-сервер. Пусть агент проверяет конечный автомат, а не гадает.

Зачем это существует

Агенты постоянно проектируют конечные автоматы — циклы повторных попыток, протоколы блокировок, жизненные циклы сессий, передачу управления между субагентами — а затем рассуждают о корректности в прозе. Рассуждения в прозе о конкурентности подводят модель так же, как и человека: рассматриваются те перемежения, которые приходят на ум, и упускается то, которое не приходит.

Агент с процедурой принятия решений не должен гадать. Он получает вердикт и, когда свойство нарушается, точную последовательность шагов, которая его ломает — а это как раз то, что нужно, чтобы исправить дизайн, а не извиняться за него.

Спецификация, которую он отправляет, — это данные, а не код, поэтому ничего из того, что отправляет агент, не выполняется — и в ответ приходит вердикт с кратчайшим контрпримером-трассой.

Related MCP server: agent-gate

Установка

# from GitHub (PyPI release pending)
pip install "minicheck-mcp @ git+https://github.com/nickharris808/minicheck-mcp.git"
pip install "minicheck-mcp[mcp] @ git+https://github.com/nickharris808/minicheck-mcp.git"  # + the MCP SDK

pip install minicheck-mcp пока не работает — пакета нет на PyPI. Установите из GitHub, как показано выше; это автоматически подтянет minicheck. python build_pypi.py создаёт артефакт, готовый для загрузки на PyPI, когда оба пакета будут опубликованы (PyPI отклоняет прямую зависимость, которую использует этот пакет, чтобы оставаться устанавливаемым без индекса).

Затем зарегистрируйте его (claude_desktop_config.json или любой MCP-клиент):

{ "mcpServers": { "minicheck": { "command": "minicheck-mcp" } } }

Репозиторий поставляется с этим файлом как mcp.json.

Быстрый старт за 30 секунд

Спросите агента: «У меня есть цикл повторных попыток, который увеличивает счётчик, пока не сработает. Проверь, что он не может повториться более 3 раз». Он отправляет эту спецификацию в check_invariant:

{
  "name": "retry",
  "fields": ["tries", "done"],
  "initial": {"tries": 0, "done": 0},
  "transitions": [
    {"label": "attempt", "when": {"done": 0}, "set": {"tries": {"incr": 1}}},
    {"label": "succeed", "when": {"done": 0}, "set": {"done": 1}}
  ],
  "invariants": {"bounded_retries": {"forbid": {"tries": 4}}}
}

и получает в ответ — воспроизведите это с помощью python -c "from minicheck_mcp import dispatch; import json; print(json.dumps(dispatch('check_invariant', {'spec': SPEC}), indent=2))":

{
  "ok": true,
  "reachable_states": 129,
  "exhaustive": false,
  "invariants": {
    "bounded_retries": {
      "holds": false,
      "counterexample": [
        {"label": null,      "state": {"tries": 0, "done": 0}},
        {"label": "attempt", "state": {"tries": 1, "done": 0}},
        {"label": "attempt", "state": {"tries": 2, "done": 0}},
        {"label": "attempt", "state": {"tries": 3, "done": 0}},
        {"label": "attempt", "state": {"tries": 4, "done": 0}}
      ],
      "steps": 4
    }
  },
  "incomplete_reason": "IntBoundExceeded: transition 'attempt' drives field 'tries' to 65, outside int_bound 64. The state space is not finite under this bound, so no exhaustive verdict is available. Re-run with int_bound >= 65.",
  "advice": "the state space was not fully explored, so any invariant not refuted below is UNDETERMINED (null), not proved. Raise int_bound or add a 'when' guard that bounds the growing field, then check again.",
  "all_hold": false,
  "verdict": "REFUTED",
  "verdict_means": "a counterexample was found; it starts at the initial state and replays"
}

Не «возможно, зациклится навсегда» — а точные четыре шага, которые это ломают.

Однако прочитайте весь ответ — и этот быстрый старт объясняет, почему: exhaustive — false. Опровержение остаётся в силе — контрпример несёт собственное свидетельство, и эта трасса воспроизводится — но ничто другое в этой спецификации не было установлено, потому что у attempt нет ограничителя, и он доводит tries до значения за пределами int_bound. Для опровержения достаточно одного свидетеля; для доказательства нужно всё пространство состояний.

Учебник — как выглядит реальная сессия

Агент написал жизненный цикл сессии и хочет узнать, можно ли использовать сессию после её закрытия. Вот весь диалог.

1. Агент запрашивает формат (spec_help), затем отправляет check_invariant:

{
  "name": "session",
  "fields": ["state", "used"],
  "initial": {"state": 0, "used": 0},
  "transitions": [
    {"label": "open",  "when": {"state": 0}, "set": {"state": 1}},
    {"label": "use",   "when": {"state": 1}, "set": {"used": 1}},
    {"label": "close", "when": {"state": 1}, "set": {"state": 2}},
    {"label": "reopen","when": {"state": 2}, "set": {"state": 1}}
  ],
  "invariants": {"no_use_after_close": {"forbid": {"state": 2, "used": 1}}}
}

2. Он получает опровержение с точным путём:

{
  "ok": true,
  "verdict": "REFUTED",
  "exhaustive": true,
  "reachable_states": 5,
  "all_hold": false,
  "invariants": {
    "no_use_after_close": {
      "holds": false,
      "steps": 3,
      "counterexample": [
        {"label": null,    "state": {"state": 0, "used": 0}},
        {"label": "open",  "state": {"state": 1, "used": 0}},
        {"label": "use",   "state": {"state": 1, "used": 1}},
        {"label": "close", "state": {"state": 2, "used": 1}}
      ]
    }
  }
}

Инвариант, как он записан, запрещает когда-либо использовать закрытую сессию, что не то, что имел в виду агент — он имел в виду «никакого перехода use в закрытом состоянии». Контрпример делает разницу конкретной, а не оставляет её на уровне правдоподобного абзаца.

3. Агент исправляет модель и запускает снова. used должно означать «использовалась с момента открытия этой сессии», поэтому close сбрасывает его:

{"label": "close", "when": {"state": 1}, "set": {"state": 2, "used": 0}}

{"ok": true, "verdict": "PROVED", "exhaustive": true, "reachable_states": 4, "all_hold": true}

PROVED и exhaustive: true — это пара, которую нужно читать. Первое не может быть выдано без второго, но проверка обоих делает привычку явной — и именно эта привычка защищает вас в тот день, когда спецификация вырастет за пределы ограничения.

4. Чего агент не должен делать. Если ответ — "verdict": "UNDETERMINED", это не прохождение. Это означает, что поиск остановился рано — прочитайте incomplete_reason и advice, ограничьте растущее поле и спросите снова. Если ok — false, вердикта не существует вовсе, и all_hold — null.

Инструменты

Формат спецификации

{
  "name": "mutex",
  "fields": ["a", "b", "lock"],
  "initial": {"a": 0, "b": 0, "lock": 0},
  "transitions": [
    {"label": "a_enter", "when": {"a": 0, "lock": 0}, "set": {"a": 1, "lock": 1}},
    {"label": "a_exit",  "when": {"a": 1},            "set": {"a": 0, "lock": 0}}
  ],
  "invariants": {"not_both": {"forbid": {"a": 1, "b": 1}}},
  "goal": {"require": {"a": 1}}
}

when — это конъюнкция проверок field == value (опустите для всегда-разрешённых). set присваивает литерал или {"incr": n} / {"decr": n} для целых чисел. Инвариант — это {"forbid": {...}} (нарушается, когда каждое перечисленное поле совпадает) или {"require": {...}} (нарушается, если они не совпадают).

Целые числа ограничены, и ограничение проверяется — int_bound (по умолчанию 64) — это наибольшая величина, которую может принимать поле. Прогон, который вывел бы поле за его пределы, останавливается и сообщает exhaustive: false, а не насыщает значение, потому что молча усечённый поиск сообщает «выполняется» для состояний, которые он никогда не посещал. См. Честные границы о том, как читать полученный вердикт.

Почему декларативно

MCP-сервер, который выполнял бы Python-код от агента через exec, был бы дырой удалённого выполнения кода с лишними шагами. Спецификации здесь — это данные: значение поля, выглядящее как __import__('os').system(...), остаётся строкой и сравнивается как строка. Есть тест, который проверяет именно это.

Без SDK? Всё равно работает.

Инструменты — это обычные функции. dispatch — та же точка входа, которую использует транспорт, так что вы можете вызывать её из скрипта или теста без агента в цикле:

from minicheck_mcp import dispatch
dispatch("check_invariant", {"spec": my_spec})

Без установленного mcp minicheck-mcp выводит JSON-ошибку с объяснением, как его установить, и завершается с ненулевым кодом, а не с traceback.

Честные границы

Читайте вердикт как трёхзначный. Это самая важная часть для агента, потому что агент читает поле и действует по нему, а не привносит суждение в абзац.

Каждый ответ также несёт verdict_means — однострочное объяснение, которое агент может процитировать пользователю дословно, а не пересказывать (и, возможно, смягчать).

Каждый ответ несёт all_hold и holds явно, включая ошибки. Более ранняя версия опускала их при сбое, поэтому result.get("all_hold") возвращал None и для краха, и для настоящего неопределённого результата — и оба ложны, точно так же, как опровержение.

Когда exhaustive — false, ответ также несёт incomplete_reason и advice, указывающие, что изменить. Массив warnings появляется, когда инвариант тривиально выполняется — он действительно выполняется, но ничего не проверяет.

Что это доказывает. Что конечный декларативный конечный автомат удовлетворяет или не удовлетворяет инварианту при каждом перемежении в пределах объявленных границ.

Чего это не доказывает.

• Ничего о вашей реализации — только о спецификации, которую вы отправили. Спецификация абстрагирует.

• Ничего за пределами int_bound (по умолчанию 64) или ограничения в 200 000 состояний. Превышение любого из них даёт UNDETERMINED, никогда не молчаливое прохождение.

• Ничего о живости за пределами AG-EF и ничего в LTL.

Ничто в спецификации никогда не выполняется. Спецификация — это данные: имена полей, литералы и сравнения. Нет eval, нет exec и нет пути кода, который превращает строку в спецификации в вызываемый объект. Именно поэтому существует декларативный загрузчик, а не приём Python.

Чего здесь нет

Это движок и безопасный способ его вызова. Поддерживаемые корпуса опасных свойств, композиционный анализ, который находит опасности, существующие только при объединении двух компонентов, и цепочка доказательств, делающая вердикт проверяемым впоследствии, — это коммерческое предложение. Этот сервер — MIT и остаётся таким.

Устранение неполадок

ok: false, error: "SpecError". Спецификация некорректна, и сообщение называет ключ. Сначала вызовите validate_spec или spec_help для формата с рабочим примером.

verdict: "UNDETERMINED" для спецификации, которая, как я ожидал, пройдёт. Поиск не покрыл всё пространство состояний — обычно это поле, которое растёт без ограничений. Прочитайте incomplete_reason и advice. Добавьте ограничитель when, который остановит рост. Не считайте это прохождением.

ok: false, error: "BadArguments". Инструмент был вызван с аргументом, который он не принимает. Каждый инструмент принимает spec; check_invariant также принимает необязательное имя invariant.

ok: false на check_liveness с "spec declares no 'goal'". Для живости нужна цель. Добавьте блок goal в той же форме, что и инвариант.

Появился массив warnings, а инвариант всё ещё говорит holds: true. Инвариант называет значение, которое ограниченное пространство не может представить, поэтому он выполняется по причине, не связанной с вашим протоколом — обычно это опечатка в литерале или int_bound ниже значения, которое вы хотели запретить.

Сервер немедленно завершается с JSON-ошибкой. MCP SDK не установлен: pip install "minicheck-mcp[mcp] @ git+https://github.com/nickharris808/minicheck-mcp.git". Инструменты остаются импортируемыми и тестируемыми без него через from minicheck_mcp import dispatch.

Мой агент считает ошибку «свойство в порядке». Он не должен иметь такой возможности: каждый ответ несёт all_hold и holds явно, и оба — null при любой ошибке, вместе с verdict: "ERROR". Сначала ветвитесь по result["ok"].

Производительность

Ограничена базовым чекером. Спецификации приходят сюда декларативно, что является скомпилированным путём чекера — примерно 2,5×10⁵–7,5×10⁵ состояний/сек в CPython 3.11 на ноутбуке с M-чипом, воспроизводимо запуском python bench.py в репозитории minicheck. Спецификация, умещающаяся в несколько десятков тысяч состояний, отвечает значительно быстрее секунды. В самом серверном слое нет измеренного узкого места — это тонкая диспетчеризация.

FAQ

«Разве запуск спеки из языковой модели не позволяет ей выполнять код?» Нет, и именно для этого существует декларативный формат. Спека — это данные: имена полей, литералы и сравнения на равенство. Здесь нет eval, нет exec и нет пути кода, который превращает строку в спеке в вызываемую функцию. Значение поля, выглядящее как __import__('os').system(...), остаётся строкой и сравнивается как строка. Существует тест, который проверяет именно это, а набор состязательных тестов отправляет payload-ы в форме кода в каждый инструмент. (minicheck's Python Model API — другое дело: это код, и недоверенные модели из него заслуживают той же осторожности, что и любой недоверенный Python. Этот сервер его не предоставляет.)

«Почему бы просто не позволить агенту писать Python и запускать его?» MCP-сервер, который exec'ил бы Python от агента, был бы дырой удалённого выполнения кода с лишними шагами. Декларативный формат стоит выразительности, но даёт свойство, которое можно сформулировать в одном предложении и протестировать.

«Мой агент прочитал all_hold и заключил, что свойство в порядке, но была ошибка.» Он не должен этого делать: каждый ответ явно содержит all_hold и holds, и оба равны null при любой ошибке, вместе с verdict: "ERROR" и ok: false. Более ранняя версия опускала их при сбое, поэтому result.get("all_hold") возвращал None и для краха, и для подлинно неопределённого результата — и оба ложны, точно так же, как опровержение. Сначала проверяйте result["ok"], затем verdict, и никогда не полагайтесь на истинность all_hold.

«Почему в каждом ответе есть строка verdict_means?» Потому что агент, перефразируя вердикт, склонен его смягчать, и «проверка была неокончательной» превращается в «выглядит нормально» через два шага. verdict_means — это однострочное объяснение, которое агент может дословно процитировать пользователю.

«UNDETERMINED — агенту следует повторить попытку или сообщить об успехе?» Ни то, ни другое по умолчанию. Это означает, что поиск остановился рано, так что ничего не установлено. Прочитайте incomplete_reason и advice, которые указывают, что изменить — обычно поле, растущее без ограничений. Ограничьте его и спросите снова. Сообщение о прохождении — это режим отказа, против которого направлен весь этот пакет.

«Нужен ли мне MCP SDK?» Только для обслуживания через транспорт. Инструменты — это обычные функции: from minicheck_mcp import dispatch — та же точка входа, которую использует транспорт, так что вы можете вызывать её из скрипта или теста без агента в цикле. Без установленного mcp команда minicheck-mcp выводит JSON-ошибку с инструкцией по установке и завершается с ненулевым кодом, а не с traceback-ом.

«Готов ли он к продакшену?» Да, и полностью протестирован — но окружающая экосистема агентов быстро развивается, поэтому поверхность MCP — это та часть, которая скорее всего потребует обновления версии. Проверяющий движок — это minicheck, и он стабилен.

«Что-то здесь дало мне уверенный ответ, который оказался неверным.» Стоит сообщить об этом как об issue, а не искать обходной путь; пожалуйста, включите спеку. Ложный holds: true, достижимый из сервера, ориентированного на агентов, — это самая серьёзная ошибка, которую может иметь этот пакет, и именно такая ошибка была найдена, исправлена и раскрыта в minicheck 0.1.0.

Тесты

pip install -e ".[test]" && pytest

$ pytest -q
........................................................................ [ 74%]
.........................                                                [100%]
100 passed in 2.31s

102 теста, каждый инструмент через реальный путь dispatch, включая некорректный ввод, неизвестные инструменты и гарантию отсутствия выполнения кода. Один из них проверяет собственное количество тестов этого README против pytest --collect-only, так что бейдж не может устареть.

Портфолио

Одна идея проходит через все: вердикт, который нельзя проверить, — не вердикт — и её следствие, управляющее каждой поверхностью здесь: неопределённость — это не прохождение.

Попробуйте в браузере · проверьте конечный автомат · таблица лидеров specforge

Эталонные данные · protocol-bench · specforge

Коммерческое предложение

Это движок. Что не является открытым исходным кодом, так это то, что делает его полезным в масштабе: поддерживаемые корпуса опасных свойств, композиционный анализ, который находит опасности, существующие только при объединении двух компонентов, анализ чувствительности к модели доверия и цепочка доказательств, делающая вердикт проверяемым задним числом. Инструменты выше имеют лицензию MIT и остаются таковыми.

Документация

Полная документация, включая руководство по концепциям и честное сравнение с TLA+, SPIN, Alloy и CBMC, находится по адресу https://nickharris808.github.io/verification-docs/.

Вклад

Приветствуются сообщения об ошибках и pull request-ы — см. CONTRIBUTING.md. Контрпример, который этот инструмент обрабатывает неправильно, — это самое полезное, что вы можете отправить.

Цитирование

Метаданные цитирования находятся в CITATION.cff; GitHub отображает кнопку Cite this repository на их основе.

Лицензия

MIT. См. LICENSE.