Anthropic заявляє, що Claude довів властивості безпеки 123 бібліотек

22 жовтня 2026 року Anthropic опублікувала дослідження, у якому повідомила, що Claude створив формальні доведення властивостей безпеки, перевірені машиною на рівні асемблерного коду RISC-V, для 239 точок входу fuzz-тестів у 123 бібліотеках із відкритим кодом у співпраці з Theorem.

За даними Anthropic, Claude виправив знайдені помилки, а потім довів, що програми завжди завершуватимуться нормально, не спричиняючи помилок безпеки пам’яті чи невдалих перевірок тверджень, для будь-яких вхідних даних обсягом до 64 МБ і за будь-якої змодельованої відповіді операційної системи Linux та будь-якого розташування пам’яті. Доведення ґрунтуються на припущенні, що програма працює як статичний бінарний файл в однопотоковому режимі з фіксованим обсягом пам’яті на процесорі RISC-V під керуванням Linux. В Anthropic повідомили, що доведення налічують близько 180 мільйонів рядків Rocq, а типове доведення складається приблизно з 600 000 рядків і охоплює бінарні файли медіанної довжини — 18 000 інструкцій RISC-V. Компанія заявила, що, наскільки їй відомо, це перша масштабна спроба застосувати ШІ для формальної верифікації готового програмного забезпечення на рівні асемблерного коду.

Частину доведень разом із семантикою RISC-V та операційної системи, що лежить у їхній основі, публікують на GitHub. В Anthropic повідомили, що також випускають створені для проєкту довірені компоненти, які ще не є загальнодоступними, повні доведення для fuzz-тестів, що не потребували виправлень, а також специфікації для fuzz-тестів, які не вдалося довести. Доведення, що можуть розкрити невиправлену помилку, компанія не публікуватиме.

Перетворення fuzz-тестів на формальні доведення

Цей підхід перетворює наявний компільований fuzz-тест кожної бібліотеки на формальну специфікацію, що кодує одне правило: тест не завершується аварійно на жодних вхідних даних обсягом до 64 МБ. Специфікацію визначено для скомпільованих інструкцій RISC-V із використанням формальної семантики набору інструкцій RISC-V і процесів Linux від Theorem, а перевірник доведень Rocq перевіряє кожне завершене доведення на відповідність специфікації. За словами Anthropic, це означає, що розробникам потрібно довіряти лише трьом компонентам: формальним моделям RISC-V і процесів Linux, точним формулюванням теорем і самому перевірнику Rocq.

В Anthropic повідомили, що застосували цей процес до сотень проєктів у межах ініціативи Google OSS-Fuzz, яка забезпечує безперервне fuzz-тестування проєктів із відкритим кодом, що відповідають вимогам, і автоматично інструментує програми мовами C та C++ за допомогою AddressSanitizer — інструмента, який аварійно завершує програму щоразу, коли відбувається неналежне звернення до пам’яті. У додатку від 22 жовтня 2026 року наведено повне доведення теореми: для всіх вхідних даних обсягом до 64 MiB і за будь-якого розташування пам’яті ані бінарний файл з інструментуванням ASan, ані звичайний бінарний файл не зазнають збою, не переривають роботу аварійно й не демонструють незмодельованої поведінки; обидва файли створюють однакові журнали операцій читання й запису, однаково завершують роботу та залишають файлову систему в однаковому кінцевому стані.

У додатку зазначено, що під час цієї роботи Claude написав близько одного мільярда рядків Rocq, з яких приблизно 180 мільйонів пройшли перевірку доведень. Для точки входу парсера cJSON обсягом 391 рядок було створено доведення на 630 000 рядків, а для fftw3, до якої підключено 51 000 рядків коду, — доведення на 480 000 рядків. Оскільки Claude міг виправляти код до завершення доведення, Anthropic запровадила штрафи за виправлення, надавала додаткову винагороду за доведення того, які вхідні дані змінює виправлення, а також реєструвала й перевіряла всі виправлення, щоб запобігти маніпулюванню системою винагород.

Помилки, виявлені під час спроб доведення

В Anthropic повідомляють, що спроби доведення виявили сотні помилок, багато з яких fuzz-тест навряд чи знайшов би. Доводячи властивості точки входу однієї з бібліотек, Claude виявив переповнення лічильника вниз у декомпресорі, що спричиняло запис за межами буфера, але лише для вхідних даних обсягом близько 20 МБ з одним рідкісним специфічним розташуванням. Серед інших знахідок — читання за межами буфера в декодері зображень, для якого були потрібні вхідні дані обсягом 64 МБ і понад 2 ГБ пам’яті; читання за межами буфера, можливе лише за певної послідовності викликів через два дескриптори того самого файлу; а також повторне виявлення CVE-2026-56132 у libexpat, для якого потрібні були глибоко вкладені вхідні дані.

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

Додаткові експерименти та висновки щодо ефективності

Окрім OSS-Fuzz, Anthropic попросила Claude написати формальну специфікацію RFC 1950 — технічного документа, що визначає формат стиснення zlib, — а потім довести, що реалізація zlib у ядрі Linux правильно її реалізує. Claude безпосередньо довів властивості бінарного файлу, скомпільованого для x86, використавши формальну семантику набору інструкцій x86, створену Claude. За словами Anthropic, компанія повторила цей процес для ще пів дюжини інших бібліотек, які широко використовуються, і виявила незначні, непридатні для експлуатації помилки в крайових випадках, про які повідомляють супровідникам проєктів. Компанія також повідомила, що під час створення семантики x86 було виявлено сотні помилок в офіційній довідковій документації та меншу кількість помилок у самому апаратному забезпеченні, а покрокове виконання семантики дає змогу завантажити користувацьке середовище Ubuntu на ядрі Linux.

В іншому експерименті Claude створив на Rust інтерпретатор для значної підмножини Python і за допомогою інструмента верифікації Verus довів, що той відповідає семантиці CPython, описаній в академічній статті. У технічному додатку зазначено, що було доведено правильність усіх 17 рівнів інтерпретатора, причому теорема стверджує: «Щоразу, коли інтерпретатор повертає результат, цей результат відповідає тому, який приписує формальна семантика». Anthropic повідомила, що емпіричне тестування 1,7 мільйона випадково згенерованих програм на Python виявило ідентичну поведінку з CPython у 99,95% тестів; із семи навмисно внесених помилок п’ять не виявилися під час випадкового тестування, тоді як усі сім порушили доведення.

Щоб оцінити ефективність, Anthropic створила 36 невеликих завдань із верифікації, скоротивши реальні точки входу OSS-Fuzz. У результаті отримали програми з 283–2 491 інструкцією, обмеживши вхідні дані 64 байтами й замінивши AddressSanitizer середовищем виконання «mini-ASan» обсягом близько 100 інструкцій. За даними Anthropic, Opus 5.5 доводить правильність половини завдань, використовуючи приблизно на 40% менше токенів, ніж Opus 5. Anthropic також повідомляє, що агенти, яким дозволили копіювати докази одне одного у спільному робочому середовищі, потребували на 17% менше токенів, ніж агенти, які працювали самостійно; деякі з них досягли успіху після попередньої невдачі в самостійній роботі, а агенти, що працювали самостійно, не змогли завершити два докази. Компанія заявила, що такий самий ефект повторного використання проявився у великому масштабі під час роботи з OSS-Fuzz: команди агентів копіювали готові докази й адаптували їх, оскільки значна частина кожного доказу охоплює спільний код ініціалізації середовища виконання C та AddressSanitizer.

Заявлені обмеження та програма OSS Verify

Anthropic зазначає, що наявність доказів не означає, ніби в бібліотеках немає помилок: ті, що залишилися, можуть міститися у довірених компонентах або виходити за межі охоплення доказів. Докази стосуються однопотокових статичних двійкових файлів RISC-V, скомпонованих із musl libc, тоді як більшість користувачів запускають ці бібліотеки на x86 або ARM і динамічно компонують їх із glibc; крім того, AddressSanitizer виявляє не всі помилки безпеки пам’яті. Компанія заявила, що очікує: з удосконаленням моделей ці обмеження стане можливо подолати.

Theorem безкоштовно пропонує той самий конвеєр проєктам із відкритим вихідним кодом, які відповідають критеріям, у межах своєї програми OSS Verify. Щоб долучитися, потрібно надіслати запит на внесення змін із файлами project.yaml, Dockerfile і build.sh до репозиторію програми. Theorem повідомляє, що перевіряє проєкти за принципами, подібними до OSS-Fuzz, надаючи пріоритет критично важливій інфраструктурі, якою широко користуються. За даними Theorem, супровідники отримують доказ у Rocq, перевірений ядром Rocq, що жодна ціль фаззингу не завершується аварійно на будь-яких вхідних даних обсягом до 64 MiB; про виявлені під час доведення помилки конфіденційно повідомляють супровідникам електронною поштою, без установленого кінцевого строку для оприлюднення, а на підготовку доказів може піти кілька днів. У дорожній карті Theorem заплановано верифікувати всю екосистему Nix, включно з критично важливою інфраструктурою, як-от glibc, OpenSSL і cURL.