Le 5 novembre 2026, Microsoft Research a présenté PDD Kit, un prototype de recherche qui transforme des exigences de développement en contrats formels pour vérifier du code Rust écrit par des agents. Dans l’exemple de Pet Store, les auteurs rapportent des preuves pour cinq fonctions liées à la connexion. Elles portent sur les contrats approuvés, tandis que plusieurs opérations externes restent des dépendances de confiance testées séparément. Microsoft Research détaille la démonstration.
Cinq fonctions de connexion, pas toute la boutique
La démonstration concerne login_flow, login_core, lookup_target, decide_login et issue_token. Microsoft Research rapporte que chacune satisfait son contrat pour toutes les entrées représentées dans le modèle. Le contrat de login_flow comprend huit clauses ensures, qui spécifient notamment les conditions d’émission d’un jeton, les rôles de compte et certaines réponses d’erreur. Ces huit clauses ne décrivent pas toute la vérification : elles appartiennent à cette seule fonction.
Pet Store est une application Rust de bout en bout d’environ 5 000 lignes, avec un backend utilisant Axum et SQLite et une interface Leptos compilée en WebAssembly. Le résultat rapporté porte sur sa logique de connexion, pas sur une preuve formelle de l’ensemble de la boutique.
Comment une exigence devient un contrat vérifiable
La vérification formelle consiste ici à démontrer, au moyen d’un outil, qu’un programme respecte des propriétés écrites dans une spécification. Il faut d’abord décider précisément quelles propriétés le contrat doit imposer. Une règle disant « aucun jeton sans le bon mot de passe » ne garantit pas à elle seule qu’un utilisateur ayant saisi le bon mot de passe en recevra un : un système qui refuserait toutes les connexions respecterait aussi cette règle.
Dans l’exemple, la carte de décision demande si un mot de passe correct doit toujours donner un jeton. L’option retenue impose les deux résultats : le bon mot de passe permet d’obtenir un jeton pour le compte concerné, tandis qu’un mauvais mot de passe est refusé. Le hash stocké illisible entraîne une erreur. Cette précision écarte le cas absurde d’un système qui refuserait tout le monde, mais elle ne prouve pas que la spécification traduit chaque attente du développeur.
Les tests couvrent des dépendances hors de la preuve
Les recherches en base de données, la vérification du mot de passe par bcrypt, la signature du jeton, l’accès à l’horloge, la gestion des erreurs de base de données et le décodage de la requête sont traités comme des opérations de confiance. Leurs contrats sont acceptés et ces composants sont testés ; leurs implémentations externes ne sont pas démontrées par la preuve Verus. Microsoft Research regroupe ces validations en six catégories, dont l’une couvre deux recherches en base de données.
La distinction est utile : une preuve porte sur les propriétés du modèle, alors qu’un test vérifie des cas précis exécutés. Dans cet exemple, l’expiration du jeton est spécifiée à 24 heures après la lecture de l’horloge. Le contrat de cette horloge reste toutefois une hypothèse de confiance. Le contrat asynchrone précise aussi les résultats attendus si l’opération aboutit, sans garantir qu’une connexion se termine ni dans quel délai.
Une preuve solide commence par une exigence assez précise pour exclure les comportements que l’on ne veut pas.
Une preuve ne valide pas l’intention à elle seule
Même si le code respecte son contrat, celui-ci peut être incomplet ou mal formulé. La revue des exigences et les contrôles de spécification de PDD Kit aident à repérer des ambiguïtés, mais ils ne démontrent pas que chaque besoin réel a été traduit dans les clauses. Dans son article publié le 17 mars 2026, Shuvendu K. Lahiri situe cette difficulté dans un problème plus large : la formalisation de l’intention va des tests et contrats exécutables aux contrats logiques, puis à la synthèse vérifiée à partir de langages dédiés. La validation des spécifications reste un enjeu central de ce domaine (article de Lahiri).
Pourquoi la démonstration repose sur Rust
Microsoft Research indique que le prototype décrit vérifie du Rust. Verus est un outil de vérification de programmes Rust fondé sur les solveurs SMT, une famille d’outils qui vérifient des contraintes logiques. Sa description officielle explique que les preuves s’appuient sur la syntaxe de Rust, ses types linéaires et son système d’emprunt (borrow checking) pour raisonner sur la propriété et la séparation des données (présentation de Verus par Microsoft Research). Ces mécanismes décrivent Verus ; le résultat sur les cinq fonctions reste celui rapporté pour la démonstration de PDD Kit.
