LLM et vérification formelle : ce que « prouvé » veut dire ici

Le 22 octobre 2026, la Frontier Red Team d'Anthropic, avec une entreprise appelée Theorem, a publié un résultat qui mérite une lecture attentive. L'équipe a utilisé Claude pour écrire des preuves formelles sur du vrai code open source, au niveau assembleur, dans 123 bibliothèques, et a trouvé au passage des bugs qui avaient survécu à des années de tests. Voici ce que cela veut dire simplement, où s'arrête le mot « prouvé », et ce qu'une équipe normale peut en tirer aujourd'hui.

La vérification formelle, sans jargon

Un test vérifie les entrées auxquelles vous avez pensé. Une preuve couvre toutes les entrées. En vérification formelle, on traduit le code en modèle mathématique, on écrit des règles qu'il doit toujours respecter, puis on essaie de prouver que le modèle les respecte. Si la preuve échoue, la façon dont elle échoue désigne un bug possible. On le corrige, on recommence, et on finit avec la preuve qu'il ne reste aucun bug qui enfreigne ces règles.

Le problème a toujours été le coût. L'article cite l'exemple classique : le noyau seL4 a demandé deux années-personnes pour être construit et 20 pour être vérifié. La vérification est donc restée cantonnée à des domaines comme le code avionique.

Ce qu'ils ont vraiment fait

Écrire la spécification est d'habitude le plus dur, alors ils en ont réutilisé une qui existait déjà : les fuzz tests de l'initiative OSS-Fuzz de Google. Un fuzz test est un point d'entrée qui plante quand quelque chose ne va pas, et un fuzzer l'inonde d'entrées générées. Il peut tourner des années sans jamais être complet. L'équipe a transformé chaque fuzz test en énoncé : ce point d'entrée ne plante jamais, pour aucune entrée de moins de 64 Mo, sur le binaire RISC-V compilé.

En quelques semaines, Claude a corrigé les bugs rencontrés et prouvé cet énoncé pour 239 points d'entrée dans 123 bibliothèques. Les preuves totalisent environ 180 millions de lignes de Rocq ; une preuve typique fait environ 600 000 lignes, pour des binaires de 18 000 instructions RISC-V en médiane. Personne ne relit ça à la main. C'est le vérificateur de preuves Rocq qui le fait, et l'article liste ce qu'il faut encore croire sur parole : les modèles formels de RISC-V et des processus Linux, les énoncés exacts des théorèmes, et le vérificateur lui-même.

Les bugs, c'est ce qu'il faut regarder

Les fuzzers mutent de petites entrées, en général plafonnées à 1 Mo. Une partie de ce que les preuves ont révélé est bien au-delà : un compteur qui passe sous zéro dans un décompresseur et provoque une écriture hors limites, seulement sur des entrées d'environ 20 Mo avec une disposition rare ; une lecture hors limites dans un décodeur d'images qui demandait une entrée de 64 Mo et plus de 2 Go de mémoire ; et la redécouverte de CVE-2026-56132 dans libexpat. Une preuve a aussi mis au jour un bug logique qui ne plante jamais : une fonction censée restreindre les fichiers qu'une application peut charger n'était pas toujours appliquée. Le point des auteurs : rien que tenter la preuve trouve de vrais bugs, qu'elle aboutisse ou non.

Où s'arrête « prouvé »

L'article est franc là-dessus, et c'est à mon avis sa partie la plus utile. « Vérifié formellement » ne veut pas dire « sans bug ». Cela veut dire que le code respecte les règles écrites, sur la machine qui a été modélisée. Deux écarts sont nommés :

• La machine. Les preuves portent sur des binaires RISC-V statiques, mono-thread, liés à musl. La plupart des gens exécutent ces bibliothèques sur x86 ou ARM, liées dynamiquement à glibc.
• L'énoncé. AddressSanitizer ne détecte pas tous les bugs mémoire, tous les points d'entrée n'ont pas été vérifiés, et un appelant peut toujours mal utiliser la bibliothèque.

Ce que cela change pour une équipe ordinaire

Vous n'allez sans doute pas écrire du Rocq demain. Mais la méthode part de quelque chose que beaucoup d'équipes ont déjà : un test qui énonce une propriété. Un harnais de fuzzing qui plante quand un aller-retour échoue est une spécification déguisée, et l'article note que prouver qu'un tel test ne plante jamais revient à prouver la propriété elle-même. Un petit exemple de la forme, illustratif, avec des noms de fonctions fictifs :

#include <assert.h>
#include <stdint.h>
#include <stdlib.h>
#include <string.h>

/* your library's own functions; the names are placeholders */
size_t encode(const uint8_t *in, size_t n, uint8_t **out);
size_t decode(const uint8_t *in, size_t n, uint8_t **out);

int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size) {
  uint8_t *packed = NULL, *back = NULL;
  size_t packed_n = encode(data, size, &packed);
  size_t back_n = decode(packed, packed_n, &back);
  assert(back_n == size && (size == 0 || memcmp(back, data, size) == 0));
  free(packed);
  free(back);
  return 0;
}

Écrire des tests de ce genre, où un échec signifie qu'une règle énoncée a été violée, sert dès aujourd'hui avec un fuzzer ordinaire, et c'est exactement ce que ce type d'outil pourra plus tard transformer en preuve. Theorem dit proposer de faire tourner la même chaîne pour d'autres projets open source et publier une skill Claude pour aider les développeurs à vérifier leur propre code.

Prochaine étape : choisissez un parseur ou un encodeur de votre code et écrivez la propriété qu'il doit toujours respecter sous forme de test qui échoue bruyamment. Puis lisez la section sur les limites de l'article original avant de faire confiance à une étiquette « vérifié formellement ». Source : Anthropic Frontier Red Team, LLMs are making formal software verification feasible at a much larger scale.