Vous validez la spec, la machine valide le code

GitHub Next et Microsoft Research ont annoncé le Proof-Driven Development Kit le 21 octobre. C'est un aperçu de recherche, il ne fonctionne que sur Rust, et il avance un argument que la plupart des équipes qui font tourner des agents de code évitent : si vous ne pouvez plus lire le diff ligne par ligne, arrêtez de faire semblant, et révisez autre chose.

Cet autre chose, c'est une spécification. Dans le workflow du PDD Kit, un humain approuve la spec, et une machine vérifie que l'implémentation la respecte pour toutes les entrées possibles.

Cinq étapes, et où se place l'humain

La boucle tourne comme ça. Une équipe planifie la fonctionnalité dans Chopin, l'outil de planification agentique multi-joueurs de GitHub Next. Le PDD Kit discute ensuite le code, infère l'intention et propose une spécification formelle écrite en Verus, un langage de preuve open source qui existe déjà pour Rust. Un humain approuve la spec — pas le code. Verus prouve alors que le code généré par l'agent satisfait cette spec pour toutes les entrées. Là où une preuve complète n'est pas possible, le kit retombe sur des tests et des agents computer-use pour une vérification empirique, et la sortie est une pull request vérifiée.

L'inversion, c'est toute l'idée. Vous révisez l'exigence. Le vérificateur révise l'implémentation. En Verus, une spec annote les fonctions avec des préconditions et des postconditions que le vérificateur doit décharger, et la garantie est plus forte qu'une suite de tests au vert d'une manière précise : les tests échantillonnent des entrées, les preuves quantifient sur toutes.

La formulation de GitHub est que Chopin plus le kit permettent de livrer du code généré par IA en production sans le relire ligne par ligne, avec une assurance plus forte que la revue de code et les tests seuls. C'est un éditeur qui décrit son propre aperçu de recherche, pas un résultat audité. À ne pas tenir trop fermement.

{{INLINE1}}

Le coût s'est déplacé, il n'a pas disparu

La tentation est de lire ça comme « le fardeau de la revue est réglé ». Non. Il a migré en amont du pipeline, et il est devenu plus dur d'une façon facile à sous-estimer.

Écrire une spec assez précise pour être prouvable est une compétence différente de la revue d'un diff. Des exigences vagues produisent des specs improuvables, et le vérificateur vous le dira en échouant, ce qui fait ressembler les premières semaines d'adoption à un outil qui ne marche pas. Ce qui se passe vraiment, c'est que l'ambiguïté de vos exigences remonte plus tôt que d'habitude, poussée par quelque chose qui ne la masquera pas avec une fonction d'apparence plausible.

Pour les équipes qui écrivent déjà des docs de conception que personne ne lit, c'est un vrai changement. Le doc de conception devient porteur, parce que c'est l'artefact qui se fait vérifier.

Là où les preuves s'arrêtent

Trois limites comptent plus que la liste de fonctionnalités.

Rust uniquement. Verus vérifie du Rust, et GitHub Next dit que le kit fonctionne sur Rust aujourd'hui, sans nouveau langage et sans changer la façon dont le code est produit. Si vos agents écrivent du TypeScript ou du Python, il n'y a rien à installer pour l'instant. Vu la part de code de production qui n'est pas du Rust, c'est une restriction énorme portée par une petite phrase.

Seulement ce qu'une spec peut exprimer. La preuve formelle couvre les propriétés que vous pouvez énoncer précisément : contrats d'entrée et de sortie, invariants, transitions d'automate. Elle ne couvre pas le comportement d'interface, l'essentiel de la logique chargée en E/S, ni tout ce dont la correction est un jugement plutôt qu'une propriété. Tout ça part sur le chemin de repli, tests et revue humaine, exactement là où vit déjà le fardeau actuel.

Aperçu de recherche, avec un historique précis. Chopin figure sur la page projets de GitHub Next comme prototype de recherche daté de septembre 2026. GitHub Next a déjà livré des prototypes — Repo Mind, Project Copernicus, SpecLang entre autres — qui n'ont jamais atteint la disponibilité générale. La première démo publique sur du vrai code est prévue à GitHub Universe, les 28 et 29 octobre.

C'est dans le repli que se trouve l'honnêteté

La décision de conception qui en dit le plus n'est pas le prouveur. C'est le second chemin explicite pour le code qui ne peut pas être prouvé, qui part vers les tests et les agents computer-use pour une vérification empirique.

C'est un aveu que la plupart des outils de vérification refusent de faire. L'architecture dit qu'il y a du code prouvable et du code qui ne l'est pas, et que prétendre le contraire serait pire que livrer deux pipelines. Une équipe qui utilise ça finit avec une étiquette par module — prouvé, testé, relu — ce qui est un inventaire de confiance plus honnête que tout ce que produit un rapport de couverture.

Le hic, c'est que le chemin de repli est aussi l'endroit où les agents corrigent leur propre copie. Un agent computer-use qui clique dans une interface pour vérifier qu'un changement a marché reste un agent, échantillonne toujours, et peut toujours conclure qu'un parcours cassé a l'air très bien. Le chemin prouvé donne une preuve. Le repli donne une démo qui est passée.

La recherche en dessous, c'est la partie rassurante

Le kit n'est pas un vérificateur construit de zéro. Verus est séparé et établi. Le dépôt verus-proof-synthesis de Microsoft Research contient les fondations : deux systèmes pilotés par LLM, AutoVerus et VeruSAGE, qui génèrent et réparent des preuves Verus, évalués sur 150 et 849 tâches de vérification respectivement.

Ce que le kit semble ajouter, c'est l'emballage. C'est la première fois que cette ligne de recherche sur la synthèse de preuves est repliée dans un workflow produit qui va du plan à la PR, plutôt que dans un exercice de benchmark. C'est une affirmation plus petite que « l'IA peut prouver son propre code », et plus crédible.

Notez aussi que les sources ne s'accordent pas sur le nom. Vous verrez Proof-Driven Development Kit et Property-Driven Development Kit dans la couverture de la même semaine, tous deux attribués à la même annonce. Choisissez-en un et avancez ; l'acronyme fait le branding dans les deux cas.

Ce que vous pouvez faire dès aujourd'hui

Le constat durable n'est pas « attendez la GA ». C'est qu'une base de code à forte densité d'agents se scinde maintenant en territoire prouvable et non prouvable, et que votre configuration devrait déjà savoir lequel est lequel.

Parseurs, automates, invariants de structures de données, arithmétique avec bornes, primitives de concurrence : c'est le territoire prouvable, et Verus est open source et utilisable dès maintenant, avec ou sans le kit. La plupart du travail front-end, la plupart du code de collage, et tout ce dont la correction dépend de ce qu'un utilisateur voulait dire, non.

Deux gestes pratiques en découlent. D'abord, étiquetez les modules prouvables de votre dépôt et pointez vos agents vers Verus pour ceux-là spécifiquement, avant qu'un éditeur ne livre un workflow. Ensuite, arrêtez de demander aux agents d'écrire aussi les tests qui valident leur propre travail ; cet arrangement a toujours été un conflit d'intérêts, et c'est la raison pour laquelle une suite au vert vaut moins qu'avant.

La question qui dérange

Si une spec peut être approuvée par un humain et une preuve déchargée par une machine, à quoi sert exactement le relecteur ? Pas à lire du code, et probablement pas à attraper le bug que l'agent a introduit ligne 412.

Le boulot du relecteur devient celui qu'il aurait toujours dû être : décider ce que le système est censé faire, et refuser une spécification qui ne le dit pas. C'est plus dur que cliquer sur approuver un diff. C'est aussi la seule partie du travail qu'un vérificateur ne peut pas faire à votre place.