Microsoft Research ha descritto il PDD Kit il 5 novembre 2026 come un prototipo di ricerca che trasforma requisiti di sviluppo in specifiche Verus e controlla il codice Rust scritto da agenti. Nella dimostrazione di Pet Store, gli autori riferiscono prove formali per cinque funzioni di login, ciascuna rispetto al proprio contratto: la verifica riguarda quelle funzioni, non l’intera applicazione. Database, controllo delle password e altre operazioni esterne restano affidati a contratti accettati e test, anziché essere dimostrati nelle rispettive implementazioni. Microsoft Research
La verifica formale è una dimostrazione controllata da una macchina che il codice soddisfa proprietà espresse in una specifica, per tutti gli input compresi nel modello. Un test, invece, controlla il comportamento su casi eseguiti. La differenza pratica è che una prova può coprire sistematicamente gli input del modello, ma vale per le proprietà scritte nel contratto.
Una prova offre garanzie precise sulle regole formalizzate; la qualità di quelle regole resta parte del lavoro di sviluppo.
Che cosa ha verificato PDD Kit nel login di Pet Store
Pet Store è un’applicazione Rust completa, descritta come composta da circa 5.000 righe di codice. Microsoft Research riferisce che PDD Kit ha verificato cinque funzioni: login_flow, login_core, lookup_target, decide_login e issue_token. Gli autori affermano che ciascuna soddisfa il proprio contratto per ogni input rappresentato dal modello.
Il contratto di login_flow contiene otto clausole ensures, che specificano condizioni e risultati attesi. Tra queste ci sono la corrispondenza tra account e token, le regole per password e ruoli e alcune risposte di errore. Otto è il numero di clausole di questa funzione, non dell’intero progetto di verifica.
Dall’intento al contratto: la scelta sulla password
Il flusso descritto da Microsoft Research parte dai requisiti, li sottopone a revisione e registra le decisioni necessarie a renderli verificabili. PDD Kit li traduce poi in contratti per Verus; le proprietà formalizzate vengono dimostrate e le parti fidate ricevono test. La scheda di decisione sul login mette a fuoco una distinzione concreta: stabilire che una password sbagliata non possa ottenere un token non equivale a richiedere anche che una password corretta consenta il login. Senza questa seconda regola, anche un sistema che rifiutasse tutti potrebbe rispettare il primo requisito.
Nel caso illustrato, la specifica richiede entrambe le condizioni: niente token con password errata e un token con quella corretta, salvo errori nella ricerca dell’account o nella firma del token. La distinzione mostra perché una frase apparentemente chiara può lasciare aperto un comportamento importante.
Dove finisce la prova e iniziano le ipotesi fidate
Nel login di Pet Store, le query al database, bcrypt, la firma dei token, l’accesso all’orologio, la gestione degli errori del database e l’estrazione dei dati dalla richiesta appartengono al perimetro fidato. Microsoft Research descrive sei categorie di approvazione per queste ipotesi; quella delle query al database ne comprende due. I contratti di queste operazioni sono accettati e i componenti vengono sottoposti a test, ma la dimostrazione non verifica le loro implementazioni esterne.
La specifica prevede che il token scada 24 ore dopo la lettura dell’orologio. Il comportamento dell’orologio, però, resta un’ipotesi fidata. Anche il completamento del login asincrono e il tempo necessario a terminarlo non sono garantiti dal contratto: questo definisce gli esiti se l’operazione restituisce un risultato.
Una prova non certifica la specifica
La prova stabilisce che il codice rispetta il contratto approvato; da sola non dimostra che quel contratto raccolga ogni esigenza dello sviluppatore. Il processo di revisione di PDD Kit serve a chiarire ambiguità e rendere esplicite le decisioni, ma il controllo formale opera sulle regole che sono state definite.
Nel quadro più ampio della formalizzazione dell’intento, Shuvendu K. Lahiri colloca test e contratti eseguibili tra gli strumenti più leggeri, i contratti logici in una fascia più formale e la sintesi verificata basata su linguaggi specifici nel livello più strutturato. Il suo lavoro individua nella validazione delle specifiche un problema centrale: manca un criterio indipendente capace di garantire che una formulazione rifletta tutto ciò che l’utente intende. Lahiri, “Intent Formalization”
Perché Verus lega il prototipo a Rust
Microsoft Research afferma che il PDD Kit descritto verifica codice Rust. Verus è uno strumento di verifica formale basato su SMT, una tecnica che usa solutori per controllare obblighi logici; la descrizione ufficiale spiega che usa la sintassi Rust e sfrutta tipi lineari e borrow checking, il controllo dei prestiti e della proprietà dei dati, nelle prove. Queste caratteristiche riguardano Verus, lo strumento sottostante, mentre il risultato di Pet Store resta quello riferito da Microsoft Research per le cinque funzioni di login. Microsoft Research su Verus
