Формальная верификация — математическая проверка того, соответствует ли код заданным свойствам. Исследователи Google DeepMind использовали ИИ-агентов и инструмент AlphaProof Code; о работе сообщил WIRED со ссылкой на исследователей. Проект был демонстрацией возможностей инструмента.
Проверка охватила протокол, но не всё мобильное приложение Signal. При этом AlphaProof Code выявил известные уязвимости в старых версиях протокола и показал, что они не проходят формальную проверку.
Исследователи опубликовали спецификацию и доказательство, подготовленные для анализа Signal. По словам технического директора Signal Эрена Кретa, прежние проверки охватывали меньшие фрагменты кода, а новый подход позволяет расширить охват. ИИ-агенты выполняли и корректировали работу на большинстве этапов, но в ключевых точках требовалась проверка людей.
