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