AlphaProof Code доказал корректность ядра шифрования Signal за 4 недели вместо лет

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

Что показали в DeepMind

Команда представила AlphaProof Code — систему, которая доказывает, что программа соответствует своей спецификации безопасности без ошибок. Демонстрацию провели на ядре протокола шифрования Signal. По словам исследователей Пушмита Кохли и Сварата Чаудхури из блога DeepMind, на такую работу обычно уходят годы, а здесь хватило четырёх недель.

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

Как это устроено на простом примере

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

Процесс разделён на два этапа:

• Сначала эксперты-люди формулируют формальные требования безопасности: что именно должен гарантировать код.
• Затем ИИ-агенты на базе Gemini Carbon помогают оформить спецификации и независимо доказывают, что программа им соответствует.

В сумме агенты написали больше шести миллионов строк на Lean. Около 1% кодовой базы система пометила для ручной проверки людьми. Для контроля исследователи заложили в код две ошибки, и обе были пойманы сразу. Технический директор Signal Эрен Крет говорит, что такой подход усиливает доверие к приватности данных на фоне растущих угроз со стороны ИИ.

Что здесь стоит держать в голове

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

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

Третье: 1% кода на человеческом ревью выглядит скромно, но речь о криптографии, где один непроверенный фрагмент может обесценить остальное. Пометка таких участков — часть метода, а не его слабость.

Что это значит на практике

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

Для продактов и основателей это новый аргумент доверия. Фраза «код доказан математически» сильнее, чем «мы прошли аудит». Если стоимость верификации действительно упадёт с лет до недель, такой аргумент станет доступен не только Signal.

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