PDD Kit : Microsoft Research veut prouver le code écrit par les agents, pas seulement le relire

Les agents de code produisent plus de lignes qu'une équipe ne peut en relire. Dans un billet daté du 5 novembre 2026, Microsoft Research propose une autre voie que la relecture : faire démontrer mathématiquement que le code respecte ce qui a été demandé. L'outil s'appelle PDD Kit, pour « Proof-Driven Development », et il est présenté comme un prototype de recherche.

Le principe

Une relecture répond à la question « est-ce que cela a l'air correct ? ». Une preuve formelle répond à « est-ce correct, pour toutes les entrées possibles ? ». Le pari des auteurs est que les agents peuvent désormais rédiger la spécification formelle et la preuve, pendant qu'un vérificateur classique, sans IA, accepte ou rejette le résultat.

PDD Kit est développé par le Catalyst Lab de Microsoft Research avec GitHub Next et le groupe RiSE. Il fonctionne dans Chopin, l'environnement de planification de GitHub Next, et s'appuie sur Verus, un vérificateur pour le langage Rust. Conséquence directe : seul Rust est pris en charge aujourd'hui.

Comment cela se déroule

• Clarifier l'intention. L'outil pose des questions au développeur avant d'écrire quoi que ce soit, et consigne les réponses.
• Séparer ce qui se prouve de ce qui se teste. Ce qui peut être formalisé devient une spécification formelle ; le reste est couvert par des tests, que l'outil présente comme des indices et non comme des preuves.
• Nommer ce qui est admis. La base de données, la bibliothèque de mots de passe ou l'horloge ne sont pas prouvées. Chaque élément admis est listé et le développeur le valide un par un.
• Écrire et vérifier. Un agent écrit le code et la preuve, Verus vérifie.
• Tester la spécification elle-même. L'outil introduit volontairement une erreur par clause : si le vérificateur ne la détecte pas, la clause ne contraint rien et elle est signalée.

L'exemple publié

La démonstration porte sur « Pet Store », une application web en Rust d'environ 5 000 lignes. Seule la connexion a été vérifiée. La demande du développeur tenait en deux phrases : seul le bon mot de passe donne un jeton, seuls les comptes administrateurs reçoivent un jeton administrateur. Elle est devenue huit clauses formelles et cinq fonctions prouvées. Une question de l'outil a levé une ambiguïté utile : le bon mot de passe doit-il toujours donner un jeton ? Sans cette précision, un système refusant tout le monde aurait respecté la consigne.

Selon les auteurs, le développeur a relu l'intention, la spécification et les éléments admis, sans lire le code généré ligne à ligne.

Les limites

Elles sont en grande partie reconnues dans le billet :

• pas de mesure à grande échelle : un seul cas d'étude, sur un seul module ;
• les modèles et agents utilisés ne sont pas nommés ;
• le billet ne précise ni licence ni dépôt public pour PDD Kit ;
• une preuve ne vaut que ce que vaut la spécification, et une spécification fausse donne un code faux mais « vérifié » ;
• les éléments admis portent une grande part du résultat : la vérification du mot de passe repose sur une bibliothèque seulement testée ;
• les temps de réponse, la limitation des tentatives ou la qualité d'un message d'erreur échappent à la preuve.

Notre lecture

Pour une PME, rien à installer pour l'instant : c'est un prototype, limité à Rust, sans date de mise à disposition. L'idée à retenir est ailleurs. Quand un agent écrit le code, le travail humain se déplace vers trois questions : qu'ai-je demandé exactement, qu'est-ce qui est prouvé, qu'est-ce qui est seulement supposé. Vous pouvez déjà exiger cette distinction de vos prestataires et de vos outils, en commençant par les parties sensibles : connexion, droits d'accès, paiement.