Utiliser Microsoft PDD Kit pour vérifier le Rust d'agent

Un agent de codage peut dériver du plan que vous lui avez donné puis écrire des tests qui louent la dérive. Microsoft Research a nommé ce trou dans son billet du 5 novembre 2026 sur PDD Kit. Le plan est censé être le contrat. Rien ne force l’agent à le garder, et lire chaque ligne que l’agent a écrite ne passe pas à l’échelle quand une tâche peut toucher des milliers de lignes.

PDD Kit est la correction que Microsoft Research a construite avec GitHub Next. Il transforme l’intention en une spécification formelle, c’est à dire un ensemble d’énoncés précis qu’une machine peut vérifier. Un outil appelé Verus prouve ensuite que le code Rust respecte cette spécification pour chaque entrée dans le modèle. Là où une preuve ne peut pas atteindre, la trousse retombe sur des tests et le dit bien en vue.

Ce que vous allez construire ou apprendre

Vous terminerez avec une méthode claire pour vérifier une pièce de Rust écrit par un agent, et avec Verus installé et prouvé sur un fichier échantillon tiré de son propre guide. La méthode suit l’exemple travaillé que Microsoft a publié. Cet exemple est Pet Store, une application Web complète d’environ 5 000 lignes de Rust, avec un système dorsal Axum et SQLite et une vitrine Leptos compilée en WebAssembly.

L’équipe dans cet exemple a vérifié la connexion. Ce tutoriel utilise la même cible parce que la connexion montre chaque partie difficile à la fois. Elle a une règle que vous pouvez énoncer en une phrase, une règle de rôle qui compte pour la sécurité, des recherches dans la base de données que le vérificateur ne peut pas voir et une vérification de mot de passe qui vit dans une caisse externe. Si vous pouvez cartographier la connexion, vous pouvez cartographier une vérification de paiement, une vérification de permission ou un analyseur avec des règles strictes.

Vous apprendrez aussi la limite qui compte le plus. Une preuve couvre sa spécification et rien d’autre. Le travail qui se trouve hors de la spécification a encore besoin de tests, d’un examen ou d’une note honnête que personne ne l’a promis.

Avant de commencer

Lisez d’abord la limite d’accès, parce qu’elle façonne tout le tutoriel. PDD Kit lui même vit dans Chopin et reste en aperçu de recherche. Il n’existe aucune commande cargo qui installe PDD Kit, et tout guide qui vous en donne une l’a inventée. Les étapes 4 à 8 décrivent le flux tel que Microsoft et GitHub Next le documentent, pour les équipes avec cet accès. Les étapes 1 à 3 et le travail Verus à l’étape 2 sont utiles seuls, et ils sont la préparation dont une équipe a besoin avant que l’accès PDD Kit arrive.

Sauvegardez le code Rust que vous comptez vérifier, et choisissez une branche pour le travail. Le flux ajoute une caisse vérifiée et de nouveaux contrats. Il ne devrait pas atterrir sur votre branche principale jusqu’à ce que la preuve et les tests pour les parties de confiance passent tous les deux. Utilisez des valeurs d’espace réservé dans chaque exemple qui touche un secret, un jeton ou une clé de signature. Aucune étape dans ce tutoriel n’a besoin d’un vrai identifiant.

Notre couverture des sessions d’agents en bac à sable avec Google Agent Substrate montre l’autre moitié de ce problème, garder un agent contenu pendant qu’il travaille. Ce tutoriel couvre la moitié preuve : montrer que le travail que l’agent a livré correspond à ce que vous avez demandé.

Étape 1 : choisir une petite fonction où un bogue coûte de l’argent réel ou de la confiance réelle

Action : choisissez la première cible comme Microsoft le conseille. Commencez avec la partie la plus sensible de l’application et vérifiez le reste une pièce à la fois. La connexion, les paiements et les permissions sont les exemples que Microsoft nomme. Une bonne première cible a des entrées claires, des sorties claires et des règles que vous pouvez énoncer sans goût ni jugement.

Résultat attendu : vous pouvez écrire la cible comme une fonction et une courte liste de résultats. Dans Pet Store, cette fonction est devenue login_flow. Elle prend les champs d’une demande de connexion et retourne un jeton ou une erreur HTTP. Cinq fonctions plus petites se trouvent sous elle : login_core, lookup_target, decide_login et issue_token parmi elles. Chacune a son propre contrat, alors un changement à une pièce a seulement besoin que cette pièce soit prouvée de nouveau.

Une mauvaise première cible est un écran entier, un classement de recherche ou tout comportement où correct est une question d’opinion. Garez ceux là pour les tests et l’examen humain. La preuve a besoin d’une règle, et une règle a besoin de mots qui signifient la même chose pour tout le monde qui les lit.

Étape 2 : installer Verus et prouver l’échantillon de son propre guide

Action : installez Verus depuis sa version binaire. C’est le vérificateur que PDD Kit utilise aujourd’hui, et il fonctionne seul sans aucun accès Chopin. Le fichier d’installation Verus donne cet ordre : téléchargez la plus récente version pour votre plateforme, décompressez la, déplacez vous dans le dossier qu’elle crée et exécutez le binaire. Sous macOS, exécutez le script dans ce dossier qui efface la quarantaine Gatekeeper d’abord.

bash macos_allow_gatekeeper.sh
./verus

Résultat attendu : Verus fonctionne ou vous dit quoi installer. Si rustup manque, il affiche la commande exacte pour l’installer et la chaîne d’outils dont il a besoin. Si rustup existe mais que la chaîne d’outils non, il affiche la commande d’installation rustup pour cette chaîne. Suivez la commande affichée, puis exécutez le binaire de nouveau. Ne devinez pas une version de chaîne d’outils. Le binaire nomme celle pour laquelle il a été construit.

Ensuite, créez le fichier échantillon du guide Verus. Nommez le getting_started.rs et collez ce contenu, que le guide utilise comme son premier exemple :

use vstd::prelude::*;

verus! {

spec fn min(x: int, y: int) -> int {
    if x <= y {
        x
    } else {
        y
    }
}

fn main() {
    assert(min(10, 20) == 10);
    assert(min(-10, -20) == -20);
    assert(forall|i: int, j: int| min(i, j) <= i && min(i, j) <= j);
    assert(forall|i: int, j: int| min(i, j) == i || min(i, j) == j);
    assert(forall|i: int, j: int| min(i, j) == min(j, i));
}

} // verus!

Le guide explique la forme en une ligne qui vaut la peine d’être apprise maintenant. Le fichier est du Rust. La macro verus! l’étend avec un langage de spécification, comme forall, et dit à Verus de vérifier les fonctions dans le bloc. Une spec fn est du code fantôme. Le vérificateur la vérifie, et le compilateur l’efface du programme que vous livrez.

./verus getting_started.rs

Résultat attendu : Verus affiche une note qu’il vérifie le module racine, puis une ligne de résultats qui lit 1 verified, 0 errors, sous la forme que le guide montre. Cette ligne est votre première preuve. Verus a vérifié les affirmations au sujet de min pour toutes les entrées, pas seulement les deux paires dans les asserts simples. Si vous voulez aussi un binaire, le guide donne la même commande avec le drapeau de compilation ajouté. La vérification seule ne compile pas le fichier.

Étape 3 : écrire l’intention en langage simple, dans les deux sens là où cela compte

Action : écrivez la demande pour votre cible en phrases simples, aussi brutes que vous voulez. Pet Store a commencé avec deux phrases pour la connexion. Vous obtenez un jeton seulement avec le bon mot de passe. Seuls les comptes administrateurs obtiennent des jetons administrateurs. PDD Kit traite l’entrée brute comme normale. Transformer l’intention brute en règles vérifiables est son travail.

Lisez ensuite chaque phrase pour le piège que Microsoft a trouvé dans la première. Une règle qui dit qu’un jeton vient seulement avec le bon mot de passe est aussi gardée par une connexion qui refuse tout le monde. La moitié manquante est que le bon mot de passe obtient toujours un jeton. Microsoft appelle la première lecture une implication et la paire de lectures un si et seulement si. Ensemble, elles excluent à la fois la mauvaise connexion et la connexion paresseuse.

Résultat attendu : chaque règle clé énonce ce qui doit se produire et ce qui ne doit jamais se produire. Pour la connexion, la forme établie couvre les deux moitiés. Un jeton est émis si et seulement si la demande nomme un vrai compte et que le mot de passe correspond au hachage rangé pour ce même compte. Ce libellé même compte compte. Il attrape un bogue de câblage où le code vérifie un compte et signe un jeton pour un autre, un bogue qu’une suite de tests pense rarement à chercher.

Étape 4 : exécuter pdd-plan dans Chopin et répondre aux cartes de décision

Action : avec un accès Chopin, ouvrez le plan pour votre dépôt et donnez à PDD Kit la cible et l’intention de l’étape 3. Son flux de planification s’appelle pdd-plan. Il lit le code d’abord. Puis il revient avec des questions sur des cartes de décision avant d’écrire quoi que ce soit. Quand une question dépend de la façon dont le code fonctionne, la carte explique cette partie d’abord, pour que vous puissiez répondre sans ouvrir la source.

Répondez à chaque carte comme une décision d’équipe, pas comme un clic rapide. Dans l’exemple de connexion, la première carte a demandé si le bon mot de passe doit toujours obtenir un jeton. L’équipe a choisi la lecture dans les deux sens de l’étape 3. Une carte ultérieure a demandé quelle part de la connexion prouver. La première ébauche a prouvé la décision au centre et a gardé le gestionnaire comme confiance et testé. Le développeur a choisi davantage : une spécification pour le gestionnaire lui même, pour que la preuve couvre la colle où les recherches sont attendues et où le jeton est signé.

Résultat attendu : PDD Kit garde une section de travail brute en haut du plan, avec un diagramme de flux de la cible, une carte de ce qui sera prouvé et de ce qui sera de confiance, et une carte d’intention. Chaque entrée d’intention renvoie à vos propres mots et vers l’avant à la section de la spécification formelle qui la modélise et aux tests qui la couvrent. Si cette carte ne correspond pas à ce que vous vouliez dire, arrêtez ici. Le reste du flux prouvera fidèlement la mauvaise chose.

Étape 5 : approuver la spécification et la frontière de confiance, pas le code

Action : examinez l’artéfact d’intention comme un tout et approuvez le avant que toute construction commence. La spécification formelle est l’intention en langage simple écrite comme des contrats Verus. Chaque fonction reçoit un bloc ensures. Ce bloc énonce ce qui doit tenir au sujet de son résultat pour chaque entrée possible. Dans la connexion, deux phrases brutes sont devenues huit clauses ensures sur login_flow, couvrant un jeton seulement pour le compte nommé, le bon mot de passe qui obtient toujours un jeton à moins qu’une étape de recherche ou de signature échoue avec un 500, un compte manquant qui obtient un 401, un mauvais mot de passe qui obtient un 401, un hachage illisible qui obtient un 500 et aucun jeton, et le rôle administrateur seulement pour une rangée admins trouvée par nom d’utilisateur sans courriel envoyé.

Examinez ensuite la frontière avec le même soin. La base informatique de confiance est le code dont la preuve suppose qu’il se comporte comme décrit. PDD Kit rend cette ligne explicite et vous demande d’accepter chaque pièce seule. Pour la connexion, le développeur a accepté six pièces :

Dans le code, une pièce de confiance se trouve derrière un petit emballage avec un contrat supposé. Verus lit le contrat et non le corps. La spécification marque cela avec des termes comme external_body pour un emballage, ou une spécification externe pour une fonction dont le code reste où il est. Les noms pour les choses que la preuve ne peut pas modéliser, comme ce que la base de données garde en ce moment, apparaissent comme des fonctions abstraites sans corps. La preuve dit alors que quoi que la base de données garde, la connexion fait la bonne chose avec, et le contrat de confiance dit que la recherche retourne ce que la base de données garde.

Lisez aussi la liste de ce que personne ne promet. Pour la connexion, cette liste nomme un futur qui ne se termine jamais, une horloge hors de plage qui panique, le minutage et le taux des tentatives, et la façon dont d’autres points de terminaison lisent le rôle. Une preuve dit ce que son résultat sera si la fonction répond. Elle ne dit rien sur la vitesse, ni si elle répond du tout.

Résultat attendu : vous avez approuvé une spécification que vous pouvez lire, une frontière que vous avez acceptée pièce par pièce et une liste de trous que personne ne prétend couvrir. Deux agents examinateurs dans le flux sondent aussi la spécification pour des trous et pour des promesses qu’une preuve ne pourrait pas montrer, et cet examen fonctionne jusqu’à ce que la spécification se lise comme solide. Votre approbation reste l’acte qui compte. Correspondre à votre intention n’est pas une preuve, alors une portée plus large ou un nouveau choix de confiance revient pour une approbation neuve.

Étape 6 : laisser l’agent mettre en œuvre, puis exécuter pdd-prove

Action : remettez le plan approuvé à l’étape de preuve. En termes Microsoft, un plan de construction transforme le plan en un petit graphe de tâches. Pour la connexion, ce graphe avait sept tâches : faire construire le fichier sous Verus dans la caisse dorsale, prouver la décision, l’étape du jeton et tout le flux, puis écrire les tests pour les emballages de confiance et pour la connexion comme un tout.

Chaque tâche exécute la même boucle. Un agent de codage écrit le code et la preuve. Verus les vérifie par rapport à la spécification. Tout ce qui est dans la frontière de confiance reçoit les tests que le plan demandait. Un agent examinateur lit ensuite le plan, la spécification et les résultats côte à côte et cherche des trous, c’est à dire des exigences sans preuve et sans vérification qui passe. Les trous retournent à l’agent de codage. Un trou dans la spécification elle même vous revient comme une décision.

Surveillez le mode d’échec que Microsoft appelle la vérification d’ambiance. Une clause faible peut se vérifier tout en n’excluant presque rien. Le garde est une vérification de mutation. L’étape de preuve plante un bogue par clause ensures dans une copie de travail du code, comme refuser tout le monde ou vérifier le nom d’utilisateur avant le courriel, et Verus doit rejeter chaque copie modifiée sur la clause qu’elle cible. Un mutant qui passe signifie que cette clause ne contraint rien, et elle revient comme un trou.

Résultat attendu : chaque clause est prouvée ou listée comme un trou avec une raison. La boucle est stricte sur le déplacement des poteaux de but. Si une construction ne peut pas être énoncée dans la version Verus en usage, la tâche s’arrête et demande à l’équipe. Elle n’échange pas une forme plus simple et n’adoucit pas un contrat pour obtenir un résultat vert.

Étape 7 : tester la frontière de confiance comme si c’était le produit

Action : exécutez les tests que le plan a écrits pour chaque pièce de confiance contre les vraies parties, pas contre leurs maquettes. Microsoft décrit les entrées du plan comme planifiées jusqu’à ce qu’elles s’exécutent, après quoi elles enregistrent le résultat de la commande et la consignation contre laquelle elles ont fonctionné. Dans la connexion, cela signifie des tests contre le vrai bcrypt, le vrai schéma SQLite et le vrai routeur.

Utilisez le même soin que vous utiliseriez pour le travail sur les secrets. Notre tutoriel pour empêcher Claude Code de fuir des secrets vers GitHub fait le même point de l’autre côté : un résultat d’outil est une preuve au sujet des entrées qu’il a essayées, et rien de plus. PDD Kit étiquette un test qui passe de la même façon. Une preuve, pas une démonstration.

Résultat attendu : chaque clause supposée à l’étape 5 a au moins un test nommé qui la vérifie, et le plan montre ce test comme exécuté et passé sur une consignation nommée. Si une pièce de confiance n’a aucun test, traitez chaque promesse qui repose sur elle comme une affirmation, pas comme un résultat. Dans la connexion, deux pièces portent la plus grande part du poids : check_password pour chaque promesse de mot de passe, et les deux recherches pour chaque promesse au sujet du compte qu’un jeton nomme.

Étape 8 : livrer avec pdd-ship et garder la preuve en CI

Action : laissez l’étape de preuve ouvrir ses demandes de tirage, examinez la demande de tirage comme un reçu et fusionnez. Dans l’exemple de connexion, le changement a ajouté une caisse vérifiée avec le flux, ses pièces, leurs preuves et les emballages de confiance avec leurs tests. Il a aussi acheminé le vrai gestionnaire de connexion par ce flux et gardé les codes de statut HTTP que l’application utilisait déjà. La logique vérifiée durcit le chemin de production. Ce n’est pas une copie gardée à un côté.

Exécutez ensuite l’étape de livraison. Le flux pdd-ship ajoute la vérification Verus à CI à côté des tests pour les parties de confiance. Chaque changement ultérieur, par une personne ou par un agent, doit continuer de prouver par rapport à la même spécification. Une preuve brisée fait échouer la construction de la même façon qu’un test qui échoue. Microsoft note aussi un effet secondaire net : les tests qui répètent seulement ce que la preuve couvre maintenant peuvent être coupés, alors que les tests qui gardent la frontière de confiance restent. CI devient plus fort et plus léger en même temps.

Résultat attendu : la description de la demande de tirage marque chaque exigence comme formellement vérifiée ou vérifiée par des tests. Votre examen s’est déjà produit sur l’artéfact d’intention. On ne vous demande pas de lire le code généré ligne par ligne, et vous devriez pouvoir dire, pour toute promesse dans la liste, lequel des deux genres de preuves l’appuie.

Faire fonctionner plusieurs agents à la fois pendant que ce travail atterrit est une compétence séparée. Notre guide pour faire fonctionner Claude Code, Codex et OpenCode avec Corgi couvre le côté espace de travail de ce problème.

Vérification

Parcourez cette liste avant de déclarer la cible vérifiée.

Premièrement, relancez Verus sur la caisse vérifiée et lisez la ligne de résultats. Elle devrait signaler les fonctions comme vérifiées avec zéro erreur. Deuxièmement, vérifiez le registre de mutation de l’étape de preuve. Chaque clause ensures devrait montrer un mutant que Verus a rejeté. Une clause sans registre de mutant n’a pas été testée pour sa force. Troisièmement, ouvrez le plan et confirmez que chaque pièce de confiance de l’étape 5 montre un test qui a fonctionné et passé, avec une consignation nommée à côté. Quatrièmement, brisez la preuve exprès dans une copie de travail, en changeant une ligne de logique, et confirmez que Verus échoue sur la clause qui la couvre. Cinquièmement, confirmez que CI exécute la vérification Verus sur la branche, pour qu’un changement futur qui brise la preuve échoue avant la fusion.

Si les cinq tiennent, vous pouvez énoncer le résultat sous la forme exacte que Microsoft utilise pour la connexion. Prouvé : les fonctions nommées respectent leurs contrats pour chaque entrée. De confiance et testé : les emballages nommés se trouvent hors de la preuve, chacun derrière un contrat qu’une personne a accepté et un test qui le vérifie. Supposé : la chaîne d’outils Verus, Rust et solveur elle même, et la bibliothèque standard Verus.

Dépannage

Prochaines étapes

Choisissez la prochaine fonction sensible et répétez la boucle : une vérification de paiement, une barrière de permission ou un analyseur avec des règles d’entrée strictes. Gardez chaque cible petite. L’habitude de preuve grandit une fonction à la fois, et la frontière de confiance devrait rétrécir à mesure que plus de code se déplace dedans.

Gardez l’artéfact d’intention avec le code. C’est le registre de ce que votre équipe voulait dire, quelle promesse repose sur une preuve et quelle promesse repose sur un test et un nom. Quand le prochain agent arrivera pour changer cette fonction, ce registre est ce qui l’empêche de réécrire discrètement le contrat pendant qu’il réécrit le code.

Faits vérifiés le 9 novembre 2026, par rapport au compte Microsoft Research de PDD Kit, à la page du projet GitHub Next pour PDD Kit, au guide Verus et au fichier d’installation Verus. Ce tutoriel suit le flux que ces sources documentent pour l’exemple de connexion Pet Store et le fichier échantillon dans le guide Verus. Il ne prétend pas que le flux PDD Kit complet a été exécuté dans Chopin pour cet article, parce que PDD Kit est un prototype de recherche et que l’accès est limité.

Sources

• The PDD Kit workflow, the Pet Store app, the two sentence login request, the decision cards, the eight clauses, the six trusted pieces, the mutation check, and the ship stage: Formally verifying agent written full stack web apps with PDD Kit, Microsoft Research
• PDD Kit as a partner inside Chopin, the intent artifact, and the Verus spec route: PDD Kit, GitHub Next
• The getting_started.rs sample, the verus! macro, ghost code, and the expected results line: Verus Tutorial and Reference
• Binary release order, platform builds, the macOS quarantine script, and the toolchain prompts: Verus INSTALL.md
• Workflow diagram and proof boundary diagram: Microsoft Research, from the PDD Kit post above. Hero and other page art: Dirty Static.