Anthropic: Claude написал машинно проверяемые доказательства для скомпилированного кода 123 open-source-библиотек
Команда Frontier Red Team компании Anthropic и фирма Theorem с помощью Claude доказали, что 239 точек входа фазз-тестов в 123 библиотеках OSS-Fuzz не могут «упасть» на входных данных до 64 МБ в смоделированной среде. Работа выявила ошибки, которые годы фаззинга пропускали, но у доказательств есть важные оговорки.
Anthropic опубликовала исследование, в котором её Frontier Red Team вместе с компанией Theorem, специализирующейся на формальных методах, с помощью Claude формально верифицировала свойства безопасности 123 открытых библиотек из проекта Google OSS-Fuzz — всего 239 точек входа фазз-тестов. Важно, что доказательства относятся к скомпилированному машинному коду RISC-V, а не к исходникам.
Как это работало
Каждый существующий фазз-тест превратили в формальную спецификацию: скомпилированный тест не должен аварийно завершаться (например, из-за ошибки памяти, пойманной AddressSanitizer, или проваленного assert) ни на каких входных данных меньше 64 МБ в смоделированной среде. Theorem предоставила формальные модели набора команд RISC-V и поведения процессов Linux, Claude писал доказательства, а их проверял Rocq. По данным DevOps.com, за несколько недель Claude сгенерировал около 180 млн строк доказательств.
Ошибки, пропущенные фаззингом
Claude разрешалось исправлять найденные ошибки, и их обнаружились сотни. Среди примеров — переполнение счётчика «вниз» в декомпрессоре, приводившее к записи за границы буфера только на входах около 20 МБ, и ошибка чтения в декодере изображений, требовавшая входа в 64 МБ. Anthropic говорит, что штрафовала крупные патчи и проверяла их, чтобы модель не могла просто переписать программу так, чтобы она «никогда не падала».
Ограничения
Anthropic подчёркивает: «формально верифицировано» не значит «без ошибок». Доказательства предполагают однопоточные статически слинкованные бинарники RISC-V с musl libc, тогда как большая часть Linux-софта работает на x86 или ARM с glibc; AddressSanitizer ловит не все ошибки памяти, и проверены не все точки входа. Ещё одно ограничение — стоимость: доказательства могут требовать сотен миллионов токенов. Данные о росте эффективности новых моделей Claude — собственные бенчмарки Anthropic. Часть доказательств опубликована на GitHub.