Google DeepMind hat gestern AlphaProof Code vorgestellt, einen agentischen Rahmen für formale Verifikation, und damit zentrale Sicherheitseigenschaften des Codes bewiesen, der hinter dem Signal-Protokoll steckt. Das ist die Technik, die Unterhaltungen in Signal und in Google Messages absichert.
Was daran neu ist
Protokolle dieser Art werden seit Jahrzehnten formal analysiert, aber fast immer auf der Ebene des Entwurfs. DeepMind hat die Implementierung bewiesen: dass der kompilierte Code die Sicherheitseigenschaften erfüllt, bis zu dem, was tatsächlich auf den Geräten läuft. Darunter die Garantie, dass Nachrichten geschützt bleiben, bevor und nachdem ein Gerät zeitweise kompromittiert war.
Das ist nach eigener Darstellung zweimal ein erstes Mal: das erste Mal, dass KI ein weit verbreitetes kryptografisches Protokoll in dieser Tiefe formal verifiziert hat – und das erste Mal überhaupt, dass die Implementierung eines solchen Protokolls formal verifiziert wurde, mit oder ohne KI. Echte Lücken sitzen meistens genau dort, wo Entwurf und Implementierung auseinandergehen.
Wie die Arbeit verteilt war
AlphaProof Code ist ein Rahmen mit mehreren Modellen, der die Verifikation so aufteilt, wie ein Forschungsteam es täte. Zuerst haben Forscher gemeinsam mit verschiedenen Modellen Signals Sicherheitsziele in formale Spezifikationen übersetzt, jede einzelne von Fachleuten geprüft. Dann haben Agenten auf Gemini Carbon die Beweise geführt und dabei über sechs Millionen Zeilen Lean erzeugt.
Anschließend haben die Agenten den Beweis selbst auditiert und markiert, was ein Mensch ansehen sollte: ein Prozent der Codebasis. Den Rest prüft Lean automatisch. Der ganze Vorgang dauerte vier Wochen – eine Aufgabe, für die Expertenteams bisher Jahre gebraucht haben.
Als Gegenprobe haben die Forscher zwei echte, längst behobene Fehler in eine isolierte Fassung von Signals Code zurückgebaut. Das System hat beide erkannt.
Zwei Agentenschwärme, zwei Ziele
Vor zwei Tagen stand hier, wie tausend Claude-Agenten Fermats letzten Satz in Lean formalisiert haben, in 28,7 Stunden. Jetzt kommt derselbe Aufbau von Google, mit derselben Beweissprache, und richtet sich auf ein Stück Software, das auf Milliarden Geräten läuft.
Interessant ist der Unterschied in der Rollenverteilung. Bei Anthropic war die Mathematik das Ziel und die Agentenzahl das Mittel. Bei DeepMind bleibt der Mensch im Zentrum der Spezifikation – was bewiesen werden soll, entscheiden Fachleute, und jede Spezifikation wird von Hand abgenommen. Beweisen ist dann die Fließarbeit. Das ist die vernünftigere Aufteilung für Sicherheitsarbeit: Ein Beweis für die falsche Eigenschaft ist kein Fortschritt, sondern ein gut belegter Irrtum.