Les LLM rendent la vérification formelle pratique à grande échelle
Sommaire
En bref
- Anthropic et Theorem ont utilisé Claude pour écrire des preuves formelles sur 123 bibliothèques open source en code RISC-V, sans intervention humaine manuelle. Ces preuves garantissent l'absence de certaines classes de bugs (plantages, débordements mémoire) sous des conditions précises. Claude a découvert des bugs restés inaperçus malgré des trillions d'exécutions de test.
Ce que dit la source
La vérification formelle a toujours été un outil réservé aux systèmes critiques (avionique d'Airbus, noyau seL4) car elle exige des années d'effort spécialisé : les preuves sont souvent bien plus longues que le code lui-même. Anthropic affirme que les LLM frontière rendent cela automatisable à large échelle. Plutôt que de demander au développeur de spécifier le comportement attendu, leur approche convertit les suites de test existantes en spécification formelle : « le test passe toujours » devient le théorème à prouver. Une fois traduit en Rocq (assistant de preuve), le code assembly RISC-V est exploré exhaustivement pour tous les chemins d'exécution.
- Claude a prouvé autonomement des propriétés de sécurité sur plus de 123 bibliothèques open source en code assembly RISC-V, une première selon Anthropic à cette échelle sur du logiciel de production.
- Les preuves garantissent qu'un programme exécuté en tant que binaire statique monothread sur une CPU RISC-V ne plantera jamais sur aucune entrée inférieure à 64 MB, pour chaque réponse du kernel Linux et configuration mémoire modélisées.
- Le vérificateur de preuve Rocq valide les preuves : seules trois surfaces de confiance restent (modèles formels de RISC-V et Linux, énoncés du théorème, le vérificateur lui-même), aucune revue manuelle massive.
- Au cours de ce processus, Claude a découvert des bugs qui avaient échappé à la détection pendant des années malgré des milliards d'exécutions de test.
- Anthropic et Theorem publient des preuves réutilisables ainsi qu'une compétence Claude pour aider les développeurs à explorer la vérification sur leurs propres projets.
Dans les commentaires
Débat partagé : d'un côté, des cas réels de succès (réécriture Postgres en Lean-Rust, déploiement en production avec preuves d'équivalence comportementale) et l'intérêt de techniquement valider les transformations (SIMD, CUDA). De l'autre, des sceptiques sur la généralité de l'approche : dépendance aux test suites pour spécifier le comportement, limitations annoncées par Anthropic elle-même concernant la scalabilité du style de preuve verbeux sur du code très complexe, et doute sur le rapport coût-bénéfice comparé à du fuzzing exhaustif ou des tests orientés propriété.
- Plusieurs commentateurs soulignent un problème fondamental : la spécification. Convertir les tests en spec signifie prouver que le code passe ses tests, mais un test suite ne capture jamais l'intention métier. La méprise entre vérification (le code fait ce qu'on demande) et validation (on demande le bon truc) reste non résolue, les LLM formels n'y échappent pas.
- L'approche repose sur ASan (AddressSanitizer) et un modèle Linux incomplet : plutôt que de prouver directement l'absence d'accès hors limites sur le binaire original, l'agent prouve que le binaire instrumenté ne plante pas, puis l'équivalence comportementale. C'est un « tour de passe-passe » fonctionnel mais moins direct que présenté.
- Anthropic reconnaît elle-même dans l'appendice que les agents risquent de heurter un mur de complexité : les preuves verboses ne passent pas à l'échelle sur du code réellement complexe sans introduire de meilleures abstractions modulaires, ce que les agents n'ont pas encore démontré capable de découvrir seuls.
- Un commentateur économe pose la question : pourquoi générer 180 millions de lignes de preuve alors qu'on pourrait exécuter les tests exhaustivement sur toutes les entrées inférieure à 64 MB pour moins cher et plus de clarté ?
- Le cas d'usage pratique semble limité : les preuves s'appliquent à des binaires statiques monothread sur une architecture précise, sous des hypothèses fortes. L'intérêt pour le code applicatif multithreads, frameworks asynchrones ou logique métier complexe reste non démontré.
Notre lecture
C'est du travail sérieux sur un problème réel, avec des résultats mesurables et des limites honnêtement énoncées. Utile pour valider des transformations optimisées (SIMD, GPU) dans des codebases critiques où la perte de comportement est le premier risque. Moins convaincant comme réponse générale à la sécurité du logiciel : LLM et vérification formelle règlent un sous-ensemble du problème (absence de plantages mémoire sous modèle Linux simplifié), pas les bugs métier, les races conditions multithreads, ou les spécifications mal alignées. À explorer pour les équipes de sécurité applicative sur du code sensible, mais ne pas confondre avec une panacée de vérification de code.