10 ноября 2026 года Google DeepMind представила AlphaProof Code, фреймворк агентов для формальной проверки кода. Агенты на Gemini 4 Carbon собрали доказательства на Lean для эталонной библиотеки Signal: личный диалог libsignal v0.105.4, до машинного кода, который собирает обычный rustc. На этом протоколе стоят сам Signal и Google Messages, варианты протокола стоят в WhatsApp и Messenger. Заметку подписали Pushmeet Kohli и Swarat Chaudhuri: блог DeepMind.
Свойства выбирают люди. Доказательство потом обязано их закрыть, и ошибка, которая их ломает, через теорему не проходит. Раньше на этом месте обычно оставалась модель протокола. Здесь в Lean загружен собранный бинарник, исходник под доказательство не переписывали.
Спецификацию пишут вместе с агентами и принимают до доказательств. В технической статье на этом шаге названы Gemini 4 Carbon и Claude Opus 5.5. Черновик формулировок смотрит агент из другого семейства моделей, человек правит текст и закрепляет его. Дальше доказательства собирают команды агентов на Gemini 4 Carbon. В блоге ту же линейку коротко называют Gemini Carbon. Авторы пишут, что сами не набрали ни строки доказательств. Объём в блоге: больше шести миллионов строк Lean. В статье рядом стоит около 6,5 миллиона строк, которые принял kernel Lean. Доверять нужно короткому слою, около 26 тысяч строк спецификаций и семантики AArch64.
Про рецензию в блоге есть отдельная бытовая оценка. Агенты подсветили места, куда человеку стоит посмотреть второй раз: около процента доказательств. Остальное закрывает проверка Lean. Роли агентов заданы skills, текстовыми инструкциями к задаче. В кампании на одной машине от 40 до 80 агентов, идёт она от суток до трёх. Спецификации и доказательства вместе заняли у пяти человек четыре недели. У экспертных команд такой объём раньше растягивался на годы.
libsignal v0.105.4
В проверку вошёл неизменённый libsignal v0.105.4. Его собрали штатным rustc в машинный код AArch64 для Linux и связали с небольшой утилитой libsignal-cli. Теоремы сформулированы про этот исполняемый файл. Закрыты постквантовое рукопожатие PQXDH и Triple Ratchet: секретность рукопожатия, подлинность сообщений, прямая секретность и восстановление после компрометации.
Прямая секретность здесь конкретная. Ключ сообщения выводят из прошлого состояния и стирают. Украденное сегодняшнее состояние старые сообщения не открывает. Восстановление после компрометации завязано на следующий ответ: в него подмешивают свежий обмен Диффи-Хеллмана. Если в этот момент атакующий только слушает, украденное состояние новую переписку уже не читает.
Групповые чаты в кампанию не вошли, разобран диалог двоих. Семантика процессора тоже узкая: один поток, без сигналов, без динамической линковки и без файлов вне текущего каталога. X25519, Kyber1024, HMAC и AES-CBC с HMAC заданы контрактами. Теорема верна, пока верны эти условия. Стойкость самих примитивов доказательством не закрыта. В символьной модели секретность рукопожатия сохраняется и если позже квантовый противник ломает Диффи-Хеллмана. Конфиденциальность сообщений в вычислительной модели посчитана для классического противника с ограниченным временем.
Две старые ошибки
Силу спецификации проверили на двух ошибках, которые раньше нашли в libsignal и уже починили. Каждую вернули в отдельную копию v0.105.4, отменив известный фикс, и собрали бинарник заново. Для обеих сборок Lean доказал, что символьная теорема безопасности на этом файле ложна. В обычной v0.105.4 оба фикса на месте. Текущий релиз этими двумя ошибками не открыт.
Первая, weak state, фикс cd36118. Prekey-сообщение не расшифровалось в новой сессии, и код пробует его на старых. Если старая сессия сообщение приняла, сохраняется неподтверждённое состояние новой. В этом состоянии лежит копия секрета подписанного prekey.
Вторая, small subgroup, фикс 5293caa. Отвечающая сторона PQXDH не проверяет, что базовый ключ X25519 инициатора лежит в допустимом диапазоне и не попадает в малую подгруппу. Повтор рукопожатия с испорченным ключом поднимает вторую сессию с тем же общим секретом.
Репозиторий на Lean
Артефакты проверки выложены открыто: google-deepmind.github.io/code-verification. Там спецификации и доказательства этой кампании. PDF лежит рядом с анонсом, на сайте DeepMind. Свой плагин, бот или бинарник в репозиторий сам не встаёт. Спецификацию по-прежнему принимает человек, а разобранный пример один: libsignal.
Ключ Gemini API этот релиз не трогает. Наружу выложен разбор libsignal v0.105.4: личный диалог, без групп, примитивы как условия, доказательства проверяет kernel Lean. Если библиотека есть в зависимостях, смотреть стоит именно эти границы.
