Код AlphaProof доказал корректность криптографии Signal — на уровне скомпилированного бинарного файла

Six and a half million lines of Lean, produced in four weeks, by agent teams that no human helped write. That is the headline number G​oogle DeepMind published on 10 November 2026 for AlphaProof Code, an agentic framework for formal verification that the lab used to machine-check the cryptographic core of the Signal protocol — and, unusually, to check it at the level of the compiled AArch64 binary rather than the design document above it. The models that did the work are a different question. one API key at provider list price with 0% markup The proof agents' engine is not something we serve.

The framework is not a model you can call. It is a harness: human experts decide what must be true, a mixture of models turns those goals into Lean specifications, and then teams of proof-writing agents — the blog names G​emini Carbon as the engine — fill in the proofs until Lean's kernel accepts them. What shipped alongside the announcement is the artifact set, at github.com/google-deepmind/code-verification, and a technical paper that is far more candid about the boundaries of the result than the blog post is. Most of what follows comes from that paper, because the paper is where the interesting numbers live.

Что на самом деле было доказано и против чего

Цель — libsignal v0.105.4 со spqr v1.6.0, собранный штатным rustc 1.98.1, статически слинкованный с musl и выпущенный в виде одного исполняемого файла AArch64 Linux. Эта деталь важнее любого бенчмарка: доказательства касаются байтов, которые выполнялись бы на телефоне, а не функции на Rust, которую компилятор, как предполагается, транслирует корректно. Команда проверила примерно 560 КБ исходного кода libsignal, около 140 000 инструкций AArch64, и сделала это, написав модель набора инструкций на Lean — 467 инструкций и 31 системный вызов в 7 578 строках — а затем доказав, что реальный образ ELF, загруженный и выполненный в рамках этой модели, сохраняет свойства безопасности.

Свойства именно такие, какие запросил бы инженер по протоколам. Десять символических теорем охватывают прямую секретность, безопасность после компрометации, секретность инициатора и ответчика, аутентификацию и пять следствий из теоремы 1 PQXDH. Основной результат называется signal_session_secure_placed. Есть также вычислительное направление с конкретной оценкой, и эти два направления используют разные модели противника: символическая сторона (Долев–Яо, через фреймворк DyLean) даже охватывает квантового атакующего, который ломает Диффи–Хеллмана после рукопожатия, тогда как вычислительная сторона охватывает только классических противников.

Куда уходят шесть миллионов строк

«Свыше шести миллионов строк» — так сформулировано в блоге, и это точно, но грубо. Полезная часть — разбивка из статьи, и её стоит читать как таблицу затрат, а не как повод похвастаться:

• Доказательства для бинарного файла — 5,3 миллиона строк, основная часть работы, охватывающая семантику машинного кода и уточнение от символьной модели вплоть до исполняемого файла.

• Вычислительные доказательства — около 860 000 строк.

• Символьные доказательства — около 350 000 строк.

• Доказательства отсутствия ошибок — около 140 000 строк для двух намеренно повторно внедрённых уязвимостей, описанных ниже.

• Доказательства для аллокатора — около 70 000 строк.

Почти семь миллионов строк, если считать комментарии и пустые строки, — в статье их считают, а в блоге нет. В любом случае важное соотношение — между доказательством и тем, что доказано: 6,5 миллиона строк на Lean, чтобы установить свойства бинарного файла размером 560 КБ. Это соотношение — честная мера того, насколько эта методика далека от рутины, и именно это число стоит приводить, когда кто-то спрашивает, стала ли формальная верификация дешёвой.

Доверенная база меньше доказательства, и в этом весь смысл.

Доказательство сильно лишь настолько, насколько сильны его допущения. Статья конкретна в этом отношении, и именно конкретность отличает её от пресс-релиза. Доверенные спецификации составляют около 18 000 строк (28 000 с документацией), семантика AArch64 — около 8 000, а кодировка машинного кода на Lean — около 95 000. Тридцать семь процедур заменены контрактами, а не верифицированы — сжатие SHA-256 и SHA-512, AES-256-CBC, X25519, операции на кривой Эдвардса, Kyber1024 и ML-KEM-768, а также libcrux HMAC. Восемнадцать точек входа panic также принимаются на веру, а не доказываются.

Итак, утверждение состоит не в том, что «всё доказано». Утверждение в том, что доказаны логика криптографического протокола, конечный автомат сеанса и уточнение (refinement) от этой логики к фактически исполняемым инструкциям, тогда как примитивы под ними считаются доверенными — так же, как любой проект верификации доверяет своим примитивам. Компилятор Rust, в частности, невходит в доверенную базу: команда избежала необходимости доверять ему, рассуждая на уровне машинного кода, — это тот же приём, который позволяет им полностью обойтись без верифицированного компилятора. Для понимания масштаба: в статье приводятся оценки seL4 примерно в 20 человеко-лет, а CompCert — около 6.

Два бага, намеренно возвращены обратно

Систему верификации, которая всегда говорит только «корректно», невозможно протестировать. Поэтому команда взяла две уязвимости, которые ранее были найдены и исправлены в коде Signal — ошибку слабого состояния и ошибку малой подгруппы — повторно внесла их в изолированную копию и заново запустила конвейер. В обоих случаях AlphaProof Code получил проверенное машиной доказательство того, что версия с ошибками не удовлетворяет теореме безопасности: символическое утверждение сводится к ¬Sec(Asm_bug).

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

Как запускались агенты

Пять исследователей на протяжении четырёх недель, каждый непрерывно запускал агентов. Само написание доказательств выполняли команды из 40–80 агентов, работавшие от 24 до 72 часов на одной машине на команду, при этом над оркестратором команды стоял агент-супервизор. Агент-привратник проверяет каждую заявку с помощью компаратора на соответствие отложенной копии спецификации и ядру Lean — защита от того, чтобы агент доказал незаметно ослабленную версию требуемого.

Человеческая работа в основном выполнялась на раннем этапе и была сосредоточена на спецификациях. Каждую спецификацию проверял эксперт до начала работы над доказательствами, а собственный аудит агентов пометил около 1% кодовой базы как требующей внимания человека. Ни один человек не писал код доказательств. В статье также прямо говорится об инженерной стороне: чистая сборка может занимать несколько часов; на ранних этапах небольшое изменение исходного кода или перекомпилированный двоичный файл вынуждали вносить масштабные исправления доказательств, и в самих доказательствах, сгенерированных ИИ, и в методах доказательства есть «существенный простор для оптимизации».

Что не охватывают доказательства

Раздел ограничений достаточно длинный, чтобы быть самым важным разделом статьи, а сами ограничения изложены без обиняков. Для свойства восстановления SPQR не установлена постквантовая гарантия — теоремы о храповике предполагают, что злоумышленник выбирает ключи SPQR. Конфиденциальность полезной нагрузки не доказана. Аутентификация отвечающей стороны не доказана для первого сообщения рукопожатия, которое так и не проходит процедуру повышения. Модель допускает одну сессию на каждое повышение, фиксированные длины сообщений, отсутствие состояния для нескольких устройств и ключи идентификации с доверием при первом использовании.

Существует также оценка, которая становится бессодержательной. Слагаемое подделки 8-байтового MAC составляет не менее 2⁻⁶⁴ на попытку и растёт квадратично по числу сообщений и эпох, а значит, оценка перестаёт что-либо давать уже для одной сессии примерно из 25 000 сообщений или для 2²⁰ сессий по 2¹⁰ сообщений. И предметом доказательства является сборка libsignal-cli, сделанная командой и запущенная как новый процесс, — а не приложение Signal на вашем телефоне. Несколько предположений об окружении обосновываются неформально, а не доказываются.

Нет ни API, ни цены, ни модели, к которой можно обратиться

Это та часть, которая разочарует любого, кто пришёл из таблицы лидеров моделей. AlphaProof Code — это исследовательский фреймворк и опубликованный набор артефактов. Здесь нет ни эндпоинта, ни тарифной сетки за токены, ни списка ожидания, ни весов: репозиторий содержит разработку на Lean, семантику AArch64, биндинг libsignal и спецификации, а не чекпоинт. В блоге сказано, что артефакты имеют открытый исходный код; на лендинге не указана лицензия, и это стоит проверить, прежде чем кто-либо планирует строить что-то поверх них.

The models that did the work are a different question. The paper names G​emini 4 Carbon for the proof agents and says Claude Opus 5.5 was used alongside other models for drafting and reviewing specifications. Claude Opus 5.5 is on OrcaRouter's catalogue today at $4 per million input tokens and $20 per million output, with provider list price passed through at 0% markup — so if the practical takeaway you want is "run a spec-drafting loop with the model the paper used," that part is a normal API call, and a vendor price change lands on our side the same day. The proof agents' engine is not something we serve, and nothing here implies we host AlphaProof Code itself.

Почему это важнее, чем результат Signal

Верификация Signal впечатляет сама по себе — это первая формальная верификация широко развёрнутого протокола, а именно его реализации любым методом, с ИИ или без него, по словам DeepMind, и первый случай, когда ИИ проверил развёрнутый криптографический протокол на такой глубине. Но переносимое утверждение — это рабочий процесс. Команда из пяти человек за четыре недели, с этапом проверки спецификации и агентом-привратником, создала корпус доказательств, который раньше был бы многолетним проектом. Если это соотношение выполняется хотя бы приблизительно, набор систем, которые могут позволить себе верификацию, меняется: прошивки медицинских устройств, программное обеспечение энергосетей, тот тип кода, который сейчас получает код-ревью и молитву.

Выдержит ли это — не проверено. Криптография Signal необычно хорошо специфицирована, команда привлекла собственных инженеров Signal к рецензированию методологии, а примитивы были отданы на подряд, а не верифицированы. Следующая система не будет столь уступчивой. Собственная формулировка статьи — объединить формальную верификацию с автоматизированными агентами защиты, такими как CodeMender, — честно отражает суть предложения: верификация говорит, что истинно, а что-то ещё должно исправлять то, что не является таковым.

Что посмотреть

Three things would move this from a landmark paper to an industrial technique. A second, independent codebase verified by someone outside G​oogle, ideally one where the specification had to be written from scratch rather than adapted from an existing analysis. A cost figure — agent-hours, accelerator-hours, dollars — because four weeks and 40-to-80-agent teams is not a unit any engineering manager can budget against. And the computational-track bug refutation, which the paper leaves open and which is the difference between a system that proves properties and a system that can also tell you, computationally, that a specific binary is broken.

А пока читайте репозиторий с артефактами, а не анонс. Доказательства там, Lean их проверяет, и в статье точно указано, какие предположения они делают.