Компания А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 совпали, а выявленные расхождения оказались известными граничными случаями.

Проведённая формальная верификация гарантирует соответствие спецификации, но полностью не исключает возникновение проблем с безопасностью, так как остаются неформализованными риски, вызванные проблемами с многопоточностью, динамическим связыванием и аномальным поведением реального оборудования. Ключевым преимуществом предложенного подхода является работа непосредственно с бинарными файлами, что позволяет обойтись без необходимости переписывания существующего кода на формально верифицируемых языках.