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

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

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

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

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

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

Где подвох

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

Главный вопрос индустрии — масштаб и цена. DeepMind провела анализ бесплатно, как исследовательский проект, а во сколько он обошёлся, в Google говорить отказались. На вопрос, планирует ли компания коммерческий продукт или сервис для формальной верификации, ответа тоже не дали. Сам исследователь Сварат Чаудхури признаёт, что до масштабирования на весь софт мира «ещё долгий путь».

Человек остаётся в контуре

Интереснее всего процесс, который команда называет «human-AI collaboration». Агенты вносят вклад почти на каждом этапе и сами исправляют свои ошибки, но на ключевых развилках запрашивают проверку человека. Чаудхури прямо говорит, что не хочет «вайбового мира», где ИИ сам формулирует цели, сам пишет доказательства и по сути сдаёт самому себе тесты. Нужна середина.

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

Что с этим делать

Разработчикам и основателям, чей продукт держится на критичной логике (платежи, криптография, протоколы синхронизации), пора присмотреться к формальной верификации как к реальной опции, а не академической экзотике. Пока её стоимость неизвестна, закладывать её в бюджет рано. Но есть и конкретная польза: DeepMind публикует спецификацию и доказательство по Signal, их можно изучать и использовать в другой верификационной работе.

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