flang компилятор доказывает, что программа не зациклится 0.6.2 GitHub

Библиотеку сегодня не выводят из спеки — её пишут агентом, а теорема работает храповиком: 85 680 строк, 1212 теорем, ноль sorry

Единственная свежая новость, которая замысел владельца не опровергает, а переформулирует. Дедуктивный синтез стоит на 75 узлах дерева (synthesis-from-a-spec-hits-75-tree-nodes). Зато агент с прувером уже сделал вещь библиотечного размера — и сделал её не выводом.

lean-zip — проверенная реализация zlib на Lean 4. В README сказано прямо: «Astonishingly, both the implementation, and the verification, are written entirely by loosely supervised AIs» (github). Померено обходом дерева: 165 файлов, 85 680 строк, из них 16 967 — реализация и 51 702 — спецификации и доказательства; 1212 объявлений теорем и лемм; настоящих sorry — ноль. По скорости обгоняет чистый OCaml в 2–4 раза и miniz_oxide на Rust при сравнимом сжатии.

Замковый камень — одна строка:

ZlibDecode.decompressSingle (ZlibEncode.compress data level) maxOutputSize = .ok data

то есть распаковка обращает упаковку для любого входа и любого уровня, проверено ядром.

И вот что здесь главное, потому что мимо этого легко пройти. Эта одна строка не породила 85 680 строк. Агенты писали код и доказательства; теорема работала храповиком — не пускала назад. Отсюда прямая переформулировка замысла:

Не «хранить спеку и выводить пакет», а хранить пакет вместе с доказательством, и позволять агенту переписывать его под неизменной теоремой.

Разница практическая, а не словесная. При выводе спека обязана определять программу — а она не определяет (a-signature-does-not-determine-a-function). При храповике спека обязана лишь отсекать порчу, и этого достаточно: неверный вариант не пройдёт ядро. Ядро flang с нулём аксиом (zero-axioms) — ровно такой храповик, и он у нас уже есть.

Цена храповика видна из тех же чисел: доказательство втрое длиннее кода (51 702 против 16 967). Для сравнения по-человечески: у seL4 отношение около 20:1 и двадцать человеко-лет; у Atmosphere OS — 7,5:1. Три к одному — хорошо, но домен лёгкий, и де Моура говорит это сам: «zlib is a sequential algorithm with a clean RFC specification… The gap between this result and a verified software stack is real» (блог).

И то, что храповик не ловит, названо в самом проекте. Теорема о круговом переводе не доказывает соответствия RFC 1951: «says the encoder and decoder are genuine inverses, not that they were transcribed from the same RFC». Вне охвата остаются разбор архивов, среда исполнения, FFI и расход памяти — «zip bombs» перечислены поимённо. Это ровно наш proven-is-not-correct, и внешний пример на 85 тысяч строк его подтверждает.

Спека — вот где теперь узкое место, и это измерено. Лучшая модель пишет верную спеку в 77,8 % случаев (Verus-SpecGym); на уровне репозитория лучший результат — 20,2 % (CodeSpecBench); в выверенном наборе формальных спек неверными оказались около 28 % (VeriEquivBench); а на пустой спеке модели надёжно жульничают — assume(false), ensures true, и у AlphaVerus это названо «snowballing effect». Иначе говоря: храповик работает ровно настолько, насколько верна теорема, которую в него вставили, — и написать эту теорему пока труднее, чем написать код.

Чем подтверждено. Разбор внешних источников 2026-08-18: клон и подсчёт lean-zip (165 файлов, 85 680 строк, 1212 теорем, sorry только в пояснительных строках), цитаты по ссылкам выше. Считано дважды, порознь: два независимых разбора клонировали хранилище и сошлись во всех шести числах — 165, 85 680, 16 967, 51 702, 1212, ноль. Редкий случай, когда чужое число проверено сверкой, а не доверием, — и потому оно тут стоит наравне со своими. Второй разбор добавил объём работы: около 2900 запросов на слияние, и надзор — это файл PLAN.md, а не человек в цикле.

Чем ограничено.

Связано: synthesis-from-a-spec-hits-75-tree-nodes, a-signature-does-not-determine-a-function, zero-axioms, proven-is-not-correct, derivation-works-where-the-domain-was-narrowed-on-purpose, other-peoples-packages-must-be-stored