AlphaProof-Code bewies, dass Signals Krypto korrekt ist – auf der Ebene der kompilierten Binärdatei

Sechseinhalb Millionen Zeilen Lean, produziert in vier Wochen, von Agententeams, bei deren Schreiben kein Mensch geholfen hat. Das ist die Schlagzeile, die G​oogle DeepMind am 10. November 2026 für AlphaProof Code veröffentlichte, ein agentisches Framework für formale Verifikation, mit dem das Labor den kryptografischen Kern des Signal-Protokolls maschinell überprüft hat – und, ungewöhnlicherweise, auf der Ebene des kompilierten AArch64-Binaries statt des darüberliegenden Entwurfsdokuments. Die Modelle, die die Arbeit erledigten, sind eine andere Frage. ein API-Schlüssel beim Anbieter zum Listenpreis mit 0 % Aufschlag Die Engine der Proof-Agenten ist nichts, was wir anbieten.

Das Framework ist kein Modell, das man aufrufen kann. Es ist ein Rahmenwerk: Menschliche Expertinnen und Experten entscheiden, was gelten muss, eine Mischung aus Modellen verwandelt diese Ziele in Lean-Spezifikationen, und dann füllen Teams von beweisschreibenden Agenten – der Blogbeitrag nennt G​emini Carbon als Engine – die Beweise aus, bis der Lean-Kernel sie akzeptiert. Zusammen mit der Ankündigung wurden die Artefaktsammlung unter github.com/google-deepmind/code-verification und ein technisches Paper veröffentlicht, das weit offener über die Grenzen des Ergebnisses spricht als der Blogbeitrag. Das Meiste im Folgenden stammt aus diesem Paper, denn dort finden sich die interessanten Zahlen.

Was wurde tatsächlich bewiesen, und wogegen?

Das Ziel ist libsignal v0.105.4 mit spqr v1.6.0, gebaut mit Standard-rustc 1.98.1, statisch gegen musl gelinkt und als einzelne ausführbare AArch64-Linux-Datei erzeugt. Dieses Detail ist wichtiger als jeder Benchmark: Die Beweise betreffen die Bytes, die auf einem Telefon laufen würden, nicht eine Rust-Funktion, von der man annimmt, dass ein Compiler sie getreu übersetzt. Das Team verifizierte etwa 560 KB libsignal-Quellcode, ungefähr 140.000 AArch64-Instruktionen, und tat dies, indem es ein Lean-Modell des Befehlssatzes schrieb – 467 Instruktionen und 31 Systemaufrufe in 7.578 Zeilen – und dann bewies, dass das reale ELF-Abbild, geladen und unter diesem Modell ausgeführt, die Sicherheitseigenschaften bewahrt.

Die Eigenschaften sind die, nach denen ein Protokollentwickler fragen würde. Zehn symbolische Theoreme decken Forward Secrecy, Post-Compromise Security, Initiator- und Responder-Geheimhaltung, Authentifizierung sowie fünf Korollare von PQXDHs Theorem 1 ab. Das Hauptergebnis heißt signal_session_secure_placed. Außerdem gibt es einen rechnerischen Zweig mit einer konkreten Schranke, und die beiden Zweige verwenden unterschiedliche Angreifermodelle: Die symbolische Seite (Dolev–Yao, über das DyLean-Framework) deckt sogar einen Quantenangreifer ab, der Diffie–Hellman nach dem Handshake bricht, während die rechnerische Seite nur klassische Angreifer abdeckt.

Wohin die sechs Millionen Zeilen gehen

„Über sechs Millionen Zeilen“ ist die Formulierung des Blogs, und sie ist korrekt, aber grob. Die Aufschlüsselung im Paper ist die nützliche, und es lohnt sich, sie als Kostentabelle zu lesen statt als Prahlerei:

• Beweise für das Binärprogramm — 5,3 Millionen Zeilen, der Großteil der Arbeit, die die Maschinencode-Semantik und die Verfeinerung vom symbolischen Modell bis hinunter zum ausführbaren Programm abdecken.

• Rechnergestützte Beweise — etwa 860.000 Zeilen.

• Symbolische Beweise — etwa 350.000 Zeilen.

• Fehlerwiderlegungsbeweise — etwa 140.000 Zeilen, für die beiden absichtlich wieder eingeführten Schwachstellen, die unten beschrieben sind.

• Allokator-Beweise — etwa 70.000 Zeilen.

Fast sieben Millionen Zeilen, wenn man Kommentare und Leerzeilen mitzählt, was das Paper tut und der Blog nicht. Wie auch immer, das entscheidende Verhältnis ist das zwischen dem Beweis und dem Bewiesenen: 6,5 Millionen Zeilen Lean, um Eigenschaften einer 560-KB-Binärdatei nachzuweisen. Dieses Verhältnis ist das ehrliche Maß dafür, wie weit diese Technik von Routine entfernt ist, und es ist die Zahl, die man zitieren sollte, wenn jemand fragt, ob formale Verifikation billig geworden ist.

Die vertrauenswürdige Basis ist kleiner als der Beweis, und genau das ist der Punkt.

Ein Beweis ist nur so gut wie seine Annahmen. Das Papier ist diesbezüglich präzise, und diese Präzision unterscheidet es von einer Pressemitteilung. Die vertrauenswürdigen Spezifikationen umfassen etwa 18.000 Zeilen (28.000 mit Dokumentation), die AArch64-Semantik etwa 8.000 und die Lean-Kodierung des Maschinencodes rund 95.000. Siebenunddreißig Routinen werden durch Verträge ersetzt statt verifiziert – SHA-256- und SHA-512-Kompression, AES-256-CBC, X25519, die Edwards-Kurven-Operationen, Kyber1024 und ML-KEM-768 sowie libcrux HMAC. Achtzehn Panic-Einstiegspunkte werden ebenfalls angenommen statt bewiesen.

Die Behauptung lautet also nicht „alles ist bewiesen“. Die Behauptung ist, dass die Logik des kryptografischen Protokolls, die Zustandsmaschine der Sitzung und die Verfeinerung von dieser Logik zu den tatsächlich ausgeführten Anweisungen bewiesen sind, während den darunterliegenden Primitiven auf dieselbe Weise vertraut wird, wie jedes Verifikationsprojekt seinen Primitiven vertraut. Der Rust-Compiler ist insbesondere nicht Teil der vertrauenswürdigen Basis — das Team vermied es, ihm vertrauen zu müssen, indem es auf der Ebene des Maschinencodes argumentierte, was derselbe Kniff ist, der es dem Team ermöglicht, einen verifizierten Compiler vollständig zu umgehen. Als Einordnung zum Umfang nennt das Papier seL4 mit rund 20 Personenjahren und CompCert mit etwa 6.

Zwei Bugs, absichtlich wieder eingebaut

Ein Verifikationssystem, das immer nur „korrekt“ sagt, ist nicht testbar. Daher nahm das Team zwei Schwachstellen, die zuvor im Signal-Code gefunden und behoben worden waren – einen Weak-State-Bug und einen Small-Subgroup-Bug –, führte sie in eine isolierte Kopie wieder ein und ließ die Pipeline erneut laufen. In beiden Fällen erzeugte AlphaProof Code einen maschinell geprüften Beweis dafür, dass die fehlerhafte Version das Sicherheitstheorem nicht erfüllt: Die symbolische Aussage reduziert sich zu ¬Sec(Asm_bug).

Das Paper fügt einen Vorbehalt hinzu, den eine Marketingseite weggelassen hätte: das rechnerische Theorem für diese Bugs zu widerlegen, sei „viel schwieriger“, und dies sei offengelassen worden. Mit anderen Worten: Der Negativtest funktioniert auf der symbolischen Spur sauber und auf der rechnerischen noch nicht. Genau diese Art von Asymmetrie sollte ein Leser kennen, bevor er das Framework als Bug-Detektor behandelt.

Wie die Agenten ausgeführt wurden

Fünf Forschende über vier Wochen, die jeweils ununterbrochen Agenten laufen ließen. Das eigentliche Schreiben der Beweise übernahmen Teams aus 40 bis 80 Agenten, die je Team zwischen 24 und 72 Stunden auf einer einzigen Maschine liefen, mit einem überwachenden Agenten über dem Team-Orchestrator. Ein Gatekeeper-Agent prüft jede Einreichung mit Komparator gegen eine zurückgehaltene Kopie der Spezifikation und gegen den Lean-Kernel – als Schutz davor, dass ein Agent eine subtil abgeschwächte Version des Geforderten beweist.

Die menschliche Arbeit wurde auf die Spezifikationen vorverlagert. Jede Spezifikation wurde von einem Experten geprüft, bevor die Beweisarbeit begann, und der eigene Audit-Durchlauf der Agenten markierte etwa 1 % der Codebasis für menschliche Aufmerksamkeit. Kein Mensch schrieb Beweiscode. Das Paper ist auch offen, was die Engineering-Seite angeht: Ein sauberer Build kann mehrere Stunden dauern, anfangs führten eine geringfügige Quellcodeänderung oder ein neu kompiliertes Binary zu umfangreichen Reparaturen an den Beweisen, und es gibt „erhebliches Optimierungspotenzial“ sowohl bei den KI-generierten Beweisen als auch bei den Beweistechniken selbst.

Was die Beweise nicht abdecken

Die Einschränkungen sind lang genug, um der wichtigste Abschnitt des Aufsatzes zu sein, und sie werden klar benannt. Für die Healing-Eigenschaft von SPQR wird keine Post-Quanten-Garantie nachgewiesen — die Ratchet-Theoreme gehen davon aus, dass der Angreifer SPQR-Schlüssel wählt. Die Privatsphäre der Nutzdaten ist nicht bewiesen. Die Responder-Authentifizierung ist für die erste Nachricht eines Handshakes, der nie hochgestuft wird, nicht bewiesen. Das Modell erlaubt eine Sitzung pro Hochstufung, feste Nachrichtenlängen, keinen Multi-Device-Zustand und Identitätsschlüssel nach dem Trust-on-First-Use-Prinzip.

Es gibt außerdem eine Schranke, die inhaltsleer wird. Der 8-Byte-MAC-Fälschungsterm beträgt mindestens 2⁻⁶⁴ pro Versuch und wächst quadratisch mit Nachrichten und Epochen, was bedeutet, dass die Schranke für eine einzelne Sitzung von ungefähr 25.000 Nachrichten oder für 2²⁰ Sitzungen mit 2¹⁰ Nachrichten nichts mehr aussagt. Und Gegenstand des Beweises ist der Build des Teams von libsignal-cli, der als frischer Prozess läuft — nicht die Signal-App auf Ihrem Telefon. Mehrere Umgebungsannahmen werden informell begründet statt bewiesen.

Es gibt keine API, keinen Preis und kein Modell, das man aufrufen kann.

Das ist der Teil, der jeden enttäuschen wird, der von einer Modell-Bestenliste kommt. AlphaProof Code ist ein Forschungsframework und eine veröffentlichte Artefaktsammlung. Es gibt keinen Endpunkt, keine Preiskarte pro Token, keine Warteliste und keine Gewichte: Das Repository enthält die Lean-Entwicklung, die AArch64-Semantik, die libsignal-Bindung und die Spezifikationen, keinen Checkpoint. Der Blog sagt, die Artefakte seien quelloffen; die Landingpage nennt keine Lizenz, was man prüfen sollte, bevor jemand plant, darauf aufzubauen.

Die Modelle, die die Arbeit geleistet haben, sind eine andere Frage. Das Paper nennt G​emini 4 Carbon für die Proof-Agenten und gibt an, dass Claude Opus 5.5 neben anderen Modellen zum Entwerfen und Überprüfen von Spezifikationen verwendet wurde. Claude Opus 5.5 steht heute im Katalog von OrcaRouter für 4 $ pro Million Input-Tokens und 20 $ pro Million Output, wobei der Listenpreis des Anbieters mit 0 % Aufschlag weitergegeben wird — wenn die praktische Erkenntnis, die Sie suchen, also lautet „eine Spec-Drafting-Schleife mit dem Modell laufen lassen, das das Paper verwendet hat“, dann ist dieser Teil ein normaler API-Aufruf, und eine Preisänderung des Anbieters kommt am selben Tag bei uns an. Die Engine der Proof-Agenten ist nichts, was wir anbieten, und nichts hier deutet darauf hin, dass wir AlphaProof Code selbst hosten.

Warum das eine größere Sache ist als das Signal-Ergebnis

Die Verifikation von Signal ist für sich genommen beeindruckend – die erste formale Verifikation der Implementierung eines weit verbreiteten Protokolls mit welcher Methode auch immer, mit oder ohne KI, laut DeepMind, und das erste Mal, dass KI ein eingesetztes kryptografisches Protokoll in dieser Tiefe verifiziert hat. Doch die übertragbare Aussage betrifft den Workflow. Ein Team von fünf Personen hat in vier Wochen mit einem Spezifikationsprüfungsschritt und einem Agenten als Gatekeeper einen Beweiskorpus erstellt, der zuvor ein mehrjähriges Projekt gewesen wäre. Wenn dieses Verhältnis auch nur grob gilt, ändert sich die Menge der Systeme, die sich Verifikation leisten können: Firmware für Medizingeräte, Software für Stromnetze, die Art von Code, die derzeit ein Code-Review und ein Stoßgebet bekommt.

Ob es Bestand hat, ist ungetestet. Signals Krypto ist ungewöhnlich gut spezifiziert, das Team ließ die Methodik von Signals eigenen Ingenieuren prüfen, und die Primitive wurden extern vergeben statt verifiziert. Das nächste System wird nicht so entgegenkommend sein. Die eigene Rahmung des Papers – formale Verifikation mit automatisierten Verteidigungsagenten wie CodeMender zu kombinieren – ist die ehrliche Form des Pitch: Verifikation sagt dir, was wahr ist, und etwas anderes muss beheben, was nicht stimmt.

Was zu sehen

Drei Dinge würden dies von einer wegweisenden Arbeit zu einer industriellen Technik machen. Eine zweite, unabhängige Codebasis, verifiziert von jemandem außerhalb von Google, idealerweise eine, bei der die Spezifikation von Grund auf geschrieben werden musste, statt aus einer bestehenden Analyse übernommen zu werden. Eine Kostenangabe — Agentenstunden, Beschleunigerstunden, Dollar —, denn vier Wochen und Teams aus 40 bis 80 Agenten sind keine Einheit, mit der ein Engineering-Manager budgetieren kann. Und die Bug-Widerlegung im Computational-Track, die das Papier offenlässt und die den Unterschied ausmacht zwischen einem System, das Eigenschaften beweist, und einem System, das Ihnen außerdem rechnerisch sagen kann, dass eine bestimmte Binärdatei defekt ist.

Bis dahin lies das Artefakt-Repository statt der Ankündigung. Die Beweise sind dort, Lean prüft sie, und das Paper sagt dir genau, was sie voraussetzen.