Формальная верификация годами оставалась штукой для самолёта и ядра вроде seL4: два года писать код, двадцать — доказательства. Frontier Red Team Anthropic вместе с Theorem показывает другой масштаб. Claude доказал свойства безопасности на уровне инструкций RISC-V больше чем в ста открытых библиотеках. Пост — от 22 октября.
Что именно доказали
Спецификацию взяли из уже существующих фазз-тестов OSS-Fuzz: «эта точка входа не падает». Её перевели на исполняемый RISC-V и модель Linux. Claude закрыл 239 точек в 123 библиотеках: нормальный выход, без ошибок памяти и сорванных assert, на любом входе меньше 64 МБ — при однопоточном статическом бинарнике, фиксированной памяти, RISC-V и Linux. Доказательств около 180 млн строк Rocq, типичный текст — сотни тысяч строк на медиану в 18 тысяч инструкций.
Человеку не нужно читать этот объём. Доверять приходится модели RISC-V и Linux, формулировке теоремы и ядру Rocq. Остальные баги либо вне этих рамок, либо в доверенных кусках. По дороге модель находила дефекты, которые не всплывали на триллионах прогонов тестов — и чинила их, прежде чем дописать доказательство.
Как смотреть
Это не аттестация «библиотека безопасна». Это доказательство узкого свойства на узкой машине. Имеет смысл мейнтейнерам C/C++ в OSS-Fuzz, которым Theorem обещает тот же пайп и навык для Claude. Не имеет смысла как замена ревью и патч-менеджменту. Смотреть, сколько чужих команд повторит проверку опубликованного подмножества доказательств, а не слоган «багов больше нет».
