Google DeepMind hat zentrale Teile der Verschlüsselungstechnik von Signal mithilfe von KI-Agenten formal verifiziert. Das untersuchte System namens AlphaProof Code erstellte mathematische Spezifikationen und Beweise für den Post-Quanten-Handshake PQXDH sowie das Triple Ratchet in libsignal v0.105.4 und SPQR v1.6.0. Geprüft wurden unter anderem Vorwärtssicherheit, Authentifizierung, Post-Compromise Security und die Geheimhaltung des Handshakes.
Die Untersuchung fand keine neuen Schwachstellen in den überprüften aktuellen Protokollteilen. Bekannte, bereits behobene Fehler älterer Versionen konnte das Verfahren dagegen identifizieren. Die Arbeit ist deshalb keine neue Sicherheitswarnung und auch kein Hinweis auf beobachtete Angriffe. Sie ist der Nachweis, dass eine Kombination aus Fachleuten, KI-Agenten und einem formalen Beweissystem ausgewählte Sicherheitsgarantien bis hinunter zur Implementierung prüfen kann.
Die wichtigste Einschränkung steht allerdings direkt neben diesem Erfolg: Verifiziert wurde weder die gesamte Signal-App noch die Sicherheit jedes übertragenen Bytes unter realen Bedingungen. Das Ergebnis gilt innerhalb eines mathematischen Modells, das unter anderem perfekte kryptografische Primitive voraussetzt.
6,5 Millionen Zeilen Beweiscode für einen begrenzten Prüfbereich
AlphaProof Code ist ein Multi-Agenten-System für formale Softwarespezifikation und Verifikation. Zunächst überführten Menschen und KI-Agenten die gewünschten Sicherheitseigenschaften in eine von Fachleuten geprüfte Lean-Spezifikation. Anschließend erzeugten Gemini-Carbon-Agenten Beweise, die den Code von libsignal mit diesen Anforderungen verbinden. Der Lean-Kernel kontrollierte, ob die Beweisschritte formal gültig sind.
So arbeitet AlphaProof Code bei der Signal-Prüfung
Die Grafik zeigt den Ablauf von den ausgewählten Sicherheitszielen über die menschlich geprüfte Spezifikation und KI-generierte Beweise bis zur Kontrolle durch Lean. Ein letzter Block markiert die begrenzte Reichweite des Ergebnisses.
Der Umfang verdeutlicht, wie weit der Vorgang von einem gewöhnlichen Chatbot-Test entfernt ist: Die Agenten generierten 6,5 Millionen Zeilen Lean-Code. Ein Team aus fünf Forschern arbeitete vier Wochen an der Prüfung. Rund ein Prozent des erzeugten Codes wurde zur menschlichen Kontrolle markiert. DeepMind beschreibt das Verfahren daher ausdrücklich als Zusammenarbeit von Mensch und Maschine, nicht als autonome Sicherheitsfreigabe.
Formale Verifikation unterscheidet sich von klassischen Tests und Audits. Ein Test kann zeigen, dass sich Software in ausgewählten Situationen wie erwartet verhält. Ein formaler Beweis soll dagegen bestätigen, dass eine präzise definierte Eigenschaft unter den Annahmen des Modells generell erfüllt ist. Das ist besonders für kryptografische Protokolle relevant, deren Sicherheitswirkung aus dem Zusammenspiel mehrerer Zustände und Schlüsselwechsel entsteht.
Die Spezifikation entscheidet, was der Beweis wert ist
Der operative Engpass verschiebt sich mit leistungsfähigeren Beweisagenten. Wenn KI große Mengen formalen Codes erzeugen kann, wird die schwierigere Frage zunehmend, welche Eigenschaft überhaupt bewiesen werden soll. Eine formal korrekte Prüfung kann nur das bestätigen, was zuvor vollständig und richtig spezifiziert wurde. Fehlerhafte Annahmen, ausgelassene Angriffspfade oder Komponenten außerhalb des Modells verschwinden nicht dadurch, dass der anschließende Beweis mathematisch stimmt.
Genau deshalb blieb die menschliche Rolle in dem Projekt zentral. Die Forscher mussten die Sicherheitsziele festlegen, die Spezifikation kontrollieren und auffällige Teile der maschinell erzeugten Beweise prüfen. KI senkt hier vor allem die Kosten der Beweisproduktion. Sie ersetzt nicht die fachliche Entscheidung darüber, wo die Systemgrenzen verlaufen.
Diese Grenze relativiert auch die naheliegende Schlagzeile, Signal sei nun vollständig „bewiesen sicher“. Nicht abgedeckt sind sämtliche App-Komponenten, Betriebssysteme, Endgeräte, Benutzerkonten und alle denkbaren Implementierungs- oder Betriebsfehler. Auch die mathematische Annahme perfekter Kryptografie garantiert nicht automatisch die rechnerische Geheimhaltung konkreter Daten. Das Resultat ist belastbar für die geprüften Eigenschaften und Versionen, aber nicht beliebig auf das gesamte Produkt übertragbar.
Warum die Prüfung über Signal hinausreicht
Das Signal-Protokoll ist nicht nur für den Signal Messenger relevant. Seine Technik bildet auch eine Grundlage für verschlüsselte Kommunikation in WhatsApp und Google Messages. Damit betrifft die Qualität der untersuchten kryptografischen Mechanismen eine deutlich größere Kommunikationsinfrastruktur als eine einzelne App. Die Verifikation von libsignal bedeutet jedoch nicht automatisch, dass jede andere Integration oder Anwendung damit ebenfalls vollständig geprüft wäre.
Das Projekt ist Teil der im April 2026 gestarteten „Signal Shot“-Initiative der Beneficial AI Foundation. Deren Ziel ist es, das Signal-Protokoll und die App mit Lean formal zu verifizieren. Die DeepMind-Arbeit erfüllt davon einen wichtigen Teil, schließt die umfassendere Aufgabe aber nicht ab.
Der wirtschaftliche und technische Reiz liegt vor allem in der möglichen Senkung des Aufwands. Frühere Großprojekte formaler Verifikation erforderten jahrelange Arbeit: Für den Mikrokernel seL4 werden etwa 20 Personenjahre genannt, für den verifizierten C-Compiler CompCert sechs Jahre Entwicklungszeit. Vier Wochen für fünf Personen sind deshalb ein bemerkenswert kurzer Zeitraum – selbst wenn der geprüfte Umfang nicht direkt mit diesen Projekten vergleichbar ist und laut DeepMind erhebliche Rechenressourcen beziehungsweise Token erforderte.
Formale Sicherheit wird zur Frage des Entwicklungsprozesses
Wenn sich der Ansatz auf weitere Codebasen übertragen lässt, könnte formale Verifikation früher in die Softwareentwicklung rücken. Statt ein fertiges System nachträglich auf ausgewählte Eigenschaften zu prüfen, könnten Spezifikationen und Beweise parallel zum Entwurf entstehen. Das wäre für kryptografische Bibliotheken, Betriebssystemkomponenten und andere sicherheitskritische Software besonders wertvoll.
Die Skalierung auf gewöhnliche Unternehmenssoftware bleibt jedoch schwieriger als die reine Erzeugung weiterer Beweiszeilen. Gewachsene Anwendungen besitzen oft keine präzisen Sicherheitsziele, eindeutigen Zustandsmodelle oder sauberen Komponentengrenzen. Je unklarer das gewünschte Verhalten, desto weniger hilft ein schneller Beweisautomat.
Der eigentliche Fortschritt von AlphaProof Code liegt damit nicht in einer pauschalen Sicherheitsbescheinigung für Signal. Das Projekt zeigt vielmehr, dass KI den teuersten mechanischen Teil formaler Verifikation stark beschleunigen kann. Dadurch wird eine bislang seltene Methode praktischer – und legt zugleich offen, dass künftig nicht der Beweis allein, sondern die Qualität und Vollständigkeit der Spezifikation über den Sicherheitsgewinn entscheidet.
Jens analysiert seit Jahren digitale Märkte, Preisbewegungen und Plattform-Strategien. Als Betreiber mehrerer datengetriebener Systeme wertet er täglich große Mengen an Produkt- und Trenddaten aus. Sein Fokus liegt auf Einordnung statt Hype: Was bedeutet eine Entwicklung wirklich für Nutzer, Preise und Märkte?
