Google DeepMind за месяц выполнила формальную проверку Signal — математически подтвердила корректность части кода криптографического протокола мессенджера. Это важно не только для пользователей Signal: тот же фундаментальный подход к сквозному шифрованию используют WhatsApp и Google Messages, а для разработчиков и ИБ-команд результат показывает, что автоматическое доказательство свойств кода перестаёт быть исключительно академической дисциплиной.
Работу выполнили с помощью AlphaProof Code — агентной системы DeepMind для формальной верификации. Как сообщает ZDNet, исследователи опирались на предыдущую работу Signal Foundation: люди вместе с ИИ-агентами сначала определяли, какие именно свойства реализации нужно доказать, а затем несколько агентов на модели Gemini Carbon строили и проверяли доказательства. В итоге человека попросили повторно изучить лишь около 1% проверяемой кодовой базы.
Не тесты, а доказательство
Обычное тестирование отвечает на вопрос, ведёт ли себя программа правильно на конкретных наборах входных данных. Формальная верификация ставит планку заметно выше: разработчик описывает свойства, которым должен соответствовать код, а система доказывает их математически. Если модель угроз, спецификация и само доказательство сформулированы корректно, проверяемый фрагмент нельзя «сломать» сценарием, который просто не попал в тестовый набор.
Именно поэтому метод особенно востребован там, где цена ошибки неприятно велика: в криптографии, платёжной инфраструктуре, авиации, медицинском оборудовании и промышленной автоматике. Но у него есть старый и довольно прозаичный враг — трудозатраты. Формальные доказательства обычно вручную готовят специалисты, которые одновременно понимают предметную область, исходный код и инструменты автоматического доказательства теорем. На крупном проекте такая работа может растянуться на годы.
DeepMind утверждает, что её команда впервые применила ИИ для формальной проверки широко используемого криптографического протокола на такой глубине. При этом речь не идёт о полном аудите всего Signal и не означает, что в приложении больше не может быть уязвимостей. Проверка относится к части базового криптографического кода; вокруг него остаются клиентские приложения, серверная инфраструктура, обновления, метаданные, реализация на конкретных платформах и человеческие ошибки.
Разработчики дополнительно дали AlphaProof Code два уже исправленных бага Signal. Система сумела отличить корректный код от дефектного и построить соответствующие доказательства. Это важная, хотя и ограниченная проверка практической пригодности: инструмент должен не только подтверждать удачные реализации, но и не пропускать известные ошибки.
ИИ в безопасности становится и атакующим, и аудитором
Новость хорошо ложится в тренд 2026 года: ИИ-инструменты одновременно ускоряют поиск слабых мест и увеличивают поверхность атаки. Агенты могут быстрее анализировать репозитории, собирать цепочки эксплуатации и генерировать код, но те же механизмы помогают защитникам разбирать большие проекты и автоматизировать аудит. В случае AlphaProof Code DeepMind делает ставку не на очередной сканер, который выдаст сотни предупреждений, а на более строгий подход: превратить часть инженерных утверждений в проверяемые доказательства.
Для команд разработки из этого следует довольно практичный вывод. ИИ не отменяет необходимость в понятной архитектуре, спецификациях и ревью — наоборот, без них доказать полезные свойства трудно. Агенту нужно объяснить, что именно считается корректностью: например, какие ключи допустимы, как устроено состояние протокола и какие переходы запрещены. Чем точнее инварианты и границы компонентов, тем больше шансов автоматизировать проверку без месячной ручной расшифровки намерений авторов кода.
Для бизнеса главный эффект может проявиться не в мессенджерах, а в критичных сервисах с длинным жизненным циклом. DeepMind прямо называет среди возможных областей прошивки медицинских устройств и ПО для энергосетей. Там даже узкая формальная проверка наиболее рискованных модулей может быть полезнее, чем попытка «покрыть тестами всё». Но считать результат готовой универсальной кнопкой безопасности преждевременно: доказательство подтверждает заявленные свойства конкретного фрагмента, а не заменяет моделирование угроз, анализ зависимостей, контроль поставки и реагирование на инциденты.
DeepMind собирается открыть исходный код AlphaProof Code. Если инструмент окажется воспроизводимым и пригодным за пределами демонстрации на Signal, формальная проверка Signal станет не разовой витриной возможностей модели, а ориентиром для криптографических библиотек и систем с высокой ценой сбоя. Главный вопрос теперь в том, смогут ли команды так же быстро формализовать требования к собственному коду — и научатся ли доверять ИИ ровно настолько, насколько позволяют проверяемые доказательства, а не рекламные обещания.
