Google DeepMind 10 листопада 2026 року представила AlphaProof Code: система за чотири тижні довела 10 властивостей безпеки криптографічного ядра Signal. Зазвичай така робота займає роки.
Для білдера цікаво, де тепер вузьке місце. Докази пише ШІ, а людям лишається специфікація. Довірена база, яку мають перевіряти люди, становить близько 26 000 рядків, і її звіряють ревʼю-агент та криптографи.
Що саме перевірили в Signal?
AlphaProof Code перевірив скомпільований машинний код, а не вихідний Rust. Ціллю стали libsignal-protocol 0.105.4 і SPQR 1.6.0 (розширення для постквантової криптографії), зібрані компілятором rustc 1.98.1 під AArch64 на Linux, за даними XenoSpectrum. Бінарник важить близько 560 КБ, це приблизно 140 000 інструкцій.
Охоплено встановлення сесії через PQXDH у листуванні один на один і роботу протоколу Triple Ratchet. Серед 10 доведених властивостей: forward secrecy, post-compromise security, автентифікація рукостискання та стійкість до атак KCI.
Перевірка бінарника має практичну вигоду: помилки компілятора й оптимізацій більше не входять у довірену базу, бо доказ стосується коду, який реально виконується.
Як розподілили роботу між ШІ та людьми?
Експерти формалізували вимоги до безпеки, а агенти на базі Gemini Carbon написали докази мовою Lean. За даними The Decoder, обсяг склав понад 6 млн рядків, приблизно 1% кодової бази агенти позначили для перевірки людьми, а два навмисно підкладені баги система знайшла одразу.
XenoSpectrum називає модель Gemini 4 Carbon і дає точнішу цифру: близько 6,5 млн рядків доказів, майже 7 млн разом із супутнім матеріалом.
Докази проходять через «gatekeeper», який звіряє їх зі схваленими людьми визначеннями, а далі через ядро Lean. Довірена база становить близько 26 000 рядків: 18 000 рядків визначень, залежних від специфікації, і 8 000 рядків семантики інструкцій AArch64.
Чого ця верифікація не гарантує?
Верифікація не гарантує безпеку всього застосунку Signal. Перевірено один Linux-бінарник, зібраний з конкретної бібліотеки та тестової обв'язки, а докази спираються на криптографічні припущення й жорсткі умови середовища виконання.
The Decoder описує результат як перевірку коду, що працює на пристроях користувачів, а XenoSpectrum наголошує на вузькому обсязі й одній збірці.
Друге обмеження стосується специфікації. Якщо в ній немає якогось шляху атаки, математично бездоганний доказ усе одно не покаже, що реальне ПЗ безпечне. Ймовірно, саме якість і аудит специфікації будуть ключовим питанням до подібних проєктів.
Заява про «першу» механічну верифікацію такого рівня належить самій DeepMind: це не висновок третьої сторони після порівняння з попередніми роботами. CTO Signal Ehren Kret каже, що підхід посилює довіру до приватності даних на тлі зростання загроз від ШІ. DeepMind планує поширити метод на енергомережі та медичні пристрої через системи на кшталт CodeMender.
