Microsoft PDD Kit: Vertrauensgrenzen vor der Beweisfreigabe festlegen

Microsoft Research zeigt mit PDD Kit einen nützlichen Ansatz für agentengenerierten Rust-Code: Sie genehmigen das beabsichtigte Verhalten, lassen die Implementierung gegen eine formale Spezifikation beweisen und testen die Abhängigkeiten, deren Korrektheit der Beweis voraussetzt. Für Unternehmen lautet die Entscheidung nicht, ob ein Etikett „verifiziert“ die technische Prüfung ersetzt. Entscheidend ist, ob eine kritische Funktion eine ausreichend kleine und explizite Vertrauensgrenze für einen begrenzten Pilotversuch besitzt.

Der unmittelbare Nutzen liegt in belastbareren Nachweisen für Anmelde-, Berechtigungs- oder Zahlungslogik. Die Grenze ist ebenso konkret: Ein Beweis über spezifiziertes Verhalten belegt nicht automatisch, dass eine Datenbank das richtige Konto liefert, eine Signaturbibliothek das richtige Geheimnis nutzt oder eine Anfrage innerhalb ihrer Frist endet. Dafür benötigen Sie jeweils eigene Nachweise.

Was Microsoft demonstriert hat

Am 5. November 2026 veröffentlichte Microsoft Research die PDD-Kit-Demonstration an einer Full-Stack-Anwendung. Der Beitrag beschreibt einen Forschungsprototyp, der in die Planungsumgebung Chopin von GitHub Next eingebunden ist. In einer Rust-Anwendung namens Pet Store verifizierte das Team die Anmeldelogik mit Verus und dokumentierte sowie testete die umgebenden Annahmen.

Der beschriebene Ablauf trennt ein Anforderungsdokument, formale Spezifikationen, generierten Code und Beweise sowie empirische Prüfungen. Menschen prüfen Entscheidungen zum gewünschten Verhalten und zu den als vertrauenswürdig vorausgesetzten Komponenten. Verus prüft den Beweis. Eine zusätzliche Lückenprüfung durch ein Sprachmodell ist ein weiterer Prüfschritt, nicht der mathematische Verifizierer. Microsoft berichtet, dabei bestehende Fehler gefunden zu haben. Das sind Ergebnisse der Autoren, keine hier reproduzierte Installation oder Benchmarkmessung.

Damit ändert sich die Prüffrage von „Sind die generierten Tests erfolgreich?“ zu „Welche Eigenschaften sind unter welchen Annahmen für welchen Versionsstand bewiesen?“. Gewöhnliche Tests bleiben notwendig. Sie erfassen beobachtete Ausführungen; ein formaler Beweis kann alle Eingaben innerhalb seines Modells und seiner Annahmen abdecken. Keine der beiden Methoden ergänzt automatisch fehlende fachliche Anforderungen.

Verfügbarkeit, Sprachunterstützung und Beschaffungsgrenzen

PDD Kit wird als Forschungsprototyp beschrieben und verifiziert derzeit Rust über Verus. Das Verus-Projekt unterstützt selbst nur einen Teil von Rust und weist auf möglicherweise fehlende Funktionen und unvollständige Dokumentation hin. Daraus folgt keine allgemeine Verfügbarkeit eines Verifizierers für beliebige Python- oder TypeScript-Anwendungen.

Die Chopin-Projektseite beschreibt einen frühen, quelloffenen Forschungsprototyp, kein fertiges Produkt, und rät zum Abrufzeitpunkt ausdrücklich von einer sofortigen Nutzung ab. Öffentliche Dokumentation und ein öffentliches Repository sind nicht gleichbedeutend mit einem unterstützten Unternehmensdienst. Die geprüften Quellen belegen weder einen kommerziellen PDD-Kit-Preis noch ein Produktions-SLA, eine EU-Hosting-Zusage oder einen fertig paketierten Bereitstellungsweg für Unternehmen. Prüfen Sie diese Punkte vor einer Beschaffung separat.

Übertragen Sie Lizenzbedingungen von Chopin oder Verus nicht pauschal auf sämtliche PDD-Kit-Komponenten oder einen verwendeten Modelldienst. Prüfen Sie die konkreten Artefakte und Abhängigkeiten Ihres Vorhabens. Zum Pilotbudget gehören Spezifikationsarbeit, Erstellung und Reparatur von Beweisen, Agenteninferenz, Verifiziererlaufzeit, Integrationstests und Wartung nach Änderungen an Abhängigkeiten. Die Ankündigung enthält keinen vollständigen Kostenvergleich, aus dem sich eine Einsparprognose ableiten ließe.

Warum die Vertrauensgrenze wichtiger ist als das Etikett

Im Microsoft-Beispiel umfasst der Beweis Funktionen wie login_flow und den Kern der Anmeldeentscheidung. Datenbankabfragen, Passwortprüfung, Uhrzugriff, JWT-Signatur, Fehlerbehandlung und Entpacken der Anfrage bleiben an benannten Grenzen vorausgesetzt und getestet. Auch Verifizierer, Compiler, Solver und relevante Verifikationsbibliothek gehören zu den Annahmen der Nachweiskette.

Ein als vertrauenswürdig vorausgesetzter Wrapper ist keine bewiesene Abhängigkeit. Verspricht sein Vertrag „liefere das Konto zu dieser E-Mail-Adresse“, kann der Beweis mit diesem Vertrag korrekt arbeiten, obwohl die Implementierung den falschen Mandanten abfragt. Ein Test des Wrappers gegen das tatsächliche Datenbankschema erfüllt eine andere Nachweispflicht als der Beweis der nachgelagerten Logik.

Ein illustratives Unternehmensszenario: Ein Agent ergänzt eine bestehende Anmeldung um Mandantenbezug. Der verifizierte Kern bindet das ausgegebene Token an das Konto aus einer Abfrage. Fehlt der Mandantenbezug im Vertrag dieser Abfrage, kann der Beweis genau die falsche Anforderung für einen mandantenfähigen Betrieb absichern. Das ist ein vorgeschlagenes Prüfszenario, kein gemeldeter PDD-Kit-Fehler. Prüfen Sie deshalb Abfragevertrag, Implementierung und Tests der Mandantengrenze gemeinsam.

Das unterscheidet sich von unserem Freigabeverfahren für KI-generierte Patches. Dort geht es darum, ob ein Reproduktionstest den gemeldeten Fehler belegt und ein Patch ihn beseitigt. Hier entscheiden Sie, auf welche Annahmen sich ein formaler Beweis verlassen darf. Beide Verfahren benötigen nachvollziehbare Evidenz, prüfen aber unterschiedliche Gegenstände.

Leere Garantien und geänderte Verträge prüfen

Microsoft zeigt eine hilfreiche Mehrdeutigkeit: „Ein Token wird nur bei richtigem Passwort ausgegeben“ erfüllt auch eine Funktion, die jede Anmeldung ablehnt. Die Anforderung braucht eine ergänzende Erfolgsbedingung unter ausdrücklich benannten Voraussetzungen. In einem echten Unternehmenssystem können dazu ein freigeschaltetes Konto, zusätzliche Authentifizierungsfaktoren und Richtlinienprüfungen gehören. Machen Sie aus dem Passwortbeispiel der Demonstration nicht Ihre gesamte Anmelderichtlinie.

Die beschriebene Mutationsprüfung von PDD Kit fügt für eine gezielt geprüfte Nachbedingung einen Fehler ein und verlangt, dass Verus diesen ablehnt. Damit wird untersucht, ob die Spezifikation das beabsichtigte Fehlverhalten ausschließt. Die Vollständigkeit der fachlichen Spezifikation ist dadurch nicht bewiesen. Überlebt eine Mutation, müssen Sie Vertrag oder Mutation untersuchen, statt den ursprünglichen grünen Beweis als ausreichend zu behandeln.

Die betriebliche Empfehlung lautet: Schützen Sie Spezifikationen als freigaberelevante Eingaben. Eine geänderte Annahme, abgeschwächte Nachbedingung oder vergrößerte Vertrauensgrenze benötigt eine neue Entscheidung des Verantwortlichen. Lassen Sie nicht denselben Agenten stillschweigend den Vertrag ändern, damit seine Implementierung besteht. Die übergreifende Architektur menschlicher Freigaben beschreibt die Zuständigkeit. Bei beweisgestützter Entwicklung gehören der geänderte Vertrag und seine Vertrauensannahmen in den Mittelpunkt der Prüfung.

Entscheidungstabelle für einen Pilotversuch

Verwenden Sie die folgenden Punkte als technische Prüfliste, nicht als Behauptung, Microsoft habe genau dieses Beschaffungsverfahren durchgeführt. Beginnen Sie mit einer sicherheits- oder geschäftskritischen Funktion, deren Verhalten sich spezifizieren lässt, ohne den Großteil der Anwendung hinter angenommenen Verträgen zu verbergen.

Benennen Sie für jede vorausgesetzte Abhängigkeit einen Verantwortlichen, die bereitgestellte Annahme und den Test, der eine verletzte Annahme sichtbar machen soll. Ein Datenbanktest muss das relevante Schema und Isolationsverhalten verwenden, nicht nur ein Mock mit dem erwarteten Rückgabewert. Ein Tokentest muss Claims und Verifikationspfad prüfen, nicht lediglich eine nichtleere Zeichenfolge.

Verknüpfen Sie Beweisergebnisse, empirische Ergebnisse, Codeversion, Spezifikationsversion und Werkzeugversionen in einem Prüfdatensatz. Verlangen Sie, dass der tatsächlich bereitgestellte Anfragepfad die verifizierte Implementierung aufruft. Ein Beweis für eine ungenutzte Hilfsfunktion verändert den Produktionspfad nicht. Microsoft beschreibt ausdrücklich, den echten Login-Handler über den verifizierten Ablauf zu führen. Übernehmen Sie diese Integrationsanforderung in Ihr eigenes Konzept.

Ein Beweis ist keine Latenz- oder Verfügbarkeitsgarantie

Microsoft stellt klar, dass die Login-Spezifikation weder den Abschluss einer Anfrage noch eine begrenzte Antwortzeit, den Ausschluss sämtlicher uhrbezogener Panics oder das Verhalten anderer tokenverarbeitender Endpunkte verspricht. Diese Auslassungen sind betrieblich relevant. Eine Anmeldung, die unbegrenzt auf die Datenbank wartet, kann weiterhin einen Vertrag partieller Korrektheit über das Ergebnis im Rückkehrfall erfüllen.

Behalten Sie Last-, Timeout-, Abbruch- und Abhängigkeitstests im Freigabeplan, wenn diese Eigenschaften Anforderungen sind. Prüfen Sie die Autorisierung auch am tokenverarbeitenden Endpunkt, nicht nur bei der Ausgabe. Ein lokal korrekter Token-Claim belegt nicht, wie ein anderer Dienst ihn interpretiert. Der Beitrag zur Prüfung von Agenten-Verifizierern ergänzt diesen Punkt: Ein Freigabemechanismus muss falsche Ergebnisse ablehnen; seine eigene Abdeckung bleibt trotzdem begrenzt.

Hinzu kommt ein Wartungszielkonflikt. Ein schmaler verifizierter Kern kann die Absicherung verbessern und den Beweisaufwand begrenzen, belastet aber die vorausgesetzten Adapter stärker. Eine breitere Verifikation kann einzelne Annahmen reduzieren und zugleich Modellierungs- und Werkzeugaufwand erhöhen. Wählen Sie die Grenze nach Fehlerkosten und der Fähigkeit, Nachweise dauerhaft zu pflegen, nicht nach dem Anteil des Codes mit dem Etikett „verifiziert“.

Nächster Schritt: ein begrenzter Nachweispilot

Für ein deutsches Unternehmen ist eine Funktion mit genehmigter Spezifikation und expliziter Liste unbewiesener Abhängigkeiten der sinnvolle nächste Schritt, nicht eine Neuentwicklung des gesamten Systems. Legen Sie vorab fest, welche Fehler die Einführung stoppen, wer geänderte Annahmen genehmigt und wie die Beweispflege in normale Releases passt. Ob Nachweise regulatorisch oder vertraglich ausreichen, müssen die zuständigen Rechts- und Prüfexperten beurteilen. Dies ist technische Orientierung, keine Compliance-Feststellung.

Wenn Sie agentengenerierten Code in prüfbare Freigabenachweise überführen möchten, unterstützt die KI-Automatisierungsberatung bei Pilotabgrenzung und Abnahmekriterien. Bringen Sie die tatsächliche fachliche Invariante und die Abhängigkeit mit, die diese am ehesten verletzen könnte. Das ist ein belastbarerer Ausgangspunkt als die Behauptung einer vollständig verifizierten Anwendung.