# AlphaProof Code and Signal: проверенные доказательства безопасности машинного кода и доверенные предположения

Published: 2026-11-11

Google DeepMind сообщает о машинных проверках выбранных свойств безопасности для скомпилированной оболочки командной строки libsignal. Lean проверяет доказательство, в то время как люди утверждают спецификацию и ее предположения. Отдельный компаратор проверяет теорему и все зависимые определения на соответствие утвержденной цели.

Canonical: https://thedailydiff.dev/ru/video/2026-11-10-signal-machine-proof/

## Что освещается в этом видео

- Агенты ИИ создают кандидаты доказательств; ядро Lean проверяет, подтверждают ли они формальное утверждение, одобренное человеком.
- Проверенная цель — это конкретная скомпилированная оболочка командной строки libsignal с доверенной семантикой и криптографическими контрактами.
- Доказательство скомпилированного бинарного файла исключает компилятор Rust из доверенной базы для заявленных свойств этого бинарного файла.
- Исследователи сообщают о двух изолированных повторных введениях ранее исправленных ошибок, которые нарушают их символическую теорему безопасности.
- Компаратор проверяет теорему и каждое зависимое определение на соответствие защищенной утвержденной спецификации; поправки проходят отдельный процесс рецензирования.

## Вопросы и ответы

### Что AlphaProof Code доказал о реализации Signal?

Google DeepMind сообщает о проверенных доказательствах выбранных свойств безопасности для скомпилированной оболочки командной строки libsignal. В техническом документе рассматриваются конфиденциальность и аутентификация сообщений, а также прямая секретность и посткомпромиссная безопасность в рамках заявленных моделей. Результат сохраняет условия для злоумышленника, сессии и криптографических предположений. Его область исключает общую гарантию для каждого приложения или установки Signal.

### Кто решает, что должно доказывать сгенерированное ИИ доказательство безопасности?

Человеческие рецензенты утверждают спецификацию и ее предположения. Технический документ Google DeepMind описывает агентов, разрабатывающих спецификации под руководством человека, и рецензентов, проверяющих, отражают ли утверждения значимые свойства безопасности. Lean проверяет логику полученного доказательства. Люди остаются ответственными за выбор сильной цели, проверку предположений и вынесение решений по предлагаемым изменениям в утвержденную спецификацию.

### Зачем проверять скомпилированный машинный код вместо того, чтобы доверять компилятору Rust?

Доказательство относительно скомпилированного бинарного файла непосредственно устанавливает заявленные свойства для этого артефакта. В документе Google DeepMind объясняется, что ошибка компилятора, нарушающая одно из этих свойств, сделала бы теорему ложной. Таким образом, компилятор Rust покидает доверенную базу для этого утверждения. Доказательство по-прежнему доверяет модели инструкций, ядру Lean и указанным криптографическим контрактам.

### Как компаратор мешает агенту доказательства ослабить свою цель?

Компаратор проверяет теорему и каждое определение, от которого она зависит, на соответствие защищенной утвержденной спецификации. В документе Google DeepMind говорится, что агенты доказательств не могут записывать в эту сохраненную копию. Проверяющий также проверяет разрешенные аксиомы и воспроизводит доказательство в свежем ядре. Предлагаемые поправки к спецификации следуют отдельному процессу рецензирования, в то время как люди остаются ответственными за силу цели.

### Какой был вердикт The Daily Diff относительно рабочего процесса проверенного доказательства?

Вердикт The Daily Diff был SHIP IT. Нико отправил бы рабочий процесс проверенного доказательства, потому что утвержденное утверждение остается отдельным от агента, дающего ответ. Он сохранял бы область действия и предположения, прикрепленные к каждому результату. Эпизод сообщает о опубликованном артефакте доказательства Google без независимого его перестраивания и одобряет рабочий процесс в рамках этих границ доказательств.

## Главы

- 0:00 Кто проверяет доказательство безопасности ИИ?
- 0:57 Как утверждение становится целью доказательства?
- 1:39 Зачем доказывать скомпилированный бинарный файл?
- 2:16 Какие свойства безопасности пережили разрыв в реализации?
- 2:59 Может ли спецификация отклонять сломанный код?
- 3:36 Может ли правильное доказательство ответить на неправильный вопрос?
- 4:13 Что улавливает движущиеся цели?
- 4:53 Отправил бы я этот рабочий процесс доказательства?

## Переведенная стенограмма

Переведено с оригинального английского повествования. Доступные аудио и субтитры контролируются YouTube.

### Кто проверяет доказательство безопасности ИИ?

0:00 Аудит безопасности ИИ по-прежнему звучит как доверие чат-боту. Новый результат Google по Signal включает математические доказательства, которые отдельное ядро проверяет. В этом видео, что доказал Google? И как они мешают агенту менять цели? Вот полезный ответ. Модели пишут кандидаты доказательств, и Lean проверяет доказательства на соответствие утверждению, одобренному человеком, о выбранном скомпилированном коде. Люди по-прежнему владеют утверждением и предположениями.

0:21 Вы можете проверить результат, не веря в победную речь модели. Отдельная проверка выявляет незаметное изменение вопроса. Мы проследим это до определений. Сегодня вторник, десятое ноября, и это The Daily Diff. AlphaProof Code — это фреймворк Google для написания спецификаций программного обеспечения с руководством человека и генерации проверенных доказательств с помощью агентов ИИ. Это исследование нацелено на libsignal, библиотеку Rust, реализующую протокол обмена сообщениями Signal, внутри конкретной программы командной строки.

0:45 Google объявил о работе сегодня. В его статье говорится, что пять исследователей работали более четырех недель. Агенты писали доказательства, в то время как люди большую часть своих усилий тратили на спецификации. Требования нашли способ стать еще более дорогими встречами. Спецификация говорит, что программа должна делать,

### Как утверждение становится целью доказательства?

0:59 что контролирует злоумышленник, и какие предположения необходимы для аргумента. Рецензенты спрашивают, отражает ли это безопасность, о которой заботятся люди. Прекрасно проверенный ответ на слабый вопрос оставляет этот вопрос без изменений. Команда основывается на более ранних исследованиях рукопожатия Signal и его хранилища ключей сообщений. Формальные анализы уже изучали эти конструкции. Утверждение Google связывает их аргументы безопасности с неизмененной производственной скомпилированной реализацией библиотеки, где дизайн должен выдержать контакт с фактическим кодом. Технический директор Signal, Эрен Крет,

1:27 описывает расширение за пределы меньших областей предыдущей проверки. Детали реализации включают сообщения не по порядку и архивированные сессии для отложенных сообщений. Реальное программное обеспечение хранит квитанции, которые ваша элегантная диаграмма выбросила. Исследователи компилируют неизмененную библиотеку Rust стандартным

### Зачем доказывать скомпилированный бинарный файл?

1:41 компилятором в исполняемый файл Arm sixty-four Linux. Их теоремы описывают этот бинарный файл с использованием формальной модели инструкций, преодолевая разрыв между исходным кодом и оптимизированным машинным кодом. Ошибка компилятора, нарушающая заявленное свойство, сделает его теорему ложной. Поэтому компилятор покидает доверенную базу для этого бинарного файла. Вы по-прежнему доверяете модели инструкций и проверяющему Lean. Граница доверия переместилась, и у нее есть адрес. Около шести с половиной миллионов строк проверенного доказательства основаны на примерно двадцати шести

2:06 тысячах доверенных спецификаций и строк семантики инструкций. Это количество артефактов. Рассматривать их как показатели интеллекта — это все равно, что ранжировать разработчиков по размеру их папки с модулями узлов.

### Какие свойства безопасности пережили разрыв в реализации?

2:16 Аргументы охватывают конфиденциальность и аутентификацию сообщений, с прямой секретностью и посткомпромиссной безопасностью в рамках заявленных моделей. Последние два описывают ограничения на ущерб от украденных ключей и восстановление после свежих обменов. Каждая гарантия имеет условия для злоумышленника и сессии. Криптографические примитивы находятся за доверенными контрактами. Доказательство предполагает, что эти процедуры ведут себя в соответствии со спецификацией, и полагается на криптографические предположения безопасности. Одно доказательство идеализирует криптографию; другое рассуждает о вероятностях успеха злоумышленника.

2:42 Оба имеют ограничения на сценарии, которые они охватывают. Спросите, какая сборка, какое свойство и какие предположения. Этот результат касается оболочки командной строки исследователей. Групповые сообщения — это будущая работа, а вычислительная модель исключает состояние нескольких устройств. Называть каждую установку Signal без ошибок выходит за рамки теоремы. Исследователи повторно ввели две ранее исправленные ошибки Signal в

### Может ли спецификация отклонять сломанный код?

3:02 изолированные копии и скомпилировали их. Проверенные доказательства показали, что эти бинарные файлы нарушали символическую теорему безопасности. Это проверяло, может ли спецификация отклонять реально сломанные реализации. Ваш зеленый флажок нуждается в красном тесте. Google публикует спецификации и доказательства с инструкциями по проверке. Репозиторий сообщает, что чистая сборка занимает часы и требует значительного объема памяти. Чтение объявления значительно проще на ноутбуке. Модель оборудования и доверенные контракты все еще нуждаются в проверке.

3:26 Я не перестраивал огромный артефакт для этого эпизода. Мы сообщаем о опубликованном результате и его границах. У сторонних наблюдателей есть возможность его проверить, что для меня важнее, чем еще один круг почета ИИ. Теперь ловушка.

### Может ли правильное доказательство ответить на неправильный вопрос?

3:36 Lean может принять правильное доказательство утверждения, которое почти ничего не требует. Невозможные предположения могут сделать теорему бессодержательной. Изменение определения, скрытого под заголовком теоремы, может ослабить цель. В статье предусмотрены проверки против этого. Хранитель хранит утвержденную спецификацию, к которой агенты доказательств не могут записывать. Они могут предлагать исправления через отдельный процесс внесения поправок. Ослабление безопасности рассматривается как потенциальная ошибка. Заявление проверяющего об успехе здесь не имеет силы.

4:00 Люди решают изменения в доверенных предположениях, напрямую или через свою политику, и пересматривают поправки после каждой кампании. Экспертная оценка остается под контролем. Агент может запросить другое задание. Он не может сам себе поставить проходной балл.

### Что улавливает движущиеся цели?

4:13 Вот обещанная проверка. Компаратор Lean сравнивает теорему и каждое определение, от которого она зависит, с этой защищенной утвержденной копией. Он также проверяет разрешенные аксиомы и воспроизводит доказательство в свежем ядре. Незаметное ослабление вспомогательного определения поэтому меняет сравниваемый объект. Принятое доказательство должно подтверждать утвержденную цель. Это по-прежнему оставляет людей ответственными за выбор сильной цели и честных предположений. Для вашего собственного рабочего процесса ИИ держите критерии приемлемости вне

4:37 разрешений на редактирование работника и отдельно рассматривайте предлагаемые изменения. Результат Google делает это разделение конкретным. Писатель доказательства выполняет работу; граница проверки решает, имеет ли это значение. Если вы предпочитаете читать это, а не слушать, The Daily Diff попадает в ваш почтовый ящик каждое утро, бесплатно на daily diff dot dev, ссылка ниже. Так что сегодняшний вердикт — SHIP IT.

### Отправил бы я этот рабочий процесс доказательства?

4:54 Я бы отправил этот рабочий процесс проверенного доказательства, потому что утвержденное утверждение остается отдельным от агента, дающего ответ. Я бы сохранял область действия и предположения, прикрепленные к каждому результату. Подпишитесь, нажмите на колокольчик и сообщите мне в комментариях, если бы вы отметили это по-другому. И это все на сегодня. Я Нико из Axrisi. Сливайтесь ответственно.

## Источники

- [AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeeping](https://google-deepmind.github.io/code-verification/) — Swarat Chaudhuri and colleagues / Google DeepMind and Google
- [Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO response](https://deepmind.google/blog/introducing-alphaproof-code/) — Pushmeet Kohli and Swarat Chaudhuri / Google DeepMind
- [Code-verification repository — initial commit, public artifacts and checking instructions](https://github.com/google-deepmind/code-verification) — Google DeepMind / GitHub
- [The PQXDH Key Agreement Protocol — older official specification and prior-analysis context](https://signal.org/docs/specifications/pqxdh/) — Ehren Kret and Rolfe Schmidt / Signal
- [The Double Ratchet Algorithm — Triple Ratchet section](https://signal.org/docs/specifications/doubleratchet/) — Trevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
- [Google DeepMind leadership — Demis Hassabis's relevant lab identity](https://deepmind.google/about/) — Google DeepMind
- [Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsement](https://commons.wikimedia.org/wiki/File:Demis_Hassabis_in_2025_by_Christopher_Michel.jpg) — Christopher P. Michel / Cmichel67 / Wikimedia Commons
- [Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlike](https://creativecommons.org/licenses/by-sa/4.0/) — Creative Commons
- [Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claim](https://imgflip.com/memetemplate/Expanding-Brain) — Imgflip / user-uploaded meme template
- [Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claim](https://giphy.com/gifs/boomerangtoons-mad-upset-1gdkNV0hroZjOXSHOU) — Boomerang Official / GIPHY / Tom and Jerry
- [Boomerang GIF source link — uploader-provided provenance](https://boomtn.co/GIPHY) — Boomerang
- [AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claims](https://news.ycombinator.com/item?id=50439193) — Hacker News
- [Code-verification licence — Apache 2.0 for Google code, third-party licences retained](https://github.com/google-deepmind/code-verification/blob/808b4b7ffef198e6a91f71ed776d641a1c236882/LICENSE) — Google / GitHub