Claude створив машинно перевірені докази властивостей безпеки для 239 точок входу fuzz-тестів у 123 open-source бібліотеках. Anthropic і Theorem перевіряли скомпільований код на рівні інструкцій RISC-V.

Дослідження вийшло 22 жовтня 2026 року, за даними Unite.AI. Доведена властивість: відповідні програми завжди завершуються нормально, без помилок безпеки пам’яті й невдалих assert-перевірок, для кожного входу розміром менше 64 МБ — за визначених припущень.

Що саме Claude довів і за яких умов?

Claude довів цю властивість для однопотокових статичних бінарників із фіксованим бюджетом пам’яті на процесорі RISC-V під Linux. За цих припущень доказ охоплює кожну змодельовану відповідь ОС і кожне розташування пам’яті, за даними Anthropic. Автори автоматично перетворили наявні компільовані fuzz-тести на специфікацію з правилом «цей тест завжди проходить».

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

Не всі спроби завершилися доказом: для частини fuzz-тестів Anthropic публікує лише специфікації. Claude написав близько 1 млрд рядків Rocq, із яких перевірку пройшли близько 180 млн — приблизно 18% (180 млн / 1 млрд × 100%). Це частка рядків, а не частка успішно перевірених бібліотек.

Типовий доказ має близько 600 000 рядків, а медіанна довжина бінарників становить 18 000 інструкцій RISC-V. Для точки входу парсера cJSON на 391 рядок вийшов доказ на 630 000 рядків.

Які баги Claude знайшов, поки писав докази?

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

Claude також знайшов логічні баги, які не спричиняють збою. Наприклад, застосунок не завжди дотримувався обмеження на те, які файли може завантажувати. Саме правило «програма не падає» не гарантує правильності такого обмеження.

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

Чим докази доповнюють тести?

Експеримент з інтерпретатором Python показав, що внесені помилки можуть пройти випадкові тести, але порушити формальний доказ. Claude написав на Rust інтерпретатор для значної підмножини Python і за допомогою Verus довів умовну властивість: якщо інтерпретатор повертає результат, той відповідає формальній семантиці CPython, описаній в академічній роботі.

Тестування на 1,7 млн випадково згенерованих програм показало збіг поведінки з CPython у 99,95% випадків. Із семи навмисно внесених багів п’ять залишилися непоміченими під час випадкового тестування, а всі сім порушили доказ.

Як моделі й спільна робота агентів впливають на витрати?

Opus 5.5 потребував приблизно на 40% менше токенів, ніж Opus 5, щоб довести половину завдань у невеликому тестовому наборі. Anthropic підготувала 36 зменшених завдань на основі реальних точок входу OSS-Fuzz: програми містили 283–2 491 інструкцію, а розмір входу обмежили 64 байтами. Цей результат сам по собі не встановлює такої самої економії для великих бінарників.

Агенти, яким дозволили копіювати докази один в одного у спільному робочому просторі, витратили на 17% менше токенів, ніж агенти, які працювали поодинці. Деякі впоралися із завданнями після невдалих самостійних спроб. Подібне повторне використання Anthropic спостерігала й у великому проєкті: значна частина доказів охоплює спільний C-рантайм та ініціалізацію AddressSanitizer.

Як скористатися результатами дослідження?

Theorem пропонує запустити той самий пайплайн для інших open-source проєктів і публікує Claude skill, який допомагає розпочати верифікацію власного коду.

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