PDD Kit soll Agentencode gegen Verus-Spezifikationen beweisen

Werkzeug und Vorgehen

GitHub Next und Microsoft Research haben auf der Universe 2026, der jährlichen Entwicklerkonferenz von GitHub, das Proof-Driven Development Kit vorgestellt. Das Werkzeug, kurz PDD Kit, gehört zu Chopin, dem GitHub-Next-Projekt für Multiplayer-Planung mit Agenten.

Zusammen mit den Entwickelnden übersetzt PDD Kit deren Absicht in eine formale Spezifikation in Verus. Danach beweist es, dass der Code des Coding-Agenten diese Spezifikation für jede Eingabe erfüllt. Wo sich kein Beweis führen lässt, übernehmen Tests. Der Unterschied liegt im Umfang: Ein Beweis gilt für alle denkbaren Eingaben, ein Test nur für die geprüften Fälle.

Die Begründung stammt von den Entwicklern selbst, es handelt sich also um Herstellerpositionen. Der Plan zwischen Mensch und Agent sei nicht bindend; der Agent müsse ihm nicht folgen. Von Agenten geschriebene Tests prüften meist, was gebaut wurde, nicht was verlangt war. Zeilenweises Review skaliere bei wachsender Codemenge kaum noch. PDD Kit soll den Agenten nach eigener Darstellung auf den Plan festlegen. Unabhängige Vergleiche mit und ohne das Werkzeug liegen bislang nicht vor.

Login-Logik von Pet Store: Fehler gefunden, Prüfumfang klein

Als Beispiel dient die Login-Logik von Pet Store, einem Rust-Shopfrontend, das in Chopin formal verifiziert wurde. Laut Hersteller deckte Verus dabei bereits vorhandene Fehler auf. Bezogen auf die Spezifikation habe es außerdem die Abwesenheit von Login-Fehlern bewiesen. Der Entwickler prüfte die Absicht und las den generierten Code nicht Zeile für Zeile. Dass die Verifikation den Code „gehärtet“ habe, ist ebenfalls eine Herstellerangabe.

Die Aussagekraft ist begrenzt. Verifiziert wurde allein die Login-Logik, nicht die gesamte Anwendung. Die Angabe, Pet Store umfasse rund 5.000 Zeilen, stammt nur aus der Zusammenfassung von icreat.ai. Bislang existiert zudem nur diese eine Fallstudie des Herstellers. Die „Abwesenheit von Fehlern“ gilt nur relativ zur Spezifikation. Ist sie lückenhaft oder falsch, beweist Verus trotzdem korrekt, nur eben das Falsche.

Aufwand, Rust-Bindung und offene Reifefragen

Der Hersteller räumt ein, dass die Beweise erheblichen Aufwand erfordern, vor allem bei der Beweiserzeugung. Klare Spezifikationen sollen ihn senken. Deshalb investiert PDD Kit zuerst viel Arbeit darin, die Absicht präzise zu erfassen.

Nach Angaben von Microsoft Research lässt sich Code aus anderen Sprachen nach Rust portieren und gegen dieselben Spezifikationen prüfen. Projekte in anderen Sprachen können verifizierten Rust-Code über Bindings aufrufen. Die Bindung an Rust bleibt damit der Weg, nicht die Ausnahme.

Der Anspruch, formale Methoden auch für Ingenieure ohne Formal-Methods-Hintergrund und für alltägliche Anwendungen nutzbar zu machen, stammt vom Hersteller. Über die Fallstudie hinaus ist er nicht belegt. Offen bleibt, wie PDD Kit Ergebnisse nach Beweis- oder Teststatus kennzeichnet. Der entsprechende Satz der Zusammenfassung ist abgeschnitten, der Anteil bewiesener gegenüber getesteter Teile ist unbekannt. Zu Verfügbarkeit, Lizenz und Preis liegen keine Angaben vor. Teams müssen die Spezifikation selbst prüfen. Der Beweis ist nur so gut wie sie.