Claude доказал свойства безопасности для 123 открытых библиотек
Claude написал 180 млн строк доказательств для 239 точек входа в 123 библиотеках.
Доказательства проверяли отсутствие падений для любого входа меньше 64 МБ при заданной модели исполнения.
Проверка шла на уровне кода RISC-V: Claude писал доказательства, а Rocq проверял их корректность.
Работа нашла сотни ошибок, включая выход за границы памяти на редком входе размером около 20 МБ.
Почему важно
Формальная верификация может перейти от многолетней экспертной работы к обычному этапу разработки, но гарантии останутся ограничены заявленными свойствами и условиями.