Компания Аnthropic представила результаты экспериментов по использованию AI-моделей для формальной верификации надёжности и безопасности уже существующих проектов. В ходе эксперимента при помощи AI-моделей для 123 открытых библиотек, протестированных в инфраструктуре OSS Fuzz, были сгенерированы математические доказательства отсутствия ошибок при работе с памятью.

Проверка проводилась на уровне скомпилированного ассемблерного кода для архитектуры RISC-V. Общий объём сгенерированных доказательств составил около 180 миллионов строк кода для системы верификации Rocq Prover (около 600 тысяч строк на бинарный файл с 18 тысячами RISC-V инструкций). Доказательства формировались через автоматическое преобразование существующих fuzzing-тестов в формальные спецификации. AI-модель Claude доказывала, что при любых входных данных объёмом до 64 МБ в программе не возникает сбоев.

В процессе построения доказательств AI-модель смогла выявить и подготовить исправления для сотен ошибок, ранее не замеченных при fuzzing-тестировании. Среди прочего, были выявлены уязвимости (например, CVE-2026-56132 в libexpat), приводящие к переполнению буфера при обработке определённых входных данных, а также логические ошибки. Помимо этого, AI-модель была использована для доказательства соответствия реализации алгоритма zlib в ядре Linux спецификации RFC 1950.

Также на языке Rust был сгенерирован интерпретатор для подмножества языка Python, для которого при помощи инструментария Verus подготовлено формальное доказательство соответствия семантике CPython. Для сравнения поведения с CPython было выполнено более 1.7 миллиона случайно сгенерированных Python-программ. В 99.95% случаев результаты выполнения этих программ в новой реализации и в CPython совпали, а выявленные расхождения оказались известными граничными случаями.