Formele verificatie is een machinegecontroleerd bewijs dat code aan vastgelegde eigenschappen voldoet. In een artikel van 5 november 2026 beschreef Microsoft Research hoe het onderzoeksprototype PDD Kit vijf functies voor de Pet Store-login formeel controleerde tegen goedgekeurde contracten. De garantie geldt voor die eigenschappen binnen het model; verschillende externe bewerkingen bleven vertrouwd en werden getest. Microsoft Research beschrijft de demonstratie.
Wat PDD Kit bij Pet Store verifieerde
Pet Store is een full-stack Rust-applicatie van ongeveer 5.000 regels. De backend gebruikt Axum en SQLite; de Leptos-webwinkel wordt naar WebAssembly gecompileerd. De demonstratie richtte zich op de loginlogica, niet op een formeel bewijs voor de hele applicatie.
Microsoft Research meldt dat vijf functies aan hun contracten voldeden voor elke invoer die het model omvat: login_flow, login_core, lookup_target, decide_login en issue_token. Het contract van login_flow bevat acht ensures-clausules. Die leggen onder meer vast bij welk account een token hoort, welke wachtwoord- en rolvoorwaarden gelden en welke foutreacties volgen. Die acht clausules horen bij login_flow, niet bij de volledige codebasis.
Een formeel bewijs geldt voor eigenschappen die in zo’n contract zijn vastgelegd. Het bestrijkt alle invoer binnen het model, terwijl een test concrete gevallen uitvoert. Dat maakt de reikwijdte van de gekozen contracten bepalend voor wat het bewijs garandeert.
Van eis naar contract: één woord verschil
Een eis als ‘geef alleen een token bij het juiste wachtwoord’ legt vast wanneer de login géén token mag geven. Op zichzelf sluit die eis niet uit dat de login iedereen weigert. De extra afspraak dat een juist wachtwoord wél tot een token leidt, maakt de gewenste uitkomst aan beide kanten duidelijker.
In het voorbeeld leidt een juist wachtwoord tot een token, behalve als een databaseopvraging of het ondertekenen van het token mislukt. Een onjuist wachtwoord bij een leesbare hash leidt tot een ongeautoriseerde reactie, tenzij de opvraging mislukt. Een onleesbare opgeslagen hash leidt tot een interne fout. De projectauteurs beschrijven ook hoe PDD Kit de eis met de ontwikkelaar bespreekt, ontwerpkeuzes vastlegt en controleert of de specificatie niet te weinig afdwingt.
Een bewijs is pas bruikbaar als de specificatie de gewenste uitkomst precies vastlegt.
Wat de formele controle niet omvat
Voor externe onderdelen accepteerden de ontwikkelaars contracten als vertrouwde aannames en testten ze de onderdelen, in plaats van hun implementaties formeel te bewijzen. Microsoft Research onderscheidt zes categorieën: databaseopvragingen, wachtwoordcontrole met bcrypt, tokengeneratie en -ondertekening, klok en verloopdatum, databasefouten en het uitpakken van verzoeken in de handler. De categorie voor databaseopvragingen omvat twee bewerkingen.
Ook een concreet detail over de tokenvervaldatum rust op een aanname: het contract stelt die op 86.400 seconden na de klokmeting. De klok zelf valt buiten het formele bewijs. En de specificatie garandeert niet dat een asynchrone login ooit wordt afgerond of hoe lang dat duurt.
Waarom bewijs de specificatie niet valideert
Een bewijs kan aantonen dat code een specificatie volgt, maar niet dat die specificatie alle bedoelingen van de ontwikkelaar bevat. Als een eis te vaag of onvolledig is, kan de code er correct aan voldoen en toch een ongewenste uitkomst geven.
In zijn paper over intentformalisering van 17 maart 2026 plaatst Shuvendu K. Lahiri tests en uitvoerbare contracten aan de lichtere kant van een spectrum. Logische contracten, zoals die in de PDD Kit-demonstratie, vormen een andere stap; geverifieerde synthese met domeinspecifieke talen gaat verder. Lahiri noemt het toetsen van specificaties aan menselijke bedoelingen een centraal probleem, omdat daar geen onafhankelijke maatstaf voor bestaat. De paper van Lahiri biedt die bredere context, geen onafhankelijke beoordeling van PDD Kit.
Waarom Verus de demonstratie aan Rust bindt
Microsoft Research beschrijft PDD Kit als een prototype dat Rust controleert. De gebruikte verifier, Verus, is SMT-gebaseerd: een solver controleert verplichtingen die uit de specificaties en code volgen. Verus gebruikt Rust-syntaxis, lineaire typen en borrow checking in bewijzen om ook redeneringen over eigenaarschap en het delen van gegevens uit te drukken. Microsoft Research licht de aanpak van Verus toe.
Die Rust-specifieke aanpak verklaart waarom de demonstratie geen bewijs biedt voor code in andere talen. Microsoft Research bespreekt het omzetten van zulke code naar Rust of het aanroepen van geverifieerde Rust-code via bindings als mogelijke routes, niet als ondersteuning voor verificatie in meerdere talen.
