DeepMind доказал математически безопасность кода Signal за 4 недели вместо лет

Любой, кто писал криптографию, знает неприятную вещь: протокол можно красиво доказать на бумаге, а уязвимость всё равно окажется в коде. Между схемой и реализацией лежит пропасть, и именно там живут настоящие баги. Google DeepMind заявляет, что научила AI-агентов закрывать эту пропасть для одного из самых важных протоколов в мире — того, что защищает переписку в Signal и Google Messages.

Что именно сделали

Система называется AlphaProof Code. Это мультиагентный фреймворк на нескольких LLM, который делит работу так же, как её поделила бы исследовательская команда. Сначала люди-эксперты вместе с моделями переводят цели безопасности Signal в формальные математические спецификации. Каждую спецификацию вручную проверяет человек. Затем агенты на Gemini Carbon пишут сами доказательства на языке Lean — получилось больше шести миллионов строк.

Дальше самое практичное. Lean сам проверяет корректность каждого доказательства, поэтому доверять модели вслепую не нужно: неверный вывод просто не пройдёт проверку. Агенты дополнительно проаудитировали результат и отметили места, где нужен взгляд человека. Это около 1% кодовой базы. Эксперты сосредоточились на них, а не на перечитывании миллионов строк.

Почему это не очередной аудит

Обычная формальная верификация протоколов останавливается на уровне дизайна: доказывают, что схема безопасна. Здесь агенты шли дальше и доказывали свойства для скомпилированного кода, который работает на устройствах. Например, что сообщения остаются защищёнными до и после временной компрометации устройства.

Для проверки честности системы авторы провели простой тест. В изолированную версию кода Signal вернули два реальных, ранее исправленных бага. В обоих случаях система выдала машинно проверяемое доказательство того, что эта версия небезопасна. То есть инструмент отличает правильный код от неправильного, а не просто «одобряет» всё подряд.

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

Ограничения и практический вывод

Стоит трезво смотреть на масштаб. Это один протокол, который давно и тщательно изучали, а основная часть заявленных цифр опирается на самоотчёт DeepMind. Людей из процесса не убрали: специфика того, что считать «безопасным», по-прежнему задаётся экспертами, и ошибка в спецификации даёт доказательство не того, что нужно. Авторы сами говорят, что для масштабирования нужны дальнейшие исследования. Заявленные направления — прошивки медицинских устройств и ПО для энергосетей — пока лишь планы.

Что это значит для разработчиков и основателей?

• Связка «LLM пишет, формальный проверяющий принимает или отклоняет» — рабочая схема для задач, где цена ошибки высока. Модели позволено ошибаться, проверяющему — нет.
• Если вы делаете криптографию, платёжную логику или критичный embedded-код, формальная верификация перестаёт быть уделом академических команд с бюджетом на годы.
• Навык формулировать спецификации становится ценнее навыка писать доказательства. Узкое место смещается к вопросу «что мы вообще хотим гарантировать».

Отдельный плюс — DeepMind открывает артефакты верификации. Их можно изучить и использовать как образец для собственных экспериментов с Lean и агентами. Вместе с инструментами вроде CodeMender, которые ищут и чинят уязвимости, формальные доказательства превращаются в часть обычного защитного контура, а не в редкую академическую экзотику.