Signal formal bewiesen: DeepMind prüft Kernprotokoll in 4 Wochen mit KI-Agenten

Vier Wochen, mehr als sechs Millionen Zeilen Beweiscode und ein Prozent menschliche Nachprüfung: Google DeepMind hat laut einem Blogbeitrag vom 10. November 2026 zentrale Sicherheitseigenschaften des Signal-Protokolls mit KI-Agenten mathematisch bewiesen. Geprüft wurde der kompilierte Kryptografie-Kern und nicht die gesamte Signal-App, wie Ars Technica am 11. November 2026 unter Berufung auf WIRED berichtet. Was die Analyse gekostet hat, will Google nicht sagen.

Was DeepMind am Signal-Protokoll in 4 Wochen bewiesen hat

DeepMind hat laut eigenem Blog bewiesen, dass der kompilierte Code des Signal-Protokolls die von Fachleuten festgelegten Sicherheitseigenschaften erfüllt, bis hinunter zum Code auf den Geräten. Formale Verifikation, also der mathematische Nachweis, dass Software exakt tut, was spezifiziert ist, gilt dort als höchster Standard der Sicherheitsprüfung. Zu den bewiesenen Eigenschaften zählt, dass Nachrichten vor und nach einer vorübergehenden Kompromittierung eines Geräts geschützt bleiben. Die meisten Protokollprüfungen enden nach DeepMind-Angaben auf der Ebene des Entwurfs, während reale Schwachstellen oft in der Lücke zwischen Entwurf und Umsetzung stecken.

Das Protokoll schützt laut Ars Technica die Kommunikation in der Signal-App, in Google Messages und in WhatsApp. WhatsApp führte es laut WIRED 2014 ein und aktivierte es zwei Jahre später standardmäßig für alle Nutzenden. Technisch setzt das Verfahren auf einen sogenannten Ratchet-Mechanismus, der nach jeder Nachricht einen neuen Schlüssel erzeugt. Die Eigenschaft heißt Perfect Forward Secrecy. Wird ein Telefon zu einem Zeitpunkt X gestohlen, bleiben vorher gesendete Nachrichten geschützt, erklärte der Kryptograf Matthew Green von der Johns Hopkins University 2020 gegenüber WIRED.

DeepMind beansprucht zwei Premieren. Nach eigener Darstellung hat erstmals eine KI ein weit verbreitetes Kryptoprotokoll in dieser Tiefe formal verifiziert. Zugleich sei die Implementierung eines solchen Protokolls bisher mit keiner Methode bewiesen worden, ob mit oder ohne KI. Für vergleichbare Aufgaben brauchten Fachteams laut DeepMind bislang Jahre.

Tipp: Vorwärtssicherheit nützt laut WIRED wenig, solange alte Chats auf einem gestohlenen Telefon liegen; schalten Sie in Signal deshalb verschwindende Nachrichten ein, wenn dieses Risiko für Sie realistisch ist.

6 Millionen Zeilen Lean, 1 Prozent Handprüfung: So arbeitet AlphaProof Code

AlphaProof Code ist ein agentisches Framework, in dem mehrere Sprachmodelle Teilaufgaben selbstständig abarbeiten und das die formale Verifikation laut DeepMind wie ein Forschungsteam aufteilt. Menschen legen gemeinsam mit der KI fest, was bewiesen werden soll. Eine Gruppe von KI-Agenten führt anschließend die Beweise. Im ersten Schritt übersetzten die Forschenden die Sicherheitsziele des Messengers mit mehreren Modellen in formale mathematische Spezifikationen, und menschliche Fachleute prüften jede einzelne davon.

Die Beweise selbst schrieben Agenten auf Basis des Modells Gemini Carbon. Sie erzeugten mehr als sechs Millionen Zeilen Lean, einer Sprache, in der Computer mathematische Beweise Schritt für Schritt nachprüfen. Danach auditierten die Agenten ihren eigenen Beweis und markierten Stellen, die ein Mensch noch einmal ansehen sollte. Laut DeepMind betraf das nur ein Prozent der Codebasis. Den Rest kontrolliert Lean automatisch.

Zum Vergleich: Bei klassischer Verifikation mussten Menschen laut WIRED die gewünschten Eigenschaften einer Software beschreiben, in Formeln übersetzen und den Beweis selbst entwickeln. Agentische KI verkürzt vor allem den letzten Schritt. Swarat Chaudhuri, Forscher bei DeepMind, nennt das Verfahren gegenüber WIRED einen „Mensch-KI-Kollaborationsprozess“, in dem Agenten fast überall mitarbeiten und sich selbst korrigieren. Eine „Vibe-Welt“, in der KI die Ziele vorgibt, die Beweise erzeugt und sich ihre Tests selbst schreibt, wolle man ausdrücklich nicht. „Es gibt einen Mittelweg“, sagt Chaudhuri.

Die Arbeitsteilung verschiebt das Vertrauen von der KI auf die Spezifikation, weil Lean jeden Beweisschritt nachrechnet, gleich wer ihn geschrieben hat. Befürwortende bezeichnen formale Verifikation laut Ars Technica seit Langem als eine Art heiligen Gral der Softwaresicherheit, weil sie per Mathematik prüft, ob Software wie vorgesehen funktioniert. Dieselbe Sprache nutzt auch OpenAI, das zuletzt einen agentisch erzeugten Lean-Beweis zu den Navier-Stokes-Gleichungen vorgelegt hat.

2 eingebaute Altfehler als Gegenprobe: Wie belastbar der Signal-Beweis ist

Die Gegenprobe mit zwei echten, längst behobenen Signal-Fehlern soll laut DeepMind zeigen, dass AlphaProof Code korrekten von fehlerhaftem Code unterscheidet. Die Forschenden bauten beide Fehler in eine isolierte Version des Codes wieder ein. In beiden Fällen lieferte das System einen maschinell geprüften Beweis, dass die fehlerhafte Version unsicher ist. Neue Lücken fanden die Agenten nicht.

Dieses Bild wurde mit KI generiertProviderhiggsfieldModellgpt_image_2_5 flare high 1k 16:9PromptPaper cut collage, top-down view on layered handmade paper. In the center a cut-out smartphone with a blue speech-bubble messaging icon, resting on long horizontal ribbons of cream paper strips that represent lines of formal proof code, with the word "Lean" on a small tag. Two small red paper-cut bug shapes are pinned onto the ribbons, each marked with a torn orange warning flag, while a green paper checkmark stamp sits beside them. Tactile paper texture, visible cut edges, soft drop shadows between layers. Palette of navy, cream, blue, with red and green accents. No people, no hands. No watermark, no signature.

Unter dem Ars-Artikel wenden Lesende ein, die Modelle könnten die Geschichte der Signal-Fehler aus ihren Trainingsdaten kennen. Andere Lesende halten dagegen, die Gegenprobe habe die bekannten Fehler immerhin gefunden. Der Einwand trifft die Aussagekraft der Gegenprobe. Den Beweis selbst rechnet Lean unabhängig nach.

Der Haken liegt in den Annahmen, auf denen jeder formale Beweis ruht. Ein Forumsmitglied zitiert im Ars-Forum aus dem technischen Paper, das Ergebnis stütze sich auf rund 26.000 Zeilen vertrauenswürdiger Spezifikationen und AArch64-Semantik, also ein formales Modell der 64-Bit-ARM-Architektur. Ist eine dieser Annahmen falsch, beschreibt der Beweis ein Modell, das an der Realität vorbeigeht. Die folgende Tabelle zeigt, welche Bereiche die Prüfung abdeckt, voraussetzt oder ausklammert.

Für Fehler oberhalb des Protokolls, etwa die Lücke, durch die Signal-Anrufe nach dem Auflegen weiterlaufen konnten, trifft der Beweis keine Aussage. Frühere und spätere Nachrichten bleiben laut dem im Ars-Forum zitierten Paper selbst dann geschützt, wenn Langzeitschlüssel oder der gesamte Zustand eines Nutzenden offengelegt sind. Für einige Ausnahmefälle vermerkt das Autorenteam demnach, dass ein Angriff trivial wäre.

Einen Vorsprung hatte das Team laut WIRED durch frühere Verifikationsarbeiten der Signal Foundation. Deren Technikchef Ehren Kret erklärt, frühere formale Verifikation habe sich auf kleinere Teile des Codes konzentriert, der Ansatz von DeepMind erlaube eine deutliche Ausweitung. Dass KI-Agenten laufenden Code in gültige Lean-Theoreme übersetzen, nennt Kret im DeepMind-Blog einen großen Durchbruch. Angesichts wachsender KI-gestützter Bedrohungen gebe ihm der rigorose Beweis noch mehr Vertrauen in die Datenschutzzusagen des Codes.

Gratis für Signal, Preis offen: Was 4 Wochen Beweisarbeit über die Rendite sagen

Die Wirtschaftlichkeit KI-gestützter formaler Verifikation bleibt nach dem Signal-Projekt offen, weil Google laut WIRED keine Kosten nennt. DeepMind führte die Analyse als Forschungsprojekt kostenlos durch. Ob ein kommerzielles Produkt oder ein Dienst folgen soll, kommentierte Google nicht. Ob sich der Ansatz zu tragbaren Kosten skalieren lässt, nennt WIRED die offene Frage der gesamten Tech-Branche.

Pushmeet Kohli, Chefwissenschaftler von Google Cloud und Forschungs-Vizepräsident bei DeepMind, denkt dabei ausdrücklich an Banken. Unternehmen, die auf Zusicherungen angewiesen sind und Fehler fürchten, könnten künftig sagen: „Ich kann diese Eigenschaften beweisen“, so Kohli gegenüber WIRED. Wer die Korrektheit solcher Implementierungen nachweisen könne, dürfe beruhigt sein, sagt er. Kryptoprotokolle tragen laut DeepMind fast die gesamte digitale Kommunikation, vom Online-Banking bis zum Surfen im Netz. Ein einzelner Fehler kann demnach Millionen Menschen zugleich treffen.

Für eine Bank ist dieser Satz nur so viel wert wie die Kalkulation dahinter. Die Rendite eines Beweises ergibt sich aus den Prüfkosten im Verhältnis zu den vermiedenen Schäden, und für die erste Größe liefert Google keinen einzigen Euro-Betrag. Signal hat für die Prüfung nichts bezahlt. Das nächste Institut, das anfragt, kennt nicht einmal die Größenordnung.

Auch die Reichweite ist begrenzt. Bis man den Ansatz auf alle Software der Welt übertragen könne, sei es noch ein weiter Weg, sagt Chaudhuri. DeepMind schreibt selbst, die Skalierung erfordere weitere Forschung. Als nächste Ziele nennt das Unternehmen Firmware für Medizingeräte und Software für Stromnetze, kombiniert mit automatischen Abwehragenten wie CodeMender, einem KI-Agenten für Codesicherheit, den DeepMind im Oktober 2025 vorgestellt hat.

1 Beweis zum Nachrechnen: Was nach dem Signal-Projekt als Nächstes ansteht

DeepMind gibt die für Signal entwickelte Spezifikation und den Beweis als Open Source frei, damit andere Teams ihre eigene Verifikationsarbeit darauf aufbauen können. Das technische Paper ist ebenfalls veröffentlicht. Fachleute außerhalb von Google können den Lean-Beweis damit konkret selbst durchlaufen lassen. Wenn Sie Sicherheitsprüfungen verantworten, sehen Sie dort auch, welche Annahmen im vertrauten Teil der Spezifikation stecken.

Das Feld wird voller. Auf arXiv beschreiben andere Gruppen verwandte Ansätze, darunter einen Erfahrungsbericht zu einer Pipeline, die Rust-Code nach Lean überträgt und von KI-Beweisern prüfen lässt. Ein weiteres Paper behandelt neuro-symbolische Beweiserzeugung, also die Kombination aus Sprachmodellen und regelbasierter Logik, für Systemsoftware. Google selbst schickt einen Theorembeweiser gegen KI-geschriebene Sicherheitsregeln.

Der nächste belastbare Schritt liegt bei Dritten. Ob AlphaProof Code außerhalb von DeepMind trägt, zeigt sich, sobald eine unabhängige Gruppe die freigegebenen Signal-Artefakte nachrechnet oder das Verfahren auf ein zweites, weit verbreitetes Protokoll anwendet.