{"data":{"id":2678,"lang":"en","title":"Google DeepMind Uses AI to Formally Verify the Signal Protocol, Producing 6.5 Million Lines of Proofs in Four Weeks","summary":"DeepMind's AlphaProof Code produced machine-checked proofs of Signal's core security properties, though only for one-to-one chats.","category":"ai","category_label":"AI","published_at":"2026-11-12T15:01:26Z","updated_at":"2026-11-12T15:01:26Z","url":"https://techtools.cz/tools/news/article/2678-google-deepmind-uses-ai-to-formally-verify-the-signal-protocol-producing-6-5","api_url":"https://techtools.cz/news-api/v1/articles/2678?lang=en","markdown_url":"https://techtools.cz/news-api/v1/articles/2678.md?lang=en","image_url":"https://images.unsplash.com/photo-1677442136019-21780ecad995?w=800","word_count":150,"reading_time_minutes":1,"sources":[{"url":"https://www.theneuron.ai/news/google-ai-math-signal-security-verification/","domain":"theneuron.ai"},{"url":"https://github.com/google-deepmind/code-verification","domain":"github.com"}],"translation":{"lang":"cs","id":2752,"title":"Google DeepMind formálně ověřil protokol Signal pomocí AI: 6,5 milionu řádků důkazů za čtyři týdny","url":"https://techtools.cz/tools/news/clanek/2752-google-deepmind-formalne-overil-protokol-signal-pomoci-ai-6-5-milionu-radku","api_url":"https://techtools.cz/news-api/v1/articles/2752?lang=cs"},"content":"Google DeepMind has used a new system called AlphaProof Code to produce machine-checked mathematical proofs of security properties in the Signal messaging protocol. Announced on November 10, the work covered message confidentiality, authentication, forward secrecy and post-compromise security, and the proofs are checked by the Lean proof system, including about 140,000 instructions of compiled machine code.\n\nFive researchers generated roughly 6.5 million lines of proofs in four weeks, work that has historically taken specialist teams years. To test the method, DeepMind reinserted two previously fixed Signal vulnerabilities into test versions, and the system produced proofs showing both modified versions violated their security requirements.\n\nThe scope is limited: only one-to-one conversations were covered, not group messaging, multi-device use or the whole mobile app, and a proof only checks the requirements it is given. Google has published the proofs and specifications on GitHub, and says there is no commercial service yet."}}