Claude доказал отсутствие падений в 123 библиотеках с открытым кодом
Claude доказал отсутствие падений в 123 библиотеках с открытым кодом Anthropic и компания Theorem с помощью Claude формально доказали, что 239 точек входа в 123 библиотеках из OSS-Fuzz не падают ни на одном входе размером до 64 МБ. Доказательства проверяют не исходный код, а скомпилированные RISC-V бинарники. Всего получилось около 180 млн строк в Rocq (бывший Coq), типичное доказательство — порядка 600 тыс. строк. Вручную читать их не нужно: корректность подтверждает проверяющее ядро Rocq. Работа заняла несколько недель. По ходу Claude нашёл и исправил баги, которые годами не замечали, несмотря на триллионы прогонов фаззинга. Есть ограничения: гарантии действуют для однопоточного статического бинарника на RISC-V под Linux и только для заданных свойств. Перенос на x86 и ARM авторы считают достижимым. Источники: https://www.anthropic.com/research/formal-verification #AI #Anthropic #Claude #Безопасность #ФормальнаяВерификация