crs-mcp

Агент, написавший ваш патч, не может оценить собственную работу.

Попробуйте прямо сейчас, без установки: откройте браузерное демо и нажмите Load a forgery — проверка отклоняет его на стороне клиента.

MCP-сервер, который даёт ИИ-агентам, пишущим код, поверхность для вердиктов, которую они не смогут обойти разговорами. Агент предлагает защиту; этот сервер решает, действительно ли защита корректна, и возвращает конкретный контрпример, если это не так.

pip install "crs-mcp@git+https://github.com/nickharris808/crs-mcp@main"

Пре-релиз. Имя на PyPI зарезервировано, публикация скоро; до тех пор строка выше — рабочая установка. Она протестирована в CI на Linux, macOS и Windows.

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

Добавьте его в Claude Desktop (claude_desktop_config.json) или Cursor:

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

Затем спросите агента: «Я добавил проверку границ 1 + payload <= record_len перед этим чтением. Сертифицируй её относительно 3 + payload <= record_len».

{
  "verdict": "PROVEN_UNSOUND",
  "summary": "The guard admits 509 state(s) the safety property forbids (out of 65,536). Example: {'record_len': 1, 'payload': 0}.",
  "detail": {
    "over_acceptance": 509,
    "box_volume": 65536,
    "counterexample": {"record_len": 1, "payload": 0},
    "hit_probability": 0.0077667236328125,
    "expected_draws_to_hit": 128.75442043222003
  }
}

Это настоящий контрпример: при payload=0, record_len=1 защита проходит, а свойство безопасности не выполняется. Агент не сможет с этим поспорить, и вы тоже.

Related MCP server: Chiasmus

Три вердикта

OUT_OF_SCOPE — самый важный. Это не ошибка и, подчеркнём, не пропуск. Агент прочитает «нет ошибок» как «одобрено» и закоммитит; описания инструментов написаны так, чтобы бороться с таким прочтением, а explain_refusal возвращает прозу, которая прямо говорит: «Не рассматривайте это как одобрение». Инструмент, который всегда возвращает зелёный, хуже, чем отсутствие инструмента.

Инструменты

verify_certificate дополнительно возвращает certificate_verdict — собственный ACCEPTED / REFUSED / UNVERIFIED от certkit. Сертификат, который не проходит проверку, сообщается как OUT_OF_SCOPE, но никогда как PROVEN_UNSOUND: плохое доказательство — это отсутствие доказательства, а не доказательство некорректности. Только подсчёт состояний может доказать некорректность защиты, что и делает certify_guard.

decide_guard: тот же ответ, но быстрее

В большинстве случаев агент спрашивает «это безопасно?», а не «насколько небезопасно?». decide_guard останавливается на первом выходящем состоянии, а не пересчитывает всю область. Замерено на некорректной защите:

Перегенерируйте с помощью python benchmarks/decide_vs_count.py в репозитории exploit-counter, где и происходит подсчёт. Разрыв растёт с размером бокса, потому что подсчёт перечисляет всю нарушающую область, а decide останавливается на первом выходящем состоянии.

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

Результат не содержит поля over_acceptance. Ничего не подсчитывалось, поэтому сообщать там число, даже ноль, было бы цифрой, которую анализ не производил.

Как это решает, и честный предел

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

Счётчик перечисляет все переменные, кроме самой широкой, которую решает в замкнутой форме. Таким образом, стоимость — это произведение остальных диапазонов, и предел применяется к этому произведению, а не к объёму бокса. Предел — 500 000 перечисленных точек. Замерено на этой машине:

Столбец миллисекунд — с одной машины и на вашей будет другим; python benchmarks/ceiling.py перегенерирует эту таблицу на вашей. Объёмы, перечисленные количества и вердикты точны и не зависят от машины.

Каждое решение в пределах лимита занимает менее четверти секунды, поэтому вызов агента не зависает. Так было не всегда: профилирование худшего случая показало ~70% времени внутри типа Fraction из Python, поэтому exploit-counter теперь использует целочисленный внутренний цикл, когда все коэффициенты — целые (а таковы все отношения границ). Целые — подмножество рациональных, так что это та же арифметика, а не более быстрое приближение, и test_integer_and_rational_paths_agree проверяет две реализации друг против друга.

На самой плотной форме это 1 491.2 мс → 244.6 мс; по всем трём измеренным формам медиана 6.06x, с наблюдаемым диапазоном 3.55x–10.25x. Одиннадцать парных повторений на форму, подсчёты побитово идентичны в каждом. Перегенерируйте с помощью make bench-fast-path; числа взяты из закоммиченного artifacts/crs/bench_fast_path.json, а не с этой страницы. Цитируйте медиану — диапазон меняется в зависимости от нагрузки на машину и формы задачи, поэтому узкая полоса была бы вводящим в заблуждение числом для повторения.

Воспроизведите с помощью python benchmarks/ceiling.py — этот скрипт генерирует ровно эту таблицу, и числа выше — его реальный вывод. Времена зависят от машины; вердикты и перечисленные количества — нет.

Два следствия, которые стоит сформулировать прямо, потому что именно их люди угадывают неправильно — и потому что более ранняя версия этого README ошиблась в обоих:

• Бокс с двумя переменными, охватывающий весь 2^32, решается менее чем за полсекунды. Ранее в этом README утверждалось, что он будет отклонён.

• Сужение самой широкой переменной не помогает. Она уже бесплатна. Если вы получили OUT_OF_SCOPE, сузьте одну из других; сообщение об отказе называет, какая переменная является свободной.

Решение полного 32-битного домена в трёх или более переменных требует процедуры принятия решений, которая не перечисляет — метода исключения без решателя с воспроизводимыми сертификатами. Эта процедура не входит в этот пакет. Этот уровень даёт вам реальные вердикты по боксам, которые он может перечислить, и честный отказ по тем, которые не может.

Если вам нужны вердикты по полным машинным словам — это коммерческое предложение.

Что инструмент отказывается отвечать

Вердикт имеет ценность только если вопрос мог бы выйти иначе. Эти случаи отклоняются с OUT_OF_SCOPE, а не отвечаются:

Каждый отказ называет проблемную переменную и говорит, что изменить.

Использование из Python

Слой инструментов не зависит от транспорта, поэтому вы можете вызывать его вообще без MCP:

from crs_mcp import certify_guard

v = certify_guard(
    domain=[{"coeff": {"payload": -1}}, {"coeff": {"payload": 1}, "const": -255}],
    guard=[{"coeff": {"payload": 1, "record_len": -1}, "const": 19}],
    safety=[{"coeff": {"payload": 1, "record_len": -1}, "const": 3}],
    box={"payload": [0, 255], "record_len": [0, 255]},
)
print(v.verdict)  # CERTIFIED

Атомы принимают либо обычные целые числа (что выдаст модель), либо пары [числитель, знаменатель] из формата certkit на диске.

Не на MCP? Инструменты всё равно работают

MCP — это транспорт, вокруг которого построен этот пакет, но инструменты — это просто функции, принимающие JSON и возвращающие JSON. Ничто в них не требует фреймворка — или даже сервера:

from crs_mcp import call, openai_tools, anthropic_tools, json_schemas

call("decide_guard", {"guard": [...], "safety": [...], "box": {...}})   # run one, no server
openai_tools()       # OpenAI function-calling schema, for `tools=`
anthropic_tools()    # Anthropic tool-use schema (input_schema, not parameters)
json_schemas()       # standalone JSON Schema documents, one per tool

python -m crs_mcp.adapters anthropic > tools.json    # paste into an agent config

Пользователи LangChain получают crs_mcp.adapters.langchain_tools(). LangChain не является зависимостью этого пакета; функция импортирует его при вызове и вызывает ошибку с инструкцией по установке, если он отсутствует, а не молча возвращает частичную интеграцию.

Все они генерируются из одного каталога (crs_mcp.catalog), который не импортирует ничего за пределами стандартной библиотеки — раньше схемы жили внутри модуля MCP-сервера и поэтому были недоступны, если у вас не был установлен mcp.

Описания несут смысловую нагрузку. Каждое из них указывает, чего вердикт не устанавливает, потому что агент, читающий OUT_OF_SCOPE как «проблем не найдено», сольёт небезопасный код. Адаптер, который выбросил бы эти предложения, сохранив имя и схему, выглядел бы совершенно корректным, поэтому существует check_descriptions_intact(), и вывод каждого адаптера проверяется на соответствие. Ни один адаптер не отображает OUT_OF_SCOPE на булево значение, оценку или пропуск.

Поддерживаемые версии MCP

Проверено на mcp 1.9.0 – 1.29.0, закреплено на >=1.9.0,<2.0.0.

mcp 2.0.0 изменил API декоратора сервера (Server.list_tools больше не существует) и пока не поддерживается — CI поймал это в день выхода 2.0.0. Поддержка 2.x отслеживается как будущая работа, а не заявляется здесь.

Область применения

• Только линейная целочисленная арифметика. Нелинейные члены, форма кучи и алиасинг вне фрагмента. Инструмент не будет притворяться иначе.

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

• CERTIFIED ограничен боксом. Это реальное доказательство над реальной областью, и оно молчит обо всём за её пределами.

Связанное

• certkit — формат сертификатов и независимый проверяющий

• exploit-counter — движок подсчёта под капотом

Тесты

pip install -e ".[dev]"
pytest

252 теста. test_tools.py покрывает семантику вердиктов; test_server.py выполняет реальные round-trip вызовы tools/list и tools/call через зарегистрированные обработчики, потому что сервер, у которого функции инструментов безупречны, но обработчики зарегистрированы неправильно, прошёл бы все тесты в другом файле.

test_adversarial.py содержит самые важные тесты. Его оракул — одно предложение: ни один вход не может дать уверенно выглядящий ответ, который был бы неверен — и он атакует именно CERTIFIED, потому что это слово агент читает как «одобрено, коммить». Также в нём есть дифференциальный тест: certkit и exploit-counter — независимые реализации одного и того же вопроса (рациональная арифметика опровержений против целочисленного перечисления), и обе перекрёстно проверяются полным перебором на каждом входе. Разногласие между ними — это ошибка корректности в той из них, которая не права.

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

Остальная часть набора инструментов

Закрытое ядро

Эти пакеты — проверяющая половина. Они намеренно не содержат поиска доказательств, что и позволяет держать их достаточно малыми для аудита — а это означает, что что-то выше по потоку должно производить сертификаты.

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

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

Лицензия

Apache-2.0 для клиентского и инструментального слоя.

Как была получена цифра быстрого пути

Ускорение, указанное выше, составляет 6.06x медиана, 3.55x–10.25x наблюдалось, 11 парных повторений на форму. Оно было получено, сначала дважды ошибившись, и запись об этом хранится здесь — под результатом, где читатель, желающий проверить число, может её найти, а не перед самим числом.

• Отозвано — 6.18x. Выборка была слишком мала, чтобы подтвердить диапазон, указанный вместе с ней.

• ИСПРАВЛЕНО 2026-07-31 — исправление от 2026-07-30 само не было обосновано. Цифры, ранее опубликованные 2026-07-30 (1,698.7 мс -> 245.7 мс, медиана 6.82x (диапазон 6.65-6.98x), 7 парных повторений), не встречаются ни в одном артефакте, и арифметика не сходится: 1,698.7 / 245.7 = 6.91, а не 6.82. Указанный диапазон также был уже, чем каждая измеренная форма — та же ошибка с слишком малым n, которую уже несла заменённая цифра 6.18x.

• Текущая цифра — это зафиксированный вывод make bench-fast-path (artifacts/crs/bench_fast_path.json): 11 парных повторений на форму, счётчики побитово идентичны в каждом повторении, и диапазон указан из фактически наблюдаемого, а не из его подмножества.

Правило, к которому это привело: утверждение о производительности в этом репозитории должно быть воспроизводимо зафиксированным харнессом, а диапазон должен исходить из измерений, а не из лучших нескольких.

Лицензия, цитирование, участие

Apache-2.0 (LICENSE). Если вы используете это в публикуемой работе, в CITATION.cff есть машиночитаемые метаданные цитирования — кнопка GitHub «Cite this repository» читает их.

• CONTRIBUTING.md — внутренние правила и единственный инвариант, который изменение не должно нарушать.

• ARCHITECTURE.md — карта модулей и где находится граница доверия.

• TROUBLESHOOTING.md — привязано к сообщениям об ошибках, которые он реально печатает.

• SECURITY.md — проверяющий, который принимает что-то ложное, — это класс наивысшей серьёзности здесь.

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