L'ESSENTIEL EN 30 SECONDES

  • PDD Kit convertit des exigences arrêtées avec le développeur en spécifications Verus ; un agent doit ensuite écrire un code Rust et des preuves acceptés par Verus.
  • Sur une démo Pet Store d'environ 5 000 lignes de Rust, cinq fonctions de connexion ont été prouvées, tandis que six composants, dont la vérification bcrypt, restent de confiance.
  • L'outil est un prototype de recherche limité à Rust ; ses auteurs reconnaissent que les parties de confiance concentrent une bonne part du risque restant.

Microsoft Research et GitHub Next ont publié une nouvelle étude de cas consacrée à PDD Kit, un prototype de recherche fondé sur ce qu'ils appellent le développement guidé par la preuve. Plutôt que de se fier à des tests qui n'échantillonnent que quelques entrées, la méthode demande aux agents de code de livrer du Rust accompagné de preuves mathématiques, vérifiées par l'outil Verus, montrant que le code respecte une spécification formelle pour toute entrée autorisée. Présenté en avant-première de recherche en octobre, le kit est désormais appliqué à une application web complète.

De l'intention validée à la preuve

PDD Kit fonctionne dans Chopin, l'outil de planification de GitHub Next. Il lit le code et pose au développeur des questions de relecteur sur des « cartes de décision », dont les réponses forment un document d'intention. Ce qui peut en être formalisé devient des préconditions et postconditions Verus. Un agent écrit ensuite l'implémentation et sa preuve, que Verus contrôle. Tout ce qui ne peut être prouvé doit être nommé, accepté par une personne et couvert par des tests, présentés comme des indices et non comme des preuves. Deux agents relecteurs comparent la spécification à l'intention, et une étape de mutation introduit un bogue par clause pour vérifier que chacune contraint réellement le code. Les pull requests listent ce qui a été prouvé et ce qui reste de confiance.

L'expérience Pet Store

L'application de démonstration est une animalerie en ligne d'environ 5 000 lignes de Rust, avec un backend Axum et SQLite et une vitrine en Leptos. L'équipe s'est concentrée sur la connexion, où un bogue pourrait exposer des comptes clients ou des fonctions d'administration, à partir d'une demande de deux phrases portant sur la vérification des mots de passe et les jetons administrateur. Le flux de connexion asynchrone obtenu comporte huit postconditions ; cinq fonctions sont prouvées, tandis que six éléments restent de confiance, dont la vérification bcrypt, deux requêtes en base et la génération de jetons.

Des limites reconnues

Selon la page du projet, PDD Kit ne prend en charge que Rust pour l'instant et l'écriture des preuves demande encore un effort réel. Les garanties ne valent que ce que valent les composants de confiance, et l'équipe admet que rien ne prouve encore la vérification du mot de passe ni les requêtes. Les preuves ne couvrent ni l'aboutissement de la connexion, ni sa vitesse, ni la limitation de débit, ni les exigences jamais formulées. Une spécification peut en outre être valide tout en trahissant l'intention du développeur, d'où le maintien d'un examen humain. Les auteurs espèrent réduire peu à peu la zone de confiance, sans avoir encore montré jusqu'où la méthode passe à l'échelle.