AlphaProof Code: KI beweist Signal-Verschlüsselung
Von Jörg SchockGründer · testet Smart Home seit den ersten Funksteckdosen im eigenen Haus · davor 35 Jahre in verschiedenen Funktionen der Polizei
Kurz gesagt: Google DeepMind hat mit AlphaProof Code den tatsächlich laufenden Code des Signal-Protokolls formal verifiziert: Agenten auf Basis von Gemini Carbon schrieben über sechs Millionen Zeilen Beweise in Lean, Menschen prüften nur rund ein Prozent des Codes nach. Der Ansatz ist ein Forschungsergebnis, kein Produkt für Endnutzer.
Symbolbild: KI-generiert
Google DeepMind hat am 10. November 2026 AlphaProof Code vorgestellt. Das System soll nicht nur den Entwurf einer Software prüfen, sondern den Code, der wirklich läuft. Als Prüfstück diente der Kern des Signal-Protokolls, auf dem der Messenger Signal aufbaut.
Was DeepMind gemacht hat
Nach Angaben von DeepMind erzeugten KI-Agenten auf Basis von Gemini Carbon über sechs Millionen Zeilen Beweise in der Beweissprache Lean. Menschliche Experten legen fest, was bewiesen werden soll; die Agenten führen die Beweise aus. Nur rund ein Prozent der Codebasis musste Menschen zur Nachprüfung vorgelegt werden. Der Prozess dauerte vier Wochen. Solche Aufgaben haben laut DeepMind bisher Expertenteams Jahre gekostet. Signal-Mitarbeiter gaben Feedback zur Methodik, Signals Technikchef Ehren Kret lobt den Ansatz.
Wie belastbar ist das?
Als Test führte DeepMind zwei früher behobene Fehler in eine isolierte Codeversion wieder ein. In beiden Fällen lieferte das System einen maschinell geprüften Beweis, dass diese Version unsicher ist. Neue, bisher unbekannte Fehler nennt DeepMind nicht. Benchmarks im Vergleich zur Konkurrenz gibt es keine, es existieren schlicht noch keine vergleichbaren Zahlen anderer Anbieter. Die Quelle bleibt zudem DeepMind selbst; eine unabhängige Bestätigung haben wir bislang nicht gefunden. Die Beweisartefakte sollen als Open Source erscheinen, das würde Überprüfung durch Dritte ermöglichen.
Unsere Einordnung
Das Vorhaben ist nicht aus dem Nichts entstanden: Bei der Lean-Community läuft bereits die Initiative „Signal Shot“, die das Signal-Protokoll samt Rust-Implementierung in Lean verifizieren will. Neu ist der Hebel durch KI-Agenten, der den Aufwand drastisch senken könnte.
Für dich als Nutzer in Deutschland ändert sich heute nichts: Du bekommst weder ein neues Tool noch ein Preisschild. Mittelfristig ist die Richtung aber interessant. Messenger, Smart-Home-Hubs und Router laufen auf Code mit Lücken, die Tests oft nicht finden. Mathematisch bewiesene Kernkomponenten wären ein Qualitätsmerkmal, das du künftig in Produktinformationen erwarten könntest. Wichtig bleibt die Einschränkung: Ein Beweis gilt nur für das, was spezifiziert wurde, und DeepMind betont selbst, dass die Skalierung weitere Forschung braucht.