PDD Kit to prototyp badawczy Microsoft Research, który zamienia wymagania dotyczące programu w formalne specyfikacje, a następnie sprawdza, czy napisany przez agenta kod im odpowiada. W opisie opublikowanym 5 listopada 2026 r. Microsoft Research przedstawił demonstrację obejmującą pięć funkcji logowania w aplikacji Pet Store. Dowody dotyczą ich zatwierdzonych kontraktów, nie całej aplikacji; część operacji zewnętrznych potraktowano jako zaufane i objęto testami.
Formalna weryfikacja to maszynowo sprawdzany dowód, że kod spełnia określone właściwości w ramach formalnego modelu. Jest przydatna, gdy trzeba sprawdzić zachowanie programu dla wszystkich wejść uwzględnionych w tym modelu, zamiast polegać wyłącznie na wybranych przypadkach testowych.
Dowód potwierdza zgodność kodu z kontraktem. To, czy kontrakt opisuje właściwe wymagania, nadal trzeba ocenić.
Co PDD Kit sprawdził w Pet Store
Pet Store to aplikacja napisana w Rust, licząca około 5000 linii kodu. Jej zaplecze wykorzystuje Axum i SQLite, a interfejs zbudowano w Leptos i skompilowano do WebAssembly. W opisie projektu Microsoft Research koncentruje się na logowaniu i wymienia pięć formalnie zweryfikowanych funkcji: login_flow, login_core, lookup_target, decide_login oraz issue_token.
Według Microsoft Research każda z tych funkcji spełnia swój kontrakt dla wszystkich wejść objętych modelem. Kontrakt login_flow zawiera osiem klauzul ensures, określających między innymi warunki wydawania tokenu, przypisanie go do konta, role i odpowiedzi błędów. Ta liczba dotyczy właśnie login_flow, nie całego pliku ani aplikacji.
W praktyce oznacza to sprawdzenie określonych obietnic związanych z logowaniem. Nie jest to formalny dowód poprawności całego Pet Store ani wszystkich jego funkcji.
Jak wymaganie staje się kontraktem
Zespół zaczyna od wymagań zapisanych zwykłym językiem, a następnie doprecyzowuje decyzje, które mogą mieć kilka interpretacji. Zatwierdzone wymagania zostają zapisane jako kontrakty Verus. Narzędzie sprawdza, czy kod spełnia te warunki, a osobne testy obejmują zaakceptowane elementy zaufane.
Przykład z logowaniem pokazuje, dlaczego szczegóły mają znaczenie. Wymóg „token tylko przy prawidłowym haśle” zabrania wydania tokenu po błędnym haśle, ale sam w sobie dopuszcza też logowanie, które odmawia wszystkim. Dodanie warunku, że prawidłowe hasło ma prowadzić do tokenu, wyklucza taką interpretację. W przykładzie nieczytelny zapisany skrót hasła może jednak skutkować błędem.
Karta pokazuje różnicę między dwoma kontraktami: jeden określa tylko, że błędne hasło nie może dać tokenu; drugi wymaga także, by prawidłowe hasło prowadziło do tokenu. To drugie wymaganie ogranicza zachowanie programu mocniej, ale sam dowód nie rozstrzyga, czy właśnie taką obietnicę chciał zapisać twórca.
Co pozostaje zaufane i objęte testami
Microsoft Research opisuje sześć kategorii elementów zatwierdzanych jako zaufane. Jedna z nich obejmuje dwa zapytania do bazy danych. Do pozostałych należą sprawdzanie hasła przez bcrypt, podpisywanie tokenów, odczyt zegara, obsługa błędów bazy danych oraz rozpakowywanie żądania przez handler.
Kontrakty tych elementów przyjęto jako założenia, a same operacje objęto testami. Ich zewnętrzne implementacje nie są częścią formalnego dowodu. W rezultacie dowód dla funkcji logowania zależy zarówno od sprawdzonych kontraktów, jak i od tych zaufanych założeń.
Opisany kontrakt nie gwarantuje też, że asynchroniczne logowanie zakończy się ani jak długo potrwa. Określa wynik, jeśli operacja zwróci rezultat, a nie jej termin zakończenia.
Dlaczego dowód nie wystarcza bez dobrej specyfikacji
Formalny dowód odpowiada na pytanie, czy kod spełnia zapisane warunki. Nie potwierdza, że te warunki obejmują wszystkie intencje programisty. Jeśli wymaganie jest niepełne, kod może poprawnie spełniać kontrakt, który nie opisuje pożądanego zachowania.
W szerszym ujęciu Shuvendu K. Lahiri opisuje spektrum metod formalizacji intencji: od testów i wykonywalnych kontraktów, przez kontrakty logiczne, po syntezę programów z wykorzystaniem języków dziedzinowych. W artykule wskazuje też walidację specyfikacji jako kluczowe wyzwanie, ponieważ nie istnieje niezależny sposób, który w pełni rozstrzygałby, czy formalny zapis oddaje intencje użytkownika. Artykuł Lahiriego o formalizacji intencji
PDD Kit lokuje się w tej części spektrum, w której kod sprawdza się względem logicznych kontraktów. Przegląd wymagań pozostaje ważny także wtedy, gdy dowód przechodzi.
Dlaczego demonstracja dotyczy Rust
Microsoft Research opisuje PDD Kit jako prototyp weryfikujący kod w Rust. Używa do tego Verus, narzędzia opartego na metodach SMT, czyli rozwiązywaniu problemów przez automatyczne solvery. Według opisu projektu Verus w Microsoft Research specyfikacje i dowody zapisuje się z użyciem składni Rust, a typy liniowe oraz mechanizm sprawdzania pożyczania pomagają wyrażać w dowodach własność i rozdzielenie zasobów.
To wyjaśnia związek demonstracji z Rust, ale nie rozszerza jej wyników: Microsoft Research opisał dowody dla pięciu funkcji logowania oraz przyjęte założenia dotyczące zewnętrznych operacji.
