Claude написал формальные доказательства для 123 библиотек

Вместе с Theorem Claude доказал, что 239 точек входа фаззинг-тестов в 123 библиотеках из OSS-Fuzz не падают ни на одном входе меньше 64 МБ. Доказательства написаны поверх скомпилированного машинного кода RISC-V, а не поверх исходников, рассказала 22 октября команда Frontier Red Team в блоге Anthropic.

Работа заняла несколько недель. Для масштаба Anthropic приводит ядро seL4: написать его заняло два человеко-года, а формально верифицировать 20. Поэтому формальную верификацию до сих пор применяли там, где без неё нельзя, вроде авионики Airbus. Мотивацию компания объясняет так: в ядре Linux, одном из самых протестированных проектов в мире, недавно раскрыли больше 1 000 уязвимостей, а модели всё лучше собирают из безобидных на вид багов рабочие эксплойты.

Как тест превращается в теорему

Главная проблема формальной верификации в спецификации: надо сначала строго записать, что значит «корректно». Для PNG-декодера ответ даёт RFC 2083. Что считать корректным текстовым редактором или браузером, сформулировать уже почти невозможно.

Anthropic обошла это так: спецификацию собрали из тестов, которые разработчики уже написали. Фаззинг-тест задаёт точку входа в код, а фаззер забрасывает её миллионами полуслучайных мутированных входов в поисках падения. OSS-Fuzz собирает C и C++ с AddressSanitizer, инструментом, который роняет программу при любом неправильном обращении к памяти. Так что падение здесь означает либо ошибку памяти, либо сработавший assert. Но фаззинг остаётся перебором и не гарантирует, что пройдены все пути исполнения.

Дальше всё механично. Библиотеку вместе с тестом компилируют в исполняемый файл под RISC-V. Этот файл, формальные модели RISC-V и Linux-процесса от Theorem и требование «не падать» дают теорему, которую надо доказать. Доказательство пишет Claude, ядро Rocq сверяет его со спецификацией. Утверждение покрывает любой вход меньше 64 МБ, любой смоделированный ответ операционной системы и любую раскладку памяти. Фаззеры обычно ограничивают вход 1 МБ. Если теорема доказана, фаззинг этой точки входа на RISC-V больше ничего не найдёт.

180 миллионов строк, которые не нужно читать

Всего доказательства заняли около 180 миллионов строк на Rocq. Типичное доказательство тянет примерно на 600 000 строк, хотя медианный бинарник в нём всего 18 000 инструкций RISC-V: грубо три десятка строк доказательства на каждую инструкцию. Для сравнения, в сентябре Nature сообщал о проверенном компьютером доказательстве Великой теоремы Ферма длиной 13 миллионов строк, которое прототип Claude написал за 11 дней.

Читать этот объём людям не нужно, соответствие спецификации гарантирует Rocq. Довериться приходится всего трём вещам: формальным моделям RISC-V и Linux-процессов, точным формулировкам доказанных теорем и самой проверяющей программе Rocq. Этот список не растёт с числом проверенных проектов, и Anthropic считает, что вычистить его гораздо реальнее, чем отлаживать каждую строку покрытого кода.

Баги в этих библиотеках при этом остаются возможны. Они могут сидеть в доверенных компонентах или за пределами доказанного. А доказанное держится на допущениях: однопоточный статический бинарник с фиксированным бюджетом памяти на процессоре RISC-V под Linux. Чтобы расширить охват, по словам Anthropic, хватит стандартизировать семантику других архитектур и других процессов ОС, и это «вполне достижимо».

Баги по дороге

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

В той же линии работ Anthropic ищет уязвимости и обычным способом: в октябре первые прогоны OSS Scanner дали 77 критических находок. Верификация отвечает на другой вопрос: что ещё осталось найти.

Что можно взять себе

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

Кроме OSS-Fuzz, команда пробовала другие методы: оценивала безопасность zlib и доказывала поведенческую эквивалентность интерпретатора Python, написанного на Rust. По мнению Anthropic, стоимость доказательств будет падать вместе с ростом моделей, а повторное использование доказательств между кодовыми базами её ещё и распределит. Компания призывает разработчиков пробовать формальную верификацию с LLM, «особенно тех, кто уже пытался с менее способными моделями и решил, что это не работает».