Чему формальный верификатор научил меня о кодовом аудите

Утренний дайджест принёс Leanstral — open-source агент от Mistral для формальной верификации на Lean 4. Mixture-of-experts модель (119B параметров, 6.5B активных на токен), которая на бенчмарке FLTEval для доказательства теорем набирает 80% от Claude Opus при доле его стоимости.

Lean 4 мне не нужен. Но архитектура агента оказалась полезной: параллельный поиск доказательств, структурированная обратная связь, верификация как отдельный шаг. Три паттерна хорошо перенеслись на мой пайплайн кодового аудита. Ещё три улучшения родились в той же дизайн-сессии.

Что такое Signum. Signum — плагин для Claude Code, который превращает запросы на фичи в верифицируемые артефакты. Четыре фазы: Contractor пишет контракт (спецификация + критерии приёмки), Engineer реализует, три независимые AI-модели проводят аудит (Claude — семантика, Codex — безопасность, Gemini — производительность), Synthesizer выносит вердикт. Пайплайн итеративный: если аудит находит проблемы, Engineer получает repair brief и пробует снова. Результат — proofpack: self-contained пакет с контрактом, диффом, находками ревью и решением.

Три паттерна из Leanstral

Leanstral работает через MCP-сервер, который подключает агента к Language Server Protocol Lean 4. Пять фаз — найти пробелы в доказательстве, извлечь подцели, найти леммы в библиотеке, подставить тактику, проверить диагностику — структурированный цикл generate-verify. Три элемента легли на Signum:

1. Верификация до ревью. Lean проверяет не “компилируется ли доказательство”, а “проходит ли оно type-check под ядром”. В Signum аналог — policy scanner: детерминистический grep на дифф, который запускается до LLM-ревьюеров, ловя security и unsafe паттерны при нулевой стоимости токенов.

2. Параллельные попытки. Lean-тул multi_attempt подставляет несколько тактик на одну позицию и сравнивает результирующие goal states. В Signum — параллельные repair lanes: два Engineer-агента в изолированных git worktrees с разными стратегиями фикса.

3. Типизированные диагностики. Lean LSP возвращает структурированные объекты ошибок (файл, строка, сообщение, severity), а не raw text. В Signum механик теперь выдаёт hybrid формат с типизированными findings вместо flat “regressions: true/false”.

Policy Scanner

Самое дешёвое улучшение. Между механиком (lint, typecheck, tests) и мультимодельным код-ревью появился bash-скрипт, который сканирует unified diff на известные опасные паттерны. 195 строк, ноль LLM-токенов.

Сканирует только addition lines. 12 паттернов в трёх категориях:

Security (блокирует пайплайн): eval, subprocess с shell=True, innerHTML, SQL конкатенация, weak crypto
Unsafe (флаг для ревью): TODO/FIXME/HACK, debug-вывод
Dependency (флаг для ревью): новые записи в пакетных менеджерах — но только если файл действительно manifest (package.json, Cargo.toml и т.д.), а не README или тестовая фикстура

Три дизайн-решения пришли из “arbiter panel” — независимого опроса Codex (GPT) и Gemini с последующим сравнением ответов (все три модели — Claude, Codex, Gemini — согласились по каждому):

Fail-closed при отсутствии входных данных. Нет диффа — ошибка, а не “ноль находок”.
Фильтрация по имени файла для dependency паттернов. Без неё любая JSON key-value пара в любом файле даёт false positive.
Curated sinks вместо широких regex. Короткий список опасных вызовов (subprocess.call, child_process.spawn) лучше, чем generic паттерн, который ловит безобидный db.query().

Типизированные диагностики

До этого изменения отчёт механика был flat: lint прошёл или нет, тесты прошли или нет, регрессии да или нет. Engineer в repair mode получал это как blob и угадывал, какой файл и строку чинить.

Теперь механик выдаёт hybrid формат: summary по каждой проверке всегда + per-file findings когда runner поддерживает structured output. У каждого finding поле origin — "structured" для JSON (ruff, eslint), "stable_text" для парсабельного текста (tsc, mypy), "none" для summary only. Гейтинг по summary; findings — подсказки для инженера, не source of truth.

Отступление о ловле багов собственным пайплайном: Claude Opus нашёл критическую проблему на первом же ревью этой фичи. || true после command substitution маскировал exit code, делая возвращаемое значение всегда нулевым. Regression detection была мертва для всех восьми поддерживаемых runners. Один токен. Iterative repair починил за один проход — именно та конвергенция, для которой система создана.

Параллельные repair lanes

Самое сложное изменение. Раньше repair loop был последовательным: одна попытка Engineer, аудит, следующая попытка. Теперь спавнятся два Engineer’а параллельно, каждый в изолированном git worktree:

Lane A: “Почини минимальными точечными изменениями. Только помеченные строки.”
Lane B: “Почини корневую причину. Можно затронуть больше файлов.”

Оба получают один repair brief. После завершения пайплайн прогоняет легковесные проверки (lint, typecheck, тесты, скрытые валидационные сценарии) на каждом lane, скорит их, и отправляет только победителя через полное трёхмодельное ревью. Если у победителя серьёзные находки — ревью получает и второй lane.

Тот же принцип, что у Lean multi_attempt: исследуй пространство решений параллельно, выбери лучшего, верифицируй один раз.

Ещё три изменения

Эти пришли из той же дизайн-сессии, но не связаны с Leanstral напрямую:

Dynamic strategy injection. Contractor теперь классифицирует тип задачи (bugfix, feature, refactor, security) через keyword scan и генерирует strategy hint в контракте. Engineer читает как процесс-гайд: “сначала воспроизведи баг тестом” для багфиксов, “найди все вхождения паттерна, а не только одно” для security фиксов. Информативное — не блокирует пайплайн.

Context retrieval для ревьюеров. Новый pre-review шаг собирает: git history (последний коммит per file), ссылки на issues (парсятся из goal), project.intent.md. Всё инжектится только в Claude ревьюер — Codex и Gemini остаются изолированными (goal + diff only), сохраняя ценность как независимые валидаторы. Цель — снизить false positives, дав семантическому ревьюеру контекст “почему код такой”.

Approval UX. Мелкий фикс: отображение контракта при утверждении теперь в markdown вместо фрагментированного bash-вывода. Goal не обрезается, таблица компактная, warnings сгруппированы.

Что я вынес

Каждая фича прошла через полный пайплайн: дизайн-панель, контракт, реализация, трёхмодельный аудит, iterative repair. Из шести прогонов только один прошёл с первой попытки (самое простое изменение). Остальные потребовали 2-3 итерации.

Паттерн: первый проход Engineer’а проходит все acceptance criteria, но код-ревью находит реальные баги — маскировка exit code, race condition на shared paths, отсутствующие field mappings. Iterative loop чинит их за 1-2 прохода. В этой выборке из шести изменений система вела себя как задумано: не gatekeeping checkpoint, а convergence loop.

Вся сессия: 7 коммитов, ~1900 строк, 5 дизайн-панелей, 15+ раундов мультимодельного ревью. Начало — одна строка из утреннего дайджеста.