Anthropic заявила, что Claude формально проверил код 123 open-source библиотек

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

Совместно с Theorem исследователи превратили тесты Google OSS-Fuzz в формальные спецификации, а Claude написал доказательства, которые проверяло ядро Rocq. За несколько недель система исправляла найденные ошибки и доказала отсутствие сбоев для любых входных данных объемом до 64 МБ в 239 точках входа. Общий объем доказательств составил около 180 млн строк.

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

Ограничения существенны: доказательства относятся к однопоточным статическим бинарным файлам RISC-V в заданной модели Linux, а не к типичным системам x86 или ARM. Они подтверждают только свойства из спецификации и не охватывают все точки входа и классы ошибок. Но работа показывает, что AI способен заметно снизить объем экспертного труда, из-за которого формальная верификация раньше была слишком дорогой для обычного ПО.