Google DeepMind gab am 10. Nov. 2026 bekannt, dass sein neues KI-Framework AlphaProof Code verwendet wurde, um den tatsächlichen Code des Signal-Protokolls formal zu verifizieren. Bei einer formalen Verifikation wird mathematisch bewiesen, dass Software genau wie vorgesehen funktioniert und keine verborgenen Fehler enthält. Das Team leitete KI-Agenten dabei an, einen Beweis zu erstellen und zu prüfen, dass der kompilierte Signal-Code zentrale Sicherheitsgarantien einhält – etwa dass Nachrichten geschützt bleiben, selbst wenn ein Gerät vorübergehend kompromittiert wird. Die gesamte Arbeit dauerte vier Wochen. Expertenteams würden dafür normalerweise Jahre benötigen.
Was AlphaProof Code macht
AlphaProof Code ist ein agentisches System aus mehreren LLMs (Large Language Models, großen Sprachmodellen). Menschliche Forschende übersetzen zunächst Signals Sicherheitsziele in formale Spezifikationen und prüfen jeden Schritt. Anschließend erstellt eine Gruppe von Agenten, die auf DeepMinds Modell Gemini Carbon basiert, den Beweis in Lean, einer Sprache zur Überprüfung mathematischer Theoreme. Die Agenten erzeugten mehr als sechs Millionen Zeilen Lean-Code und markierten nur etwa ein Prozent der Codebasis für eine menschliche Prüfung. Das System erkannte außerdem zwei zuvor behobene Fehler korrekt wieder, als diese erneut eingebaut wurden. Das zeigt, dass es sicheren von fehlerhaftem Code unterscheiden kann.
Warum das wichtig ist
Die Verifikation umfasst die kompilierte Implementierung und nicht nur den Entwurf. Damit wird eine Lücke geschlossen, in der sich viele Schwachstellen aus der Praxis verbergen. Signals Chief Technology Officer Ehren Kret sagte, das Ergebnis schaffe „größeres Vertrauen in die Datenschutzgarantien unseres Codes“. Fachleute sehen darin einen Schritt hin zum Einsatz von KI, um Banken, medizinischen Geräten, Software für Stromnetze und anderen kritischen Systemen ein Höchstmaß an Sicherheit zu bescheinigen.
Warum es wichtig ist
Für Nutzer im Alltag bedeutet die Arbeit, dass die Verschlüsselung, die Milliarden Nachrichten in Signal und Google Messages schützt, auf Implementierungsebene mathematisch überprüft wurde. Das verringert das Risiko verborgener Schwachstellen. Für Entwickler zeigt sie einen praktikablen Weg, KI-gestützte formale Verifikation einzusetzen und Sicherheitsprüfungen zu beschleunigen. Wie gut sich das Verfahren skalieren lässt und welche Kosten damit verbunden sind, ist allerdings noch unklar.
