AlphaProof Code от DeepMind верифицировал криптопротокол Signal за 4 недели

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

Google DeepMind предлагает другой путь и выпустила AlphaProof Code. Это мультиагентная система, которая автоматизирует формальную верификацию кода.

Что такое формальная верификация, если без математики

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

Это самый высокий уровень гарантий в безопасности. Но им почти никто не пользуется: метод дорогой и долгий, а нужных специалистов единицы. Доказательство нередко оказывается длиннее самого кода, и писать его приходится вручную.

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

Команда применила AlphaProof Code к коду криптографического протокола Signal. На нём работает шифрование переписок в Signal и Google Messages. Агенты на базе Gemini 4 Carbon написали более шести миллионов строк на Lean. Это язык и проверяемая среда для формальных доказательств. В итоге математически доказано, что код обеспечивает заявленные гарантии безопасности.

Два числа здесь важнее остальных:

• 4 недели. По словам авторов, у команд экспертов задача такого масштаба обычно занимает годы.
• ~1%. Столько мест агенты сами отметили после аудита собственного доказательства как требующие взгляда человека. Остальное прошло без ручного вмешательства.

Google называет это первым случаем, когда ИИ использовали для формальной верификации реальной программы. Это заявление самой компании, независимой проверки пока нет.

Где подвох

Сначала о границах. Формальное доказательство честно настолько, насколько честна спецификация. Если свойства записаны неполно или не те, код докажут корректным относительно неверной цели. Поэтому слова «доказана безопасность» стоит читать как «доказано соответствие конкретным записанным гарантиям». Это не «взломать невозможно».

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

У подхода есть и сильная сторона. Доказательство проверяется автоматически, и ему не нужно верить на слово ни агентам, ни авторам. Если Lean принял доказательство, оно корректно. Галлюцинации модели здесь не страшны: неверный шаг просто не пройдёт проверку.

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

Разработчикам критичного кода (криптография, платежи, ядра ОС, протоколы консенсуса): следите за тем, как формальная верификация дешевеет. Если месяц вместо лет подтвердится на других проектах, порог входа резко упадёт.

Продактам и основателям в безопасности: вместо «мы прошли аудит» можно будет предъявлять проверяемое математическое доказательство. Это сильный аргумент для регулируемых отраслей и корпоративных клиентов.

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

Главный вывод простой. Агенты уже умеют писать код, и теперь появляется способ доказывать его корректность в масштабе, который раньше был недоступен. Авторы считают, что это, возможно, единственный способ противостоять скорости и масштабу современных кибератак. Спорное утверждение, но направление понятное.