Tu approvi la spec, la macchina controlla il codice

GitHub Next e Microsoft Research hanno annunciato il Proof-Driven Development Kit il 21 ottobre. È in anteprima di ricerca, funziona solo su Rust, e sostiene un argomento che la maggior parte dei team con agenti di coding ha evitato: se non riesci più a leggere il diff riga per riga, smetti di fingere di riuscirci e revisiona qualcos'altro.

Quel qualcos'altro è una specifica. Nel flusso del PDD Kit, una persona approva la spec e una macchina verifica che l'implementazione la rispetti per ogni input possibile.

Cinque passi, e dove si siede la persona

Il ciclo funziona così. Un team pianifica la funzionalità in Chopin, lo strumento di pianificazione agentica multiplayer di GitHub Next. Poi il PDD Kit discute il codice, inferisce l'intento e propone una specifica formale scritta in Verus, un linguaggio di prova open source già esistente per Rust. Una persona approva la spec, non il codice. Verus dimostra poi che il codice generato dall'agente soddisfa quella spec per ogni input. Dove una prova completa non è possibile, il kit ripiega su test e agenti computer-use per una verifica empirica, e l'output è una pull request verificata.

L'inversione è tutta l'idea. Tu revisioni il requisito. Il verificatore revisiona l'implementazione. In Verus, una spec annota le funzioni con precondizioni e postcondizioni che il verificatore deve scaricare, e la garanzia è più forte di una suite di test verde in un modo preciso: i test campionano input, le prove quantificano su tutti.

La formulazione di GitHub è che Chopin più il kit permettono di portare codice generato da IA in produzione senza revisionarlo riga per riga, con un'assicurazione più forte della sola code review più test. Ma è un vendor che descrive la propria anteprima di ricerca, non un risultato verificato da terzi. Prendilo con le molle.

{{INLINE1}}

Il costo si è spostato, non è sparito

La tentazione è leggerlo come «il problema della revisione è risolto». Non lo è. Si è spostato all'inizio della pipeline, ed è diventato più difficile in un modo facile da sottovalutare.

Scrivere una spec abbastanza precisa da essere dimostrabile è un'abilità diversa dal revisionare un diff. Requisiti vaghi producono spec indimostrabili, e il verificatore te lo dirà fallendo, per cui le prime settimane di adozione sembrano quelle di uno strumento che non funziona. Quello che succede davvero è che l'ambiguità nei tuoi requisiti emerge prima del solito, spinta da qualcosa che non la coprirà con una funzione dall'aria plausibile.

Per i team che già scrivono documenti di design che nessuno legge, questo è un cambiamento reale. Il documento di design diventa portante, perché è l'artefatto che viene controllato.

Dove si fermano le prove

Ci sono tre limiti che contano più della lista di funzionalità.

Solo Rust. Verus controlla Rust, e GitHub Next dice che il kit oggi funziona su Rust, senza nuovi linguaggi e senza cambiare come viene prodotto il codice. Se i tuoi agenti scrivono TypeScript o Python, non c'è ancora niente da installare. Considerato quanto codice di produzione non è Rust, è una restrizione enorme dentro una frase piccola.

Solo ciò che una spec può esprimere. La prova formale copre proprietà che puoi enunciare con precisione: contratti di input e output, invarianti, transizioni di macchina a stati. Non copre il comportamento dell'interfaccia, né la maggior parte della logica con molto I/O, né tutto ciò in cui corretto è un giudizio invece di una proprietà. Tutto questo scende sul percorso di fallback di test e revisione umana, che è esattamente dove vive già il carico di oggi.

Anteprima di ricerca, con una storia precisa. Chopin è elencato nella pagina progetti di GitHub Next come prototipo di ricerca datato settembre 2026. GitHub Next ha già rilasciato prototipi — Repo Mind, Project Copernicus, SpecLang tra gli altri — che non sono mai arrivati alla disponibilità generale. La prima demo pubblica su codice reale è in programma a GitHub Universe, il 28 e 29 ottobre.

È nel fallback che sta l'onestà

La decisione di progetto che dice di più non è il dimostratore. È il secondo percorso esplicito per il codice che non si può dimostrare, che porta a test e agenti computer-use per la verifica empirica.

È un'ammissione che quasi tutti gli strumenti di verifica rifiutano di fare. Dice, nell'architettura, che un po' di codice è dimostrabile e un po' no, e che fingere il contrario sarebbe peggio che spedire due pipeline. Un team che usa questo finisce con un'etichetta per modulo — dimostrato, testato, revisionato — che è un inventario di fiducia più onesto di qualsiasi cosa produca un report di copertura.

Il problema è che il percorso di fallback è anche il posto dove gli agenti si correggono i compiti da soli. Un agente computer-use che clicca per un'interfaccia per controllare se una modifica ha funzionato è ancora un agente, sta ancora campionando, ed è ancora in grado di concludere che un flusso rotto sembra a posto. Il percorso dimostrato dà una prova. Il fallback dà una demo che è passata.

La ricerca sotto è la parte rassicurante

Il kit non è un verificatore costruito da zero. Verus è separato e consolidato. Il repository verus-proof-synthesis di Microsoft Research contiene le fondamenta: due sistemi guidati da LLM, AutoVerus e VeruSAGE, che generano e riparano prove Verus, valutati rispettivamente su 150 e 849 attività di verifica.

Quello che il kit sembra aggiungere è il packaging. È la prima volta che questa linea di ricerca sulla sintesi di prove viene piegata in un flusso di prodotto che va dal piano alla PR invece che in un esercizio di benchmark. È un'affermazione più piccola di «l'IA può dimostrare il proprio codice», e più credibile.

Nota anche che le fonti non concordano sul nome. Vedrai Proof-Driven Development Kit e Property-Driven Development Kit nella copertura della stessa settimana, entrambi attribuiti allo stesso annuncio. Scegline uno e vai avanti; il branding lo fa comunque l'acronimo.

Cosa puoi fare oggi

Il punto che resta non è «aspetta la GA». È che una codebase piena di agenti ora si divide in territorio dimostrabile e non dimostrabile, e la tua configurazione dovrebbe già sapere quale è quale.

Parser, macchine a stati, invarianti di strutture dati, aritmetica con limiti, primitive di concorrenza: questo è territorio dimostrabile, e Verus è open source e usabile subito, con o senza il kit. La maggior parte del lavoro front-end, la maggior parte del codice colla, e tutto ciò la cui correttezza dipende da cosa intendeva un utente, no.

Ne seguono due mosse pratiche. Prima: tagga i moduli dimostrabili nel tuo repo e punta gli agenti su Verus solo per quelli, prima che qualsiasi vendor rilasci un flusso. Seconda: smetti di chiedere agli agenti di scrivere anche i test che validano il loro stesso lavoro; quella disposizione è sempre stata un conflitto di interessi, ed è il motivo per cui una suite verde vale meno di prima.

La domanda scomoda

Se una spec può essere approvata da una persona e una prova scaricata da una macchina, a cosa serve esattamente il revisore? Non a leggere codice, e probabilmente non a beccare il bug che l'agente ha introdotto alla riga 412.

Il lavoro del revisore diventa quello che avrebbe dovuto essere fin dall'inizio: decidere cosa il sistema deve fare, e rifiutare una specifica che non lo dice. È più difficile che cliccare approva su un diff. È anche l'unica parte del lavoro che un verificatore non può fare al posto tuo.