Формальная верификация кода: что показал баг в Lean 4

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

13 апреля 2026 года автор Kiran Codes опубликовал разбор эксперимента с lean-zip - реализацией zlib на Lean. Он направил Claude на кодовую базу, подключил AFL++, AddressSanitizer, UndefinedBehaviorSanitizer, Valgrind и статические анализаторы. Результат: 105,823,818 fuzzing-запусков не нашли ошибок памяти в проверенном прикладном коде на Lean, зато нашли переполнение буфера в куче (heap buffer overflow) в среде выполнения Lean 4 и отказ в обслуживании в непроверенном участке парсера ZIP.

Главный вывод не в том, что «формальная верификация не работает». Наоборот: она показала сильный результат внутри доказанной границы. Но граница оказалась важнее рекламного тезиса. Если программа зависит от среды выполнения, парсера, файлового ввода и C++-кода под капотом, вся эта часть становится доверенной базой вычислений. И именно там ИИ с фаззером начал находить проблемы.

Проверенный слой Lean и zlib

lean-zip - порт zlib на Lean с доказанными свойствами сжатия и распаковки. В исходном материале говорится о реализации, для которой верно такое утверждение: для байтового массива меньше 1 ГБ результат распаковки после сжатия должен совпадать с исходными данными. Это важный класс свойства: не «код выглядит правильно», а машинно проверяемое утверждение о поведении функций.

Чтобы не подсказывать агенту, что код «доказан», автор эксперимента убрал теоремы, спецификации, Markdown-документацию и C FFI-привязки к zlib. Остались нативные Lean-определения для DEFLATE, gzip, ZIP archive handling и tar. Идея была простая: если в этой части найдётся ошибка памяти, это будет ударом по самому проверенному Lean-коду.

Такого удара не случилось. По данным исходного разбора, проверенный прикладной код прошёл ночь фаззинга без переполнений буфера в куче, use-after-free, stack buffer overflow, неопределённого поведения и выходов за границы массивов в сгенерированном C-коде. Это сильный аргумент в пользу формальной верификации, а не против неё.

Результаты ИИ-фаззинга

Эксперимент был не про «Claude сам нашёл баг». Это связка ИИ, фаззинга и классических инструментов проверки. Claude помогал работать с кодовой базой, собирать тестовые обвязки и запускать проверки. AFL++ генерировал входные данные. ASan, UBSan и Valgrind ловили ошибки памяти и неопределённое поведение.

За ночь Claude запустил 16 параллельных фаззеров по шести поверхностям атаки: ZIP extract, gzip decompress, raw DEFLATE inflate, tar extract, tar.gz и compression. Всего получилось 105,823,818 запусков, 359 seed-файлов, около 19 часов работы, 4 входа, вызывавших сбой, и 1 уязвимость памяти.

Наиболее серьёзная находка оказалась не в коде lean-zip, а в среде выполнения Lean 4. Уязвимая функция lean_alloc_sarray выделяет память для скалярных массивов вроде ByteArray. При очень большом размере вычисление объёма памяти могло переполниться, после чего среда выполнения выделяла маленький буфер, но пыталась читать в него огромный объём данных.

Триггер шёл через lean_io_prim_handle_read, C-функцию под IO.FS.Handle.read. В исходном разборе приводится пример ZIP64-файла размером 156 байт, который объявляет compressedSize как 0xFFFFFFFFFFFFFFFF. Этого достаточно, чтобы довести среду выполнения до переполнения буфера в куче.

Граница формальной верификации

Формальная верификация кода проверяет ровно те свойства, которые были сформулированы, и ровно тот слой, к которому эти свойства применили. В lean-zip доказательства покрывали цепочку сжатия и распаковки: DEFLATE, Huffman, CRC32 и корректность полного цикла. Они не доказывали корректность всего, что находится рядом.

Отказ в обслуживании нашёлся в Archive.lean - коде, который читает ZIP-заголовки и извлекает файлы. Этот участок, по словам автора эксперимента, не имел теорем даже в исходной кодовой базе. Поле compressedSize читалось из недоверенного заголовка и передавалось в выделение памяти без проверки на реальный размер файла. Для формальной верификации это не «пропущенный баг», а незаданная спецификация.

С переполнением буфера в среде выполнения история глубже. Runtime - часть доверенной базы вычислений. Любое доказательство на Lean предполагает, что ядро, среда выполнения, компилятор, ввод-вывод и низкоуровневые примитивы ведут себя корректно. Если ошибка находится там, доказанный прикладной код может оставаться корректным, но программа всё равно падает или нарушает безопасность на нижнем уровне.

Lean 4 быстро получил исправление

По состоянию на 15 апреля 2026 года факт исправления подтверждается в репозитории Lean 4. GitHub issue #13388 описывает переполнение буфера в lean_io_prim_handle_read. Pull request #13392 с заголовком fix: file read buffer overflow был принят в master 13 апреля 2026 года.

В описании PR сказано, что исправление закрывает heap buffer overflow, вызванный integer overflow при вычислении размера выделяемой памяти. Также в релевантные пути выделения памяти добавили проверяемую арифметику: будущие переполнения должны превращаться в безопасное аварийное завершение или ошибку out of memory, а не в запись за пределы буфера.

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

Роль ИИ в поиске бага

ИИ в этом кейсе не заменил исследователя и не отменил классические инструменты безопасности. Он ускорил перебор рабочих гипотез, настройку окружения и запуск проверок. Главную проверку выполняли AFL++, ASan, UBSan, Valgrind, cppcheck и flawfinder. Claude был агентом-исполнителем в этом контуре, а не самостоятельным источником истины.

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

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

Практические выводы для разработчиков

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

Второй вывод: доверенная база вычислений должна быть отдельным объектом внимания. Среду выполнения, компилятор, FFI-слой, системные вызовы и библиотеки ввода-вывода надо фаззить не меньше, чем прикладной код. Иначе вся уверенность верхнего уровня упирается в предположение, которое никто давно не проверял.

Третий вывод: ИИ-ассистентам в разработке нужны правила ответственности. Как мы уже писали в материале про правила для ИИ-кода в Linux kernel, модель может помогать писать и проверять код, но ответственность остаётся у человека и команды. В безопасности это особенно жёсткое требование: любой найденный сбой должен быть воспроизводим, минимизирован и проверен без веры в ответ модели.

Итог

Кейс Lean 4 полезен именно тем, что он не укладывается в простую лозунговую формулу. Формальная верификация не провалилась: проверенный прикладной код выдержал 105,823,818 fuzzing-запусков без ошибок памяти. ИИ-фаззинг тоже не оказался пустым шумом: он нашёл реальное переполнение буфера в среде выполнения Lean и проблему отказа в обслуживании в непроверенном парсере.

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