Google DeepMind: KI hat Signal-Code verifiziert und 1 % zur Prüfung markiert
Google DeepMind zufolge hat sein Framework AlphaProof Code ausgewählte Sicherheitseigenschaften im Protokollcode von Signal formal verifiziert und innerhalb von vier Wochen mehr als sechs Millionen Zeilen Lean-Beweise erzeugt. Die Agenten markierten rund 1 % der Codebasis für eine erneute Prüfung durch Menschen. Das Ergebnis macht die routinemäßige Prüfung von Pull Requests jedoch nicht überflüssig.
- AlphaProof Code verifizierte ausgewählte Sicherheitseigenschaften in libsignal.
- DeepMind zufolge erzeugten die Agenten innerhalb von vier Wochen mehr als sechs Millionen Zeilen Lean-Beweise.
- Rund 1 % der Codebasis wurde für eine erneute Prüfung durch Menschen markiert.
- Menschliche Experten prüften jede formale Spezifikation.
- Von Agenten erzeugte Pull Requests müssen weiterhin anhand der Regeln und Anforderungen eines Teams geprüft werden.
Was AlphaProof Code geprüft hat
AlphaProof Code ist ein Multi-Agenten-Framework für die formale Verifizierung, das Google DeepMind am 10. Nov 2026 vorgestellt hat. DeepMind zufolge verifizierten die Agenten zentrale Sicherheitseigenschaften von libsignal, der Referenzimplementierung von Signal, auf Ebene des Maschinencodes. Dazu gehörten Forward Secrecy, Authentifizierung, Sicherheit nach einer Kompromittierung und Geheimhaltung des Handshakes.
Das Team arbeitete zunächst mit mehreren Modellen daran, die Sicherheitsziele von Signal in formale Spezifikationen zu übertragen. Menschliche Experten prüften jede Spezifikation. Anschließend verfassten von Gemini gesteuerte Agenten die Beweise in Lean. Der Lean-Checker akzeptiert einen Beweis nur, wenn jeder einzelne Schritt gültig ist. DeepMind zufolge prüften die Agenten die Beweise danach selbst und identifizierten Bereiche für eine menschliche Prüfung.
Das Projekt dauerte vier Wochen und umfasste laut der technischen Arbeit von DeepMind ein Team von fünf Personen. In der Arbeit heißt es: „Keiner der Autoren hat Beweiscodes geschrieben.“ DeepMind berichtet von mehr als sechs Millionen Zeilen Lean-Beweisen, während die Arbeit die Zahl mit rund 6,5 Millionen Zeilen angibt. Unterstützt wurden sie von etwa 26.000 Zeilen vertrauenswürdiger Spezifikationen und Maschinen-Semantik.
Ein Beweis hängt weiterhin von menschlichen Spezifikationen ab
Die formale Verifizierung beweist, dass der Code eine festgelegte Eigenschaft für jede Eingabe erfüllt, anstatt eine Auswahl von Eingaben zu testen. Der Beweis deckt jedoch nur die Eigenschaften ab, die in der Spezifikation enthalten sind. In der Arbeit von DeepMind heißt es: „Sobald Beweise billig werden, lautet die schwierige Frage, was bewiesen werden soll.“ Außerdem heißt es dort: „Der Großteil unserer Arbeit floss nicht in die Beweise, sondern in die Spezifikationen.“
Eine Spezifikation legt fest, was der Code garantieren muss. DeepMind zufolge kann sie nicht automatisch geprüft werden. Zu eng gefasste Annahmen können dazu führen, dass ein fehlerhaftes Programm die Spezifikation erfüllt. Die Arbeit zu Signal setzte außerdem perfekte Kryptografie voraus und verifizierte laut den Quellen nicht die vollständige Signal-App.
DeepMind berichtet, dass zwei zuvor behobene Fehler in einer isolierten Kopie des Codes erneut eingebaut wurden. In beiden Fällen zeigte ein maschinengeprüfter Beweis, dass die fehlerhafte Version unsicher war. Laut der zitierten Berichterstattung fand das Projekt in den geprüften Teilen des Protokolls keine neuen Schwachstellen.
Warum von Agenten verfasste Pull Requests weiterhin geprüft werden müssen
Das Signal-Projekt befasst sich mit einer eng abgegrenzten, sicherheitskritischen Codebasis und Spezifikationen, die von menschlichen Experten genehmigt wurden. Die meisten alltäglichen Pull Requests von Coding-Agenten verfügen nicht über eine vergleichbare formale Spezifikation. Sie müssen weiterhin anhand der Regeln eines Teams, der Anforderungen in einem Ticket und des übrigen Projektkontexts geprüft werden.
Qodo zufolge ist die Prüfung und Validierung von KI-generiertem Code für 25,8 % der Entwickler und 26,0 % der technischen Führungskräfte die wichtigste Einschränkung bei der Auslieferung. Grundlage ist die Umfrage des Unternehmens aus dem Jahr 2026. In derselben Befragung von 500 Entwicklern aus den USA und 300 technischen Führungskräften aus den USA gaben 36,4 % der Entwickler an, dass KI-generierter Code genauso viel Prüfzeit in Anspruch nimmt, aber mehr geistige Anstrengung erfordert.
Formale Verifizierung und die Prüfung von Pull Requests arbeiten daher auf unterschiedlichen Ebenen. AlphaProof Code liefert eine maschinengeprüfte Antwort zu ausgewählten Eigenschaften einer einzelnen Codebasis. Qodos Ansatz auf der PR-Ebene prüft jede Änderung anhand der REVIEW.md eines Teams, eigener Anweisungen und des verknüpften Tickets und leitet schwerwiegende Befunde an die jeweils verantwortlichen Personen weiter. Die Quelle stellt beide Methoden als Ergänzung zueinander dar: Formale Beweise können in einer kritischen Codebasis die Aufmerksamkeit der Menschen auf bestimmte Punkte lenken. Wo Anforderungen jedoch nicht als formale Spezifikationen formuliert wurden, bleibt die alltägliche Prüfung notwendig.
