DeepMind за четыре недели формально верифицировала ключевые гарантии протокола Signal

Тесты показывают, что код работает на тех входных данных, которые вы догадались проверить. Формальная верификация отвечает на другой вопрос: можно ли математически доказать, что код ведёт себя правильно на любых данных. Инженеры давно называют это святым граалем безопасности, но на практике доказательства писали вручную, и на это уходили месяцы и годы. Теперь DeepMind показала, что значительную часть этой работы можно отдать агенту.

Что именно сделали

Исследователи Google DeepMind с помощью нового фреймворка AlphaProof Code формально верифицировали ряд ключевых криптографических гарантий протокола Signal. На этом протоколе держится шифрование в приложении Signal, Google Messages и WhatsApp. Проект был proof-of-concept и занял всего четыре недели.

Чтобы оценить скорость, нужно понимать, из чего состоит работа. Сначала люди описывают, какими свойствами должен обладать код. Затем это описание превращают в формулы. И только потом пишут само доказательство. Агентный ИИ сильно сокращает время именно на последнем, самом трудоёмком этапе.

Есть и проверка на практике. Новых уязвимостей в изученных частях протокола система не обнаружила. Зато на старых версиях Signal с давно исправленными багами AlphaProof Code эти проблемы нашёл и показал, что такой код формально верифицировать нельзя. Для инструмента проверки это важный тест: он не просто подтверждает «всё хорошо», а действительно ломается там, где код ошибочен.

Стартовали исследователи не с нуля. Signal Foundation раньше уже делала формальную верификацию меньших фрагментов кода, и это дало DeepMind фору. Технический директор Signal Эрен Крет говорит, что подход DeepMind позволяет заметно расширить охват проверки, и это добавляет уверенности в приватности реализации.

Почему это важно для практиков

Главный сдвиг здесь в стоимости. Формальная верификация была недоступна большинству команд не потому, что никто не понимал её пользу, а потому, что доказательства обходились слишком дорого по человеческому времени. Если агенты берут на себя рутину, круг кода, который имеет смысл доказывать, расширяется. Пушмит Кохли из Google Cloud и DeepMind прямо говорит о банках и других компаниях, которые смогут заявить: «я могу доказать эти свойства».

Самое здравое в проекте — организация работы. Агенты вносят вклад и самокорректируются почти на каждом шаге, но в ключевых точках запрашивают проверку человека. Исследователь DeepMind Сварат Чаудхури объясняет, почему: нужен не «вайб-мир», где ИИ сам генерирует цели, сам пишет доказательства и по сути сдаёт тесты, которые написал сам. Нужна золотая середина.

Для разработчика отсюда следует простая вещь. Доказательство ценно ровно настолько, насколько верна спецификация, то есть описание того, что считается правильным поведением. Если и спецификацию, и доказательство пишет модель, вы получаете красивую бумагу без гарантий. Ответственность за формулировку требований остаётся за человеком.

Ограничения и что делать

Стоит трезво смотреть на масштаб. Целое мобильное приложение Signal не верифицировали, только отдельные части протокола. Чаудхури сам признаёт, что до проверки всего софта в мире ещё очень далеко. Новых багов система не нашла, так что пока это скорее подтверждение чужой работы, чем открытие.

Главный вопрос индустрии — экономика. DeepMind делала анализ бесплатно как исследовательский проект, а стоимость Google не раскрыла. От комментариев о коммерческом продукте или сервисе формальной верификации компания тоже отказалась. То есть готовой кнопки «верифицировать мой код» пока нет.

Что можно сделать уже сейчас. Исследователи публикуют спецификацию и доказательство по Signal, и это хороший учебный материал для тех, кто пишет критичный код: платежи, криптографию, инфраструктуру доверия. Если вы работаете в таких областях, имеет смысл следить за тем, как инструменты вроде AlphaProof Code превращаются из демонстрации в продукт, и заранее учиться формулировать свойства кода так, чтобы их можно было доказывать. Именно эта навык, а не умение писать доказательства руками, судя по всему, станет ценным.