Хочете будувати кар’єру в Data Science та AI? Vodafone Big Data Lab відкриває новий набір —>
Наталя ХандусенкоAI Eng
10 November 2026, 17:26
2026-11-10
Google DeepMind's AI first verified the Signal security protocol code: how it works and why it matters
Researchers at Google DeepMind have conducted a formal verification of the security of the Signal messenger. This is the first time in history that artificial intelligence has helped create a mathematical proof that connects the fundamental security guarantees of a protocol with its real-world cryptographic implementation.
To do this, the DeepMind team used the AlphaProof Code multi-agent system, built on the Lean mathematical proof language and Gemini Carbon models.
Researchers at Google DeepMind have conducted a formal verification of the security of the Signal messenger. This is the first time in history that artificial intelligence has helped create a mathematical proof that connects the fundamental security guarantees of a protocol with its real-world cryptographic implementation.
To do this, the DeepMind team used the AlphaProof Code multi-agent system, built on the Lean mathematical proof language and Gemini Carbon models.
What exactly did the artificial intelligence check?
AlphaProof Code analyzed Signal's key cryptographic mechanisms, testing the libsignal library for compliance with theoretical security requirements:
post-quantum handshake PQXDH — tested for protection against potential attacks using future quantum computers;
Triple Ratchet Protocol — verified guarantees of forward secrecy, authentication, post-compromise protection, and key exchange security.
During the study, AI agents generated 6.5 million lines of Lean code. The system then conducted an audit and identified areas that needed additional human analysis.
Hybrid approach: human + AI
The project's uniqueness lies in the synergy between researchers and artificial intelligence. Scientists formulated mathematical specifications for Signal's security goals, and Gemini Carbon agents created proofs of their correctness for machine code.
“This is a system that is fundamentally designed for human-AI collaboration. Previously, it was believed that the most difficult thing in formal methods was the verification process itself. Thanks to AI, we have learned to scale this. Now the main question is: what exactly are we verifying? And this process of formalizing requirements remains with humans,” explained Swarat Chaudhuri, a researcher at Google DeepMind and professor at the University of Texas at Austin.
Why this is a breakthrough for the industry
Traditional formal verification of complex software required enormous resources. For example, verification of the seL4 microkernel took 20 person-years, and development of the verified CompCert C compiler took 6 years.
Using AlphaProof Code allowed a team of five to fully test the Signal cryptographic protocol in just four weeks.
DeepMind notes that with the rapid development of cyberattack tools (including “offensive AI”), automated code review is becoming critically important. The company’s next step will be to apply this technology to software design — not just for cryptography, but for general software around the world.
Як нейромережі бачать вільну та незалежну Україну? Тест dev.ua
Нейронні мережі для генерації зображень бачать світ по-своєму, їхню логіку зрозуміти часом зовсім неможливо. Але таки хочеться. На честь Дня Незалежності України редакція dev.ua вирішила провести невеликий експеримент.
Ми задали чотирьом різним нейронним мережам п’ять однакових запитів: «прапор України», «День Незалежності України», «український Крим», «перемога України» та «українці». Отриманими результатами ми ділимося з вами нижче.
У TikTok тепер можна генерувати фон за допомогою нейромережі. Ми протестували її та ділимося результатами
У TikTok з’явилася нова функція «Розумний фон». З її допомогою як фон для тіктоків можна підставляти згенеровані нейромережею зображення. Редакція dev.ua протестувала цю технологію і ділиться своїми враженнями.
