# AlphaProof Code и Signal: проверени машинно-кодови доказателства за сигурност и доверени допускания

Published: 2026-11-11

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

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

## Какво обхваща този видеоклип

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

## Въпроси и отговори

### Какво доказа AlphaProof Code за имплементацията на Signal?

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

### Кой решава какво трябва да установи генерираното от AI доказателство за сигурност?

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

### Защо да се проверява компилиран машинен код, вместо да се доверява на компилатора Rust?

Доказателство за компилирания бинарен файл установява директно посочените свойства за този артефакт. Документът на Google DeepMind обяснява, че грешка в компилатора, която нарушава едно от тези свойства, би направила теоремата невярна. Следователно компилаторът Rust напуска доверената база за това твърдение. Доказателството все още се доверява на модела на инструкциите, ядрото на Lean и посочените криптографски договори.

### Как компараторът спира агент за доказване да отслаби своята цел?

Компараторът проверява теоремата и всяка дефиниция, от която зависи, спрямо защитена одобрена спецификация. Документът на Google DeepMind казва, че агентите за доказване не могат да пишат в това скрито копие. Проверяващият също така проверява разрешените аксиоми и преиграва доказателството в свежо ядро. Предложените изменения на спецификацията следват отделен процес на преглед, докато хората остават отговорни за силата на целта.

### Каква беше присъдата на The Daily Diff за работния процес на провереното доказателство?

Присъдата на The Daily Diff беше SHIP IT. Нико би приел работния процес на провереното доказателство, защото одобреното твърдение остава отделено от агента, който произвежда отговора. Той би запазил обхвата и допусканията прикрепени към всеки резултат. Епизодът отразява публикувания доказателствен артефакт на Google, без да го преизгражда независимо, и одобрява работния процес в рамките на тези граници на доказателствата.

## Глави

- 0:00 Кой проверява доказателство за сигурност на AI?
- 0:57 Как една претенция става цел за доказване?
- 1:39 Защо да се доказва компилираният бинарен файл?
- 2:16 Кои свойства за сигурност оцеляха при пропастта в имплементацията?
- 2:59 Може ли спецификацията да отхвърли счупен код?
- 3:36 Може ли коректно доказателство да отговори на грешен въпрос?
- 4:13 Какво улавя променящите се цели?
- 4:53 Бих ли използвал този работен процес за доказване?

## Преведен препис

Преведено от оригиналния английски разказ. Наличните аудио и субтитри се контролират от YouTube.

### Кой проверява доказателство за сигурност на AI?

0:00 Одитът за сигурност на AI все още звучи като доверяване на чатбот. Новият резултат на Google за Signal идва с математически доказателства, отделно ядро проверява. В това видео, какво доказа Google? И как спират агент да променя целите? Ето полезния отговор. Моделите пишат кандидат-доказателства, а Lean проверява доказателствата спрямо одобрена от човека претенция за избран компилиран код. Хората все още притежават претенцията и допусканията.

0:21 Можете да проверите резултата, без да вярвате на победната реч на модела. Отделна проверка улавя тихото променяне на въпроса. Ще го проследим до дефинициите. Вторник, десети ноември е, и това е The Daily Diff. AlphaProof Code е рамката на Google за писане на софтуерни спецификации с човешко ръководство и генериране на проверени доказателства с AI агенти. Това проучване цели libsignal, библиотеката на Rust, имплементираща протокола за съобщения на Signal, във вътрешността на конкретна програма от командния ред.

0:45 Google обяви работата днес. В статията се казва, че петима изследователи са работили над четири седмици. Агентите написаха доказателствата, докато хората прекараха по-голямата част от усилията си върху спецификациите. Изискванията са намерили начин да станат още по-скъпи срещи. Спецификацията казва какво трябва да прави програмата,

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

0:59 какво контролира атакуващият и какви допускания са необходими за аргумента. Рецензентите питат дали тя улавя сигурността, която е важна за хората. Красиво проверен отговор на слаб въпрос оставя този въпрос непокътнат. Екипът надгражда по-ранни изследвания на ръкостискането на Signal и неговия ключ за съобщения ratchet. Формалните анализи вече са изследвали тези дизайни. Твърдението на Google свързва техните аргументи за сигурност с непроменена производствена компилирана имплементация на библиотека, където дизайнът трябва да оцелее при контакт с действителен код. Техническият директор на Signal, Ерен Крет,

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

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

1:41 компилатор в Arm 64 Linux изпълним файл. Техните теореми описват този бинарен файл, използвайки формален модел на инструкциите, преминавайки през пропастта между изходния и оптимизирания машинен код. Грешка в компилатора, която нарушава дадено свойство, би направила теоремата му невярна. Следователно компилаторът напуска доверената база за този бинарен файл. Все още се доверявате на модела на инструкциите и на проверката на Lean. Границата на доверие се е преместила и има адрес. Около шест милиона и половина реда проверено доказателство се основават на приблизително двадесет и шест

2:06 хиляди доверени спецификационни и инструкционни семантични реда. Това са бройки на артефакти. Третирането им като интелигентност е като класирането на разработчици по размера на папката им с node модули.

### Кои свойства за сигурност оцеляха при пропастта в имплементацията?

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

2:42 И двете имат ограничения за сценариите, които обхващат. Питайте за коя версия, кое свойство и какви допускания. Този резултат се отнася до командния инструмент на изследователите. Груповите съобщения са бъдеща работа, а изчислителният модел изключва състоянието на няколко устройства. Наричането на всяка инсталация на Signal безгрешна излиза извън теоремата. Изследователите повторно въведоха две по-рано отстранени грешки в Signal в

### Може ли спецификацията да отхвърли счупен код?

3:02 изолирани копия и ги компилираха. Проверени доказателства показаха, че тези бинарни файлове нарушават символичната теорема за сигурност. Това тества дали спецификацията може да отхвърли реални счупени имплементации. Вашата зелена отметка се нуждае от червен тест. Google публикува спецификациите и доказателствата с инструкции за проверка. Хранилището казва, че чистото изграждане отнема часове и значителна памет. Четенето на съобщението е значително по-лесно на лаптопа. Хардуерният модел и доверените договори все още се нуждаят от преглед.

3:26 Не съм преизградил огромния артефакт за този епизод. Ние докладваме публикувания резултат и неговите граници. Външни лица имат път да го инспектират, което е по-важно за мен от още един AI кръг на победа. Сега капанът.

### Може ли коректно доказателство да отговори на грешен въпрос?

3:36 Lean може да приеме коректно доказателство на твърдение, което почти нищо не изисква. Невъзможни допускания могат да направят една теорема безсмислена. Променянето на дефиниция, скрита под основната теорема, може да отслаби целта. Документът проектира проверки срещу това. Пазителят поддържа скрита одобрена спецификация, в която агентите за доказване не могат да пишат. Те могат да предлагат корекции чрез отделен процес на изменение. Отслабването на сигурността се ескалира като потенциална грешка. Декларацията за успех на доказващия няма власт тук.

4:00 Хората отсъждат промени в доверени допускания, директно или чрез тяхната политика, и преглеждат измененията след всяка кампания. Експертната преценка остава отговорна. Агентът може да поиска друго назначение. Не може да си даде преминаваща оценка.

### Какво улавя променящите се цели?

4:13 Ето обещаната проверка. Компараторът на Lean сравнява теоремата и всяка дефиниция, от която зависи, с това защитено одобрено копие. Той също така проверява разрешените аксиоми и преиграва доказателството в свежо ядро. Тихото отслабване на помощна дефиниция следователно променя това, което се сравнява. Приетото доказателство трябва да установи одобрената цел. Това все още оставя хората отговорни за избора на силна цел и честни допускания. За вашия собствен работен процес на AI, дръжте критериите за приемане извън

4:37 разрешенията за редактиране на работника и преглеждайте предложените промени отделно. Резултатът на Google прави това разделение конкретно. Авторът на доказателството върши работата; границата на проверката решава дали тя се брои. Ако предпочитате да прочетете това, отколкото да ме чуете да го казвам, разликата пристига във вашата входяща кутия всяка сутрин, безплатно на thedailydiff.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