DeepMind: агенты AlphaProof Code за 4 недели сгенерировали 6+ млн строк Lean-доказательств для Signal

Google DeepMind опубликовал AlphaProof Code — агентный мульти-LLM framework для формальной верификации, и сразу показал результат: за ~4 недели ключевые свойства безопасности libsignal (библиотеки протокола Signal) были проверены формально, с генерацией более 6 миллионов строк доказательств на Lean.

Как устроен пайплайн

• Спецификации — цели верификации (например, forward secrecy) формулируются как формальные утверждения; люди вместе с моделями их готовят и эксперты ревьюят каждую.
• Доказательства — агенты (на базе Gemini Carbon) генерируют Lean-коды доказательств; каждый шаг проверяется машиной автоматически.
• Ревью — по заявлению DeepMind, на финальное ручное ревью уходит порядка процента результата.

Артефакты и технический отчёт открыты.

Что это значит

Формальная верификация исторически была дорогой ручной работой «на годы». Если агенты за четыре недели закрывают критичный крипто-модуль:

• формальная проверка становится практичным инструментом, а не исследовательским демо — можно пилотировать на компактных критичных модулях;
• меняется экономическая модель assurance: «модели тянут, человек ревьюит»;
• для security-critical инфраструктуры (шифрование, протоколы, парсеры) появляется измеримый критерий: сколько строк доказательств, сколько покрыто, сколько осталось на ручное ревью.

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

Источник: Google DeepMind Research — AlphaProof Code (объявлено 10 ноября 2026)