Microsoft Research beschrieb PDD Kit am 5. November 2026 als Forschungsprototyp und berichtete über formale Beweise für fünf Funktionen des Pet-Store-Logins. Die Prüfung bezog sich auf vereinbarte Verträge für Rust-Code; externe Operationen blieben vertrauensbasierte Annahmen, die getestet wurden. Microsoft Research
Ein formaler Beweis zeigt, ob der Code die festgelegten Regeln erfüllt. Ob diese Regeln wirklich alle Anforderungen treffen, muss weiterhin geprüft werden.
Was beim Pet-Store-Login formal geprüft wurde
Pet Store ist eine etwa 5.000 Zeilen große Rust-Anwendung mit einem Backend aus Axum und SQLite sowie einer Leptos-Oberfläche, die zu WebAssembly kompiliert wird. PDD Kit setzte bei der Login-Logik an. Microsoft Research zufolge erfüllten fünf Funktionen ihre jeweiligen Verträge für alle Eingaben, die das formale Modell abbildet: login_flow, login_core, lookup_target, decide_login und issue_token.
Ein Vertrag legt fest, welches Verhalten eine Funktion einhalten muss. Der Vertrag von login_flow enthält acht ensures-Klauseln, etwa zu Kontozuordnung, Passwörtern, Rollen und festgelegten Fehlerantworten. Diese acht Klauseln gehören zu dieser Funktion; sie sind keine Aussage über sämtliche Eigenschaften der Anwendung.
Wie aus einer Absicht ein prüfbarer Vertrag wird
PDD Kit führt Entwicklerabsichten in der GitHub-Next-Umgebung Chopin über überprüfte Entscheidungen zu Verus-Verträgen und Beweisen. Die Spezifikation wird dabei konkret genug formuliert, dass sich ihre Aussagen maschinell prüfen lassen.
Eine Login-Regel macht den Unterschied greifbar: „Mit falschem Passwort darf kein Token ausgegeben werden“ legt fest, wann ein Login scheitern muss. Sie sagt allein noch nicht, dass ein korrektes Passwort zum Erfolg führen muss. Eine Anwendung, die alle Anmeldungen ablehnt, könnte die erste Regel trotzdem erfüllen. Die zusätzliche Zusage, dass ein korrektes Passwort zum Token führt, schließt diesen Fall aus.
Die PDD-Kit-Entscheidungskarte stellt diese beiden Zusagen als unterschiedliche Möglichkeiten gegenüber. Sie veranschaulicht die Anforderungsentscheidung, nicht unabhängig das Ergebnis der formalen Prüfung.
Wo der Beweis endet und Tests übernehmen
Ein formaler Beweis prüft die festgelegten Eigenschaften für alle Eingaben innerhalb des Modells. Ein Test führt den Code dagegen mit bestimmten Fällen aus. Im Pet-Store-Beispiel stützte sich die Prüfung auf angenommene Verträge für externe Schritte, deren Implementierungen nicht durch den Beweis abgedeckt waren.
Microsoft Research beschreibt sechs Kategorien solcher vertrauensbasierten Freigaben. Dazu zählen Datenbankabfragen, bcrypt zur Passwortprüfung, das Signieren von Tokens, der Zugriff auf die Uhr, der Umgang mit Datenbankfehlern und das Auslesen der Anfrage. Die Kategorie für Datenbankabfragen umfasst zwei Abfragen. Diese Komponenten wurden getestet; ihre tatsächlichen Implementierungen wurden nicht formal bewiesen.
Auch das Verhalten der asynchronen Anmeldung hat eine Grenze: Der Vertrag legt mögliche Ergebnisse fest, wenn die Funktion zurückkehrt. Er garantiert nicht, dass sie beendet wird oder wie lange sie dafür braucht. Der Bericht über die Demonstration beschränkt sich auf die Login-Logik, nicht auf einen formalen Beweis der gesamten Pet-Store-Anwendung.
Warum ein Beweis die Spezifikation nicht ersetzt
Der Beweis zeigt, dass der Code die freigegebenen Vorgaben erfüllt. Er kann nicht selbst feststellen, ob darin alle Anforderungen der Entwickler enthalten sind. PDD Kit nutzt Prüfungen und Rückfragen, um Unklarheiten in den Vorgaben sichtbar zu machen; die Entscheidung, welche Anforderung tatsächlich gemeint ist, bleibt dennoch menschlich.
Shuvendu K. Lahiri ordnet die Formalisierung von Absichten in einem Fachbeitrag vom 17. März 2026 in ein breiteres Spektrum ein: von Tests und ausführbaren Verträgen über logische Verträge bis zu Verfahrenssprachen für verifizierte Synthese. Die Validierung der Spezifikation bleibt dabei ein zentrales Problem, weil sich die Absicht nicht durch einen unabhängigen Maßstab vollständig überprüfen lässt. Lahiris Beitrag zur Formalisierung von Absichten
Warum Verus die Demonstration auf Rust beschränkt
Microsoft Research beschreibt das PDD-Kit-Prototyping als auf Rust beschränkt. Verus ist ein SMT-basiertes Werkzeug zur formalen Prüfung von Rust-Programmen. SMT-Löser prüfen logische Bedingungen, die aus den Spezifikationen entstehen. Verus verwendet Rust-Syntax und greift beim Formulieren von Beweisen auf lineare Typen und Borrow Checking zurück, um Besitzverhältnisse und getrennte Speicherbereiche auszudrücken. Diese Eigenschaften beschreiben Verus; sie sind keine zusätzlichen Ergebnisse der Pet-Store-Demonstration. Microsofts Beschreibung von Verus
Für Teams empfiehlt Microsoft Research, zunächst besonders kritische Komponenten formal zu prüfen und den Umfang schrittweise zu erweitern.
