Le laboratoire RDI de l'université de Californie à Berkeley a publié un benchmark baptisé Vero. Il exige que les agents IA accomplissent, à l'échelle d'un dépôt entier, deux tâches à la fois : implémenter chaque API requise et démontrer que chaque spécification donnée est valide, tout en gardant le code, la preuve et la compilation constamment cohérents. Les benchmarks de vérification formelle précédents s'arrêtaient pour l'essentiel au niveau d'un seul théorème ou d'une seule fonction ; celui-ci est le premier à l'échelle d'un dépôt entier.
L'énoncé se compose de 43 projets Lean 4 multi-modules, portés à partir de code existant en Python, Dafny, Verus et Coq, couvrant au total 743 API et 2 705 spécifications formelles. L'évaluation s'exécute selon deux modes : en mode preuve seule, une implémentation de référence est fournie et l'agent doit seulement la démontrer ; en mode code et preuve, l'agent doit écrire lui-même l'implémentation puis démontrer qu'elle satisfait la spécification.
Le tableau des scores
Nombre d'instances entièrement résolues (sur un total de 43) avec un budget de 90 minutes :
| Configuration | Code et preuve | Preuve seule |
|---|---|---|
| GPT-5.5 (xhigh) + Codex | 27 | 25 |
| Claude Opus 4.8 + Claude Code | 8 | 10 |
| GPT-5.5 (medium) + Codex | 2 | 6 |
| Claude Sonnet 5 + Claude Code | 2 | 2 |
L'écart entre la première et la troisième ligne mérite qu'on s'y attarde : avec le même GPT-5.5 et le même Codex, le simple passage du niveau de raisonnement de medium à xhigh fait bondir le score en mode code et preuve de 2 à 27. Sur ce type de tâche, le rendement marginal du budget de raisonnement est loin d'être saturé.
La difficulté n'est pas de prouver une spécification isolée
La première ligne du classement livre un autre lot de chiffres. GPT-5.5 (xhigh) réussit 87,3 % des spécifications individuelles en mode code et preuve, et 85,8 % en mode preuve seule, mais selon le critère de « l'instance entièrement résolue », il ne reste plus que 27/43 et 25/43. Le constat des chercheurs est sans ambiguïté : démontrer chaque spécification isolée n'est plus le point difficile ; ce qui l'est, c'est de maintenir la cohérence de tout le dépôt de preuves.
L'écart entre ces deux chiffres a des implications concrètes en ingénierie. Un taux de réussite de 87 % par spécification, rapporté à un projet comportant des dizaines de spécifications, signifie que presque tous les projets resteront bloqués sur quelques-unes d'entre elles. Or la vérification formelle fonctionne en tout ou rien : il suffit qu'une seule spécification reste non démontrée pour que tout le dépôt échoue à la compilation, sans que les parties déjà correctement démontrées n'obtiennent le moindre crédit partiel. C'est totalement différent d'un projet dont 87 % des tests unitaires passent et qui peut malgré tout être mis en production.
Un autre détail concerne la composition du code de preuve. Dans les exécutions entièrement résolues, les lemmes auxiliaires représentent une médiane de 73,6 % du code de preuve. Autrement dit, les trois quarts de ce qu'écrivent les agents ne sont que des échafaudages montés à la hâte pour soutenir la preuve principale. Cette proportion suggère que les modèles actuels privilégient une approche en largeur, empilant les lemmes pour forcer le passage, plutôt que de trouver une structure de preuve concise.
Choisir soi-même son algorithme : utile 5 fois, contre-productif 17 fois
Le mode code et preuve laisse à l'agent un degré de liberté : puisque l'implémentation peut être écrite librement, il peut aussi choisir un algorithme plus facile à prouver. Les chercheurs ont mesuré l'effet net de cette liberté : sur des comparaisons appariées, 5 cas ont réussi grâce au changement d'algorithme, tandis que 17 ont échoué à cause de lui.
Ce rapport de 5 contre 17 en dit long. En théorie, pouvoir choisir sa propre implémentation ne devrait qu'aider — au pire, il suffit de recopier l'implémentation de référence. Dans les faits, le modèle choisit souvent une version qu'il juge « astucieuse » mais qui se révèle plus difficile à prouver, puis s'enlise dedans sans pouvoir en sortir dans les 90 minutes imparties. Savoir écrire du code et savoir quel code est facile à prouver sont deux compétences distinctes, et les agents actuels ne maîtrisent que la première.
Le classement laisse aussi une note en suspens : sur les 43 instances, 10 n'ont jamais été résolues par aucune configuration, dans aucun des deux modes. Cet ensemble constitue le plafond dur actuel de la méthode, et c'est aussi là que la prochaine phase de travail devrait le plus se concentrer.
Pour ceux qui conçoivent des outils de programmation par IA, l'intérêt de Vero ne réside pas dans le classement, mais dans le fait qu'il transforme la « cohérence à l'échelle du dépôt » — jusque-là seulement perçue empiriquement — en une métrique mesurable. Les benchmarks du type SWE-bench évaluent la capacité à corriger correctement un seul bug ; Vero évalue la capacité à tenir face à l'ensemble des contraintes d'un projet d'ingénierie. Ces deux difficultés ne relèvent pas du même ordre de grandeur.
Sources : blog public du laboratoire RDI de Berkeley, CocoLoop ; l'ampleur du benchmark, le nombre d'instances entièrement résolues dans les deux modes, le taux de réussite par spécification, la part des lemmes auxiliaires et les statistiques de comparaison appariée ont tous été vérifiés selon le rapport public.