Millennium Harness CLI
Millennium Harness проверяет доказательства на Lean 4 и Dafny и отсекает подделки, пока агент не докажет теорему без лазеек.
- 2 893 ★ репозитория
- Последний коммит
- MIT
Расширенный доступ
Почему такой уровень
- Установка ставит Python-пакет из клона и запускает Lean и Dafny на чужих файлах, а режим агентов тратит платные вызовы моделей.
Установка
- Работает в
Ручная установка
git clone https://github.com/sahibzada-allahyar/Formal-Verification-RSI.git millennium-harness
cd millennium-harness && pip install -e ".[dev]"Команды из раздела Quickstart. Отдельно нужны Lean `v4.23.0-rc2` и Dafny 4.11.
Доступ и проверки
Как мы проверяемРасширенный доступИнструмент запускает код или ходит в сеть, а внешние данные только читает.
- Установка ставит Python-пакет из клона и запускает Lean и Dafny на чужих файлах, а режим агентов тратит платные вызовы моделей.
Это чужой код. Посмотрите файлы в репозитории перед установкой.
Что делает
Проверяющий шлюз без модели внутри: решение засчитывается, только если замороженная спецификация сохранила смысл и доказана без лазеек. Для Lean он ловит `sorry`, подмену экземпляров и нотации, лишние аксиомы, подмену скомпилированного кода и выполнение кода при разборе, затем повторяет проверку ядром. Для Dafny отклоняет `assume`, `{:axiom}`, леммы без тела и запрещенные атрибуты. В цикле с OpenCode или Claude Code агент завершает работу только при вердикте `PROVED`, а отказ возвращается ему следующим запросом. Автор приводит аудит 4 219 опубликованных решений и красную команду из 96 подделок, из которых шлюз принял ноль.
Для кого. Тем, кто поручает агентам формальные доказательства или проверенный код на Lean и Dafny и не хочет принимать на веру отчет «0 ошибок».
Подходит, если
- Агент сдает доказательство на Lean, где подозрительно сошлось с первой попытки и есть `sorry` или свой `instance`.
- Нужно проверить, не изменился ли смысл утверждения при неизмененном тексте теоремы.
- Бенчмарк или конвейер принимает решения по коду возврата, и надо убедиться, что его не обманывают.
- Агентский цикл в OpenCode или Claude Code должен продолжаться, пока решение не пройдет проверку.
Не подходит, если
- Обычный код без формальной спецификации: проверять там нечего.
- Нет возможности поставить Lean `v4.23.0-rc2` или Dafny 4.11: шлюз привязан к этим версиям.
- Нужен инструмент для построения доказательств: шлюз только проверяет готовое решение.
Пример запроса к агенту
Проверь мое решение `Solution.lean` против замороженной спецификации `frozen.json` и объясни вердикт: доказано оно по-настоящему или нет.Ограничения
Нужны Python 3.10 или новее и закрепленные версии: Lean `v4.23.0-rc2` через elan и Dafny 4.11. Путь к Dafny задается переменной `MILLENNIUM_DAFNY`. Сами проверки к модели не обращаются, но запуск агентов требует `OPENROUTER_API_KEY` или `ANTHROPIC_API_KEY`. Цифры в README собраны автором: набор подделок писался вместе с проверяющим, а 93 подделки в опубликованном бенчмарке названы нижней оценкой. С другими моделями прирост в цикле составил от нуля до двух задач. Установка идет из клона репозитория через `pip install -e`.
Как отключить. Удалите клон `millennium-harness` и виртуальное окружение, где выполнен `pip install -e`. Плагины из каталога `adapters/` отключите в настройках OpenCode или Claude Code.
Частые вопросы
Какие вердикты выдает шлюз?
`PROVED`, `UNPROVED`, `CHEAT_REJECTED`, `SPEC_TAMPERED` или `CHECK_ERROR`. Поле `feedback` содержит сообщение, которое видит агент.
Как зафиксировать спецификацию?
Командой `python -m millennium_harness.lean lock task_record.json frozen.json`. Затем решение проверяют командой `check`.
Что он ловит в Dafny?
`assume`, `{:axiom}`, леммы без тела с `ensures`, запрещенные атрибуты и перехваченные вспомогательные определения спецификации, затем идут `dafny audit` и проверка компиляции.
Нужны ли ключи API?
Для самих проверок нет. Ключ `OPENROUTER_API_KEY` или `ANTHROPIC_API_KEY` нужен только для запуска агентов и бенчмарков.
С какими агентами он работает?
В каталоге `adapters/` лежат плагины для OpenCode и Claude Code, а `bench/agents_fv.py` запускает любой из них со шлюзом в песочнице.
Обсуждение
Вопросов и отзывов пока нет.
Похожие
CLI-инструментыПлагин для доказательства теорем в Lean 4: поиск по mathlib, циклы заполнения sorry, проверка аксиом и страховочные хуки
Хартия на 2,4 КБ для CLAUDE.md и три скилла по вызову: агент проверяет результат и ждет подтверждения перед необратимым
ADLC Harness ведет задачу от намерения до PR одной командой, а человек подтверждает только четыре ключевых этапа.
Линтер обвязки агента проверяет AGENTS.md, CLAUDE.md, CI и хуки репозитория и выставляет оценку по шести направлениям.
Скиллы Lean 4 для Codex и Claude Code: от проекта до сверки формулировки с исходной теоремой, 12 процессов
Плагин DiDi для Codex и Claude Code ведет задачу от предложения к архиву и копит проверенные знания проекта в репозитории
Коротко о README
README объясняет, как агенты обманывают проверку доказательств, и показывает шлюз Millennium Harness с таблицей результатов. Ставится из клона, есть плагины для OpenCode и Claude Code.