Microsoft Research ha annunciato il 5 novembre PDD Kit, un insieme di strumenti per verificare applicazioni full-stack prodotte da agenti. Il sistema parte dall’intento del programmatore, genera una specifica formale in Verus e prova che parti del codice rispettino proprietà dichiarate, affiancando la dimostrazione matematica ai test eseguibili.
La verifica formale può escludere classi di errori rispetto a una specifica, ma non dimostra che la specifica descriva davvero ciò che l’utente voleva. Se requisiti, minacce o assunzioni sono incompleti, il software può essere formalmente corretto e comunque insicuro. Sono quindi necessarie revisione umana, test d’integrazione e monitoraggio dopo il rilascio.
Per imprese italiane in finanza, sanità e pubblica amministrazione la proposta è rilevante perché gli agenti aumentano il volume di codice più rapidamente delle revisioni. Prove formali mirate possono proteggere autenticazione, autorizzazioni e integrità dei dati. Occorre però formare sviluppatori capaci di leggere le specifiche, non soltanto accettare un sigillo automatico.
Microsoft dovrà mostrare costi, copertura e compatibilità su progetti reali. Il confronto utile è con code review, analisi statica e test generativi, misurando bug sfuggiti e tempo totale. PDD Kit non sostituisce secure-by-design: diventa un livello aggiuntivo quando le proprietà critiche sono formulate con precisione.