Что произошло 11 ноября 2026 года
Google DeepMind заявила, что применила систему AlphaProof Code для формальной проверки криптографического ядра Signal. По сообщению The Decoder, пересказавшего публикацию исследователей DeepMind, работа заняла четыре недели; исследователи сопоставляют этот срок с годами, которые обычно требуются для задач такого типа.
Для пользователей это не новое изменение настроек Signal и не отдельный режим защиты. Речь идёт о заявленной проверке конкретной части программного кода, а не о смене работы мессенджера.
Как описана проверка
Сначала специалисты задали формальные требования безопасности. Затем AI-агенты на базе Gemini Carbon создали более шести миллионов строк доказательств на языке Lean. По сообщению The Decoder со ссылкой на исследователей DeepMind, около одного процента кода система выделила для проверки людьми.
The Decoder также сообщает, что в проверку включили два намеренно внесённых дефекта и AlphaProof Code обнаружила оба. Это описание относится к подготовленному тесту и само по себе не показывает, насколько полно система находит неизвестные ошибки.
Какая часть Signal проверялась
По данным The Decoder, AlphaProof Code проверяла криптографическое ядро Signal — код, работающий на устройствах пользователей. Это конкретнее, чем проверка только теоретического описания криптографического протокола, но охват работы нельзя приравнивать ко всему мессенджеру.
В сообщении не установлено, что проверены интерфейс, операционные системы и устройства, серверная инфраструктура, доставка сообщений, обновления или весь код приложений Signal. Независимого воспроизведения результата и полного описания методики в доступной публикации также нет.
Что это меняет для пользователя
Если описанная проверка проведена корректно, она может помочь находить ошибки в охваченном криптографическом коде и проверять его соответствие заданным требованиям. Но результат формальной проверки зависит от самих требований и границ проверенного кода: он не гарантирует безопасность всей системы или каждого сценария её использования.
Срок в четыре недели, объём доказательств и обнаружение двух тестовых дефектов The Decoder приводит со ссылкой на исследователей DeepMind. Пока это сообщение не подтверждено независимой проверкой, его следует понимать как описание заявленного результата, а не как доказательство абсолютной безопасности Signal.
