Du prüfst die Spec, die Maschine prüft den Code

GitHub Next und Microsoft Research haben am 21. Oktober das Proof-Driven Development Kit angekündigt. Es ist eine Research Preview, läuft nur auf Rust, und es vertritt ein Argument, das die meisten Teams mit Coding-Agents bisher umgangen sind: Wenn du den Diff nicht mehr Zeile für Zeile lesen kannst, hör auf, so zu tun, und prüf stattdessen etwas anderes.

Dieses andere ist eine Spezifikation. Im Workflow des PDD Kit gibt ein Mensch die Spec frei, und eine Maschine prüft, ob die Implementierung sie für jede mögliche Eingabe erfüllt.

Fünf Schritte, und wo der Mensch sitzt

Die Schleife läuft so. Ein Team plant das Feature in Chopin, GitHub Nexts kollaborativem agentischen Planungstool. Das PDD Kit diskutiert dann den Code, leitet die Absicht ab und schlägt eine formale Spezifikation in Verus vor, einer bestehenden Open-Source-Beweissprache für Rust. Ein Mensch gibt die Spec frei — nicht den Code. Verus beweist dann, dass der generierte Code diese Spec für jede Eingabe erfüllt. Wo ein vollständiger Beweis nicht möglich ist, fällt das Kit auf Tests und Computer-Use-Agents für empirische Prüfung zurück, und das Ergebnis ist ein verifizierter Pull Request.

Die Umkehrung ist die ganze Idee. Du prüfst die Anforderung. Der Verifier prüft die Implementierung. In Verus annotiert eine Spec Funktionen mit Vor- und Nachbedingungen, die der Verifier dischargeen muss, und die Garantie ist auf eine bestimmte Weise stärker als eine grüne Testsuite: Tests samplen Eingaben, Beweise quantifizieren über alle.

GitHubs eigene Formulierung: Chopin plus das Kit erlauben es Teams, KI-generierten Code ohne Zeile-für-Zeile-Review in Produktion zu bringen, mit stärkerer Zusicherung als Codereview und Tests allein. Das ist ein Anbieter, der seine eigene Research Preview beschreibt, kein auditiertes Ergebnis. Nicht zu fest halten.

{{INLINE1}}

Die Kosten sind gewandert, nicht verschwunden

Es liegt nahe, das als „das Review-Problem ist gelöst“ zu lesen. Ist es nicht. Es ist an den Anfang der Pipeline gewandert, und es ist auf eine Weise schwieriger geworden, die man leicht unterschätzt.

Eine Spec zu schreiben, die präzise genug für einen Beweis ist, ist eine andere Fähigkeit als das Review eines Diffs. Vage Anforderungen erzeugen unbeweisbare Specs, und der Verifier sagt dir das, indem er scheitert. Deshalb sehen die ersten Wochen der Einführung aus wie ein Tool, das nicht funktioniert. Was tatsächlich passiert: Die Mehrdeutigkeit in deinen Anforderungen wird früher als sonst sichtbar, von etwas, das sie nicht mit einer plausibel aussehenden Funktion zudeckt.

Für Teams, die ohnehin Design-Dokumente schreiben, die niemand liest, ist das eine echte Veränderung. Das Design-Dokument wird tragend, weil es das Artefakt ist, das geprüft wird.

Wo die Beweise aufhören

Drei Grenzen sind wichtiger als die Feature-Liste.

Nur Rust. Verus prüft Rust, und GitHub Next sagt, das Kit funktioniert heute auf Rust, ohne neue Sprache und ohne Änderung daran, wie der Code entsteht. Wenn deine Agents TypeScript oder Python schreiben, gibt es noch nichts zu installieren. Wenn man bedenkt, wie viel Produktionscode kein Rust ist, ist das eine große Einschränkung in einem kleinen Satz.

Nur was eine Spec ausdrücken kann. Formale Beweise decken Eigenschaften ab, die du präzise formulieren kannst: Ein- und Ausgabeverträge, Invarianten, Zustandsübergänge. Sie decken kein UI-Verhalten ab, nicht den Großteil I/O-lastiger Logik, und nichts, wo „korrekt“ ein Urteil statt einer Eigenschaft ist. All das geht in den Fallback-Pfad aus Tests und menschlichem Review, also genau dorthin, wo die heutige Last schon liegt.

Research Preview, mit einer konkreten Vorgeschichte. Chopin steht auf der Projektseite von GitHub Next als Research-Prototyp mit Datum September 2026. GitHub Next hat schon früher Prototypen ausgeliefert — Repo Mind, Project Copernicus, SpecLang darunter — die nie allgemein verfügbar wurden. Die erste öffentliche Demo an echtem Code ist für GitHub Universe angesetzt, 28. bis 29. Oktober.

Die Ehrlichkeit steckt im Fallback

Die Designentscheidung, die am meisten aussagt, ist nicht der Prover. Es ist der explizite zweite Pfad für Code, der sich nicht beweisen lässt, und der zu Tests und Computer-Use-Agents für empirische Prüfung führt.

Das ist ein Eingeständnis, das die meisten Verifikationstools verweigern. Die Architektur sagt: Manches ist beweisbar, manches nicht, und so zu tun als ob wäre schlimmer, als zwei Pipelines auszuliefern. Ein Team, das das nutzt, landet bei einem Label pro Modul — bewiesen, getestet, reviewed — und das ist ein ehrlicheres Inventar des Vertrauens als alles, was ein Coverage-Report produziert.

Der Haken: Der Fallback-Pfad ist auch der Ort, an dem Agents ihre eigenen Hausaufgaben korrigieren. Ein Computer-Use-Agent, der durch eine UI klickt, um zu prüfen, ob eine Änderung gewirkt hat, ist immer noch ein Agent, sampelt immer noch und kann immer noch zu dem Schluss kommen, ein kaputter Flow sehe gut aus. Der bewiesene Pfad liefert einen Beweis. Der Fallback liefert eine Demo, die durchgelaufen ist.

Die Forschung darunter ist der beruhigende Teil

Das Kit ist kein von Grund auf gebauter Verifier. Verus ist eigenständig und etabliert. Das Repository verus-proof-synthesis von Microsoft Research enthält das Fundament: zwei LLM-getriebene Systeme, AutoVerus und VeruSAGE, die Verus-Beweise erzeugen und reparieren, benchmarkiert an 150 beziehungsweise 849 Verifikationsaufgaben.

Was das Kit offenbar hinzufügt, ist Packaging. Zum ersten Mal wird diese Linie der Proof-Synthesis-Forschung in einen Produkt-Workflow von der Planung bis zum PR gefaltet statt in eine Benchmark-Übung. Das ist eine kleinere Behauptung als „KI kann ihren eigenen Code beweisen“, und eine glaubwürdigere.

Nebenbei: Die Quellen sind sich beim Namen nicht einig. In der Berichterstattung derselben Woche tauchen Proof-Driven Development Kit und Property-Driven Development Kit auf, beide derselben Ankündigung zugeordnet. Nimm eins und mach weiter; das Branding macht sowieso das Akronym.

Was du heute tun kannst

Die haltbare Erkenntnis ist nicht „warte auf GA“. Sie ist: Eine agentenlastige Codebasis teilt sich jetzt in beweisbares und nicht beweisbares Terrain, und deine Konfiguration sollte schon wissen, welches welches ist.

Parser, Zustandsmaschinen, Invarianten von Datenstrukturen, Arithmetik mit Grenzen, Nebenläufigkeits-Primitives — das ist beweisbares Terrain, und Verus ist Open Source und jetzt nutzbar, mit oder ohne das Kit. Der größte Teil der Frontend-Arbeit, der größte Teil des Klebecodes und alles, dessen Korrektheit davon abhängt, was ein Nutzer gemeint hat, nicht.

Zwei praktische Schritte folgen. Erstens: Tagge die beweisbaren Module in deinem Repo und richte deine Agents gezielt auf Verus dafür aus, bevor irgendein Anbieter einen Workflow ausliefert. Zweitens: Hör auf, Agents auch noch die Tests schreiben zu lassen, die ihre eigene Arbeit validieren; diese Konstellation war immer ein Interessenkonflikt, und sie ist der Grund, warum eine grüne Suite weniger bedeutet als früher.

Die unbequeme Frage

Wenn eine Spec von einem Menschen freigegeben und ein Beweis von einer Maschine discharged werden kann, wofür genau ist dann der Reviewer da? Nicht zum Codelesen, und wahrscheinlich nicht, um den Bug zu fangen, den der Agent in Zeile 412 eingebaut hat.

Die Aufgabe des Reviewers wird die, die sie immer hätte sein sollen: entscheiden, was das System tun soll, und eine Spezifikation ablehnen, die das nicht sagt. Das ist schwerer, als bei einem Diff auf Genehmigen zu klicken. Es ist auch der einzige Teil der Arbeit, den ein Verifier nicht für dich erledigen kann.