Claude доказал надёжность кода 123 открытых библиотек и нашёл сотни багов

Формальная верификация — это способ доказать надёжность программы так же строго, как доказывают теорему в математике. Обычные тесты проверяют программу на тысячах примеров. Доказательство покрывает все возможные входные данные в заданных рамках. Метод давно известен, но для настоящих программ он требует годы работы специалистов. Anthropic называет новую работу первой масштабной попыткой поручить это ИИ на реальном производственном коде.

Claude проверял библиотеки, на которых держится интернет

Команда Frontier Red Team, отдел Anthropic по проверке опасных возможностей моделей, взяла библиотеки из OSS-Fuzz. Это проект Google, который постоянно гоняет популярный открытый код через случайные входные данные в поисках сбоев. В списке программы для сжатия, разбора изображений, XML и других форматов. Такие библиотеки работают внутри браузеров, серверов и приложений.

Задача для Claude звучала так. Нужно доказать, что скомпилированная программа не упадёт на любом входе размером до 64 МБ. Проверке подлежал машинный код, который реально исполняет процессор. Доказательства Claude писал на языке Rocq. Это программа-проверщик, которая принимает доказательство, только если в нём нет ни одного пробела.

Масштаб работы такой:

• Библиотеки → 123 из OSS-Fuzz
• Точки входа → 239, то есть места, через которые программа принимает данные
• Объём доказательств → около 180 млн строк, типичное доказательство около 600 тыс. строк
• Срок → несколько недель

Сотни багов нашлись по дороге к доказательству

Доказать надёжность кода с ошибкой нельзя. Поэтому каждый раз, когда доказательство не сходилось, Claude находил реальную проблему. Так всплыли сотни багов. Точного числа Anthropic не называет. Среди примеров переполнение счётчика в распаковщике данных и чтение за пределами памяти в декодере изображений. Ещё Claude заново нашёл уже известную уязвимость в libexpat, библиотеке для разбора XML.

Часть доказательств Anthropic выложила в открытый доступ вместе с моделью процессора и операционной системы, на которую они опираются. Доказательства, которые могут указать на ещё не исправленные ошибки, компания придержала. Theorem отдельно опубликовала навык для Claude, с которым можно проверять другие проекты.

«Верифицировано» у Claude не значит «без ошибок»

Авторы сами перечисляют ограничения работы. Доказательство верно, только если верны исходные описания и модель машины. Проверялись программы под процессорную архитектуру RISC-V. Большинство людей запускает те же библиотеки на x86 и ARM с другими системными компонентами. Доказана только устойчивость отдельных точек входа, а не всей библиотеки целиком. Ошибки при неправильном вызове библиотеки из чужой программы тоже остаются за рамками.

Цена тоже не мелкая. Одно доказательство может съесть сотни миллионов токенов, а в долларах Anthropic расходы не раскрывает. Для одиночного разработчика метод пока недоступен, для крупных проектов уже реален.

Вторая работа Anthropic за неделю о безопасности открытого кода

Двумя днями раньше, 20 октября, та же команда Anthropic показала другой подход. Claude разобрал 25 открытых проектов, больше 5 млн строк кода, и нашёл 493 проблемы в настройках. 94 сочетания параметров молча отключали защиту. В OpenSSH около 4500 строк экспериментального кода были доступны клиентам без входа в систему. Исправление вошло в OpenSSH 10.6.

Вместе с недавней историей о дыре в PHP, найденной с помощью ИИ, картина складывается однозначная. Модели находят ошибки быстрее, чем их успевают исправлять. Формальная верификация даёт защитникам ответный инструмент. Найденную ошибку исправляют, и потом доказательство подтверждает, что в проверенном месте её больше нет.

Что брать на заметку владельцам сайтов и разработчикам

Библиотеки из OSS-Fuzz стоят внутри CMS, веб-серверов и обработчиков картинок. Исправления по найденным багам выходят в обычных обновлениях. Самое полезное прямо сейчас — не откладывать обновление зависимостей и серверного ПО, особенно библиотек для изображений и XML.

Главная проверочная точка для метода — первый крупный проект, который сделает формальную верификацию с Claude частью обычного выпуска версий. Пока это исследование одной лаборатории. До рабочего процесса отрасли метод ещё не дорос.