Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa Agrawal
Evyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai Zeldovich
Nicholas Carlini, Rajashree Agrawal, Jason Gross
La plupart des logiciels sont truffés de bogues, que l'IA peut désormais facilement trouver et exploiter. Les défenses standard contre les cyberattaques ne suffisent plus : nous avons besoin de moyens de prouver que le code est exempt de bogues. La vérification formelle de logiciels pourrait fournir cette garantie, mais elle a historiquement exigé des années d'efforts d'experts, la rendant peu pratique pour la plupart des projets réels. En collaboration avec Theorem, cependant, nous montrons que ce n'est plus le cas : les LLM peuvent désormais produire des preuves formelles à grande échelle, permettant de nouveaux flux de développement logiciel incluant des garanties de sécurité prouvées. En utilisant Claude, nous avons prouvé des propriétés de sécurité au niveau du code assembleur (RISC-V) dans plus de 100 bibliothèques logicielles open source réelles. À notre connaissance, il s'agit du premier effort à grande échelle utilisant l'IA pour appliquer la vérification formelle à des logiciels de production au niveau du code assembleur. En écrivant les preuves, Claude a également découvert des bogues qui avaient échappé à toute détection pendant des années, malgré des billions de cycles de test. À mesure que les capacités des modèles continuent de s'améliorer, nous nous attendons à ce que la vérification formelle devienne une partie essentielle du développement de logiciels sécurisés.
Introduction
Même les logiciels matures et fortement testés contiennent des bogues, et les LLM sont de plus en plus habiles à les trouver. Le noyau Linux — l'un des logiciels les plus testés aujourd'hui, déployé sur des milliards d'appareils dans le monde — a récemment vu plus de 1,000 vulnérabilités divulguées. Alors que les modèles de pointe deviennent plus capables de chaîner des bogues apparemment bénins en exploits critiques, nous avons besoin de techniques capables de détecter et de corriger ces bogues avant qu'ils ne puissent être exploités dans la nature.
Idéalement, de telles techniques pourraient trouver et corriger tous les bogues, puis fournir une preuve qu'il n'y en a plus à trouver. La vérification formelle est un moyen d'y parvenir. Dans la vérification formelle, les développeurs traduisent leur code en un modèle mathématique, puis tentent de prouver qu'il respecte toujours un ensemble défini de règles de sécurité. S'ils ne parviennent pas à le prouver, cela signifie qu'il pourrait y avoir un bogue dans le code qui violerait une règle, et la nature de l'échec indique ce que pourrait être ce bogue. En répétant ce processus (après avoir éliminé la cause de chaque échec), on obtient finalement la preuve que le code est exempt de tout bogue qui violerait ces règles.
Cependant, la vérification formelle n'est pas facile. Les preuves peuvent être plusieurs fois plus volumineuses que le code original, et leur rédaction exige un effort considérable ainsi qu'un ensemble de compétences pointues et hautement spécialisées. Par exemple, il a fallu deux personnes-années pour implémenter le noyau du système d'exploitation seL4, mais 20 personnes-années pour le vérifier formellement. Par conséquent, la vérification formelle n'a été pratique que dans des applications véritablement critiques, comme le code avionique d'Airbus.
Mais les LLM rendent cela beaucoup plus facile. Les modèles de pointe peuvent désormais produire, de manière entièrement autonome, des preuves de correction pour des logiciels réels. Pour le démontrer, nous avons demandé à Claude de prouver d'utiles propriétés de sécurité sur 123 bibliothèques open source, notamment en montrant que certains de leurs artefacts exécutables ne peuvent jamais planter sous certaines conditions. Plus précisément, Claude a prouvé que ces programmes se termineront toujours normalement sans déclencher d'erreurs de sécurité mémoire ni d'échecs d'assertions, pour toute entrée de moins de 64 Mo et pour toute réponse modélisée du système d'exploitation (OS) Linux et toute disposition mémoire, sous certaines hypothèses (à savoir que le programme s'exécute en tant que binaire statique monothread avec un budget mémoire fixe sur un processeur RISC-V1 utilisant l'OS Linux). Cela reste bien loin de corriger tous les bugs possibles, mais cela nous rapproche bien plus qu'auparavant et fournit une feuille de route vers cet objectif.
Nous publions un sous-ensemble de ces preuves afin que chacun puisse les vérifier et les réutiliser, ainsi que la sémantique RISC-V et OS. Theorem, notre collaborateur sur ce projet, propose également d’exécuter le même pipeline pour d’autres projets open source, et publie une compétence Claude pour aider les développeurs à se lancer dans la vérification de leur propre code.
La vérification formelle est un vaste domaine aux nombreuses méthodologies. Ci-dessous, nous décrivons également nos premières explorations utilisant d’autres méthodes de vérification formelle pour accélérer d’autres tâches de sécurité ou de développement logiciel, comme l’évaluation de la sécurité de l’algorithme de compression zlib, la preuve de l’équivalence comportementale d’un interpréteur Python écrit en Rust, et l’élimination de bugs de longue date dans des logiciels critiques.
L’avenir de la vérification formelle est prometteur. Le coût de la rédaction de preuves diminue à mesure que les modèles deviennent plus intelligents. De plus, à mesure qu’une part croissante du code est formalisée et que les méthodes permettant d’obtenir des garanties de sécurité se standardisent, la capacité de réutiliser ou de modifier des preuves entre bases de code permettra d’amortir ce coût. Nous encourageons tous les développeurs à explorer la vérification formelle avec les LLM —en particulier ceux qui l’avaient déjà tentée avec des modèles moins performants et avaient constaté que cela ne fonctionnait pas.
Dans la suite de cet article, nous présentons plus en détail nos expériences de vérification formelle.
Transformer les tests en preuves
Pour prouver qu’un logiciel est correct, nous devons d’abord énoncer ce que signifie même « correct ». L’exactitude est définie par la spécification (spec). Dans certains programmes, il existe un moyen clair de spécifier formellement le comportement voulu du programme. Par exemple, un décodeur PNG prend une séquence d’octets et (en suivant la RFC 2083) décode ces octets en l’image correspondante. Mais pour la plupart des programmes, les choses ne sont pas si simples. Que signifierait qu’un éditeur de texte ou un navigateur web soit « correct » ? La difficulté d’obtenir une spécification complète et non ambiguë constitue un obstacle majeur à la vérification des logiciels à plus grande échelle.
Pour résoudre ce problème pour le code des bibliothèques open source que nous cherchions à prouver, nous adoptons l’approche consistant à convertir automatiquement leurs suites de tests existantes et compilables en une spécification, en encodant la règle « cette suite de tests passe toujours », à l’aide d’un modèle général de ce que signifie exécuter n’importe quel binaire compilé pour RISC-V sous Linux. Historiquement, prouver de telles spécifications était intractable, compte tenu de la complexité inhérente à la rédaction d’une preuve capable d’englober et d’étayer un argument sur tous les comportements et interactions possibles de dizaines de milliers d’instructions d’assemblage sur n’importe quelle entrée (et du fait que les preuves tendent, par conséquent, à être extrêmement volumineuses). C’est là que les LLM d’aujourd’hui interviennent : parcourir des millions de lignes de code à la poursuite d’un objectif bien défini est une tâche pour laquelle les LLM sont particulièrement bien adaptés.
Pour ce projet, nous avons commencé par des tests de fuzzing. Dans ces tests, les développeurs écrivent un point d’entrée2 dans leur code qui accepte des entrées, de sorte que toute entrée provoquant un plantage constitue un bug dont les auteurs se soucient. Ensuite, le fuzzer, un moteur de test, génère un nombre énorme d’entrées semi-aléatoires et mutées au point d’entrée afin de trouver un bug (visualisé dans la Figure 1). Plus un fuzzer s’exécute longtemps, plus il peut trouver de bugs. Mais il s’agit fondamentalement d’un processus de force brute, sans garantie d’exercer chaque chemin de code possible, quel que soit le nombre d’entrées essayées.
Pour trouver tous les bugs qui auraient été révélés par un test de fuzzing, nous avons transformé ce test en une spécification définie sur les instructions RISC-V compilées. La spécification indique que le test de fuzzing ne plantera pour aucune entrée de moins de 64 MB.3 Si Claude peut prouver cette spécification, le test de fuzzing sur RISC-V devient superflu : le fuzzing de ce point d'entrée ne trouvera jamais aucun bug.
Nous avons fait cela pour des centaines de projets de l'initiative OSS-Fuzz de Google, qui fournit des tests de fuzzing continus pour les projets open source éligibles. OSS-Fuzz contient des milliers de points d'entrée écrits par des développeurs qui recherchent des propriétés de code défectueuses en provoquant un plantage (par exemple, sur une assertion échouée). OSS-Fuzz instrumente automatiquement les programmes C et C++ avec AddressSanitizer4 (ASan), ce qui les fait planter chaque fois que la mémoire est accédée de manière incorrecte (ce qui est une cause majeure de vulnérabilités logicielles). Les spécifications à large spectre comme la sécurité de la mémoire s'appliquent à presque tous les logiciels.
Sur une période de quelques semaines, Claude a réussi à corriger les bugs qu'il a trouvés, puis à prouver qu'il n'y a aucun crash sur aucune entrée (jusqu'à 64 MB) pour 239 points d'entrée répartis sur 123 bibliothèques OSS-Fuzz différentes. Ces preuves opèrent sur les instructions RISC-V compilées (c'est-à-dire les binaires exécutables), et elles représentent environ 180 millions de lignes de Rocq, une preuve typique atteignant environ 600,000 lignes pour fournir des garanties de sécurité sur des binaires d'une longueur médiane de 18,000 instructions RISC-V. Ces preuves sont construites en traduisant le code assembleur RISC-V vers un modèle mathématique utilisant les sémantiques d'instructions RISC-V et de processus Linux de Theorem. Cela signifie que ces preuves supposent actuellement que le programme s'exécute comme un binaire statique mono-thread avec un budget mémoire fixe sur un CPU RISC-V utilisant l'OS Linux. Étendre la portée de ces preuves est tout à fait à portée de main, car cela impliquerait de standardiser les sémantiques pour davantage d'architectures assembleur et d'autres processus de systèmes d'exploitation. Voir le point de vue d'un expert sur les preuves écrites par Claude.
Bien qu'il s'agisse d'un volume énorme de code de preuve, pratiquement rien ne doit être relu manuellement. Le vérificateur de preuves Rocq garantit que la spécification est correctement satisfaite par la preuve. Par conséquent, les seuls artefacts auxquels un développeur doit faire confiance sont :
- Les modèles formels de RISC-V et des processus Linux ;
- Les énoncés exacts des théorèmes qui ont été prouvés ;
- Le vérificateur de preuves Rocq lui-même.5
Cela ne signifie pas que ces bibliothèques ne contiennent aucun bug. Cela signifie plutôt que tout bug restant se trouve soit dans les artefacts listés ci-dessus, soit hors de la portée de la preuve de Claude. Renforcer ces composants de confiance qui pourraient encore contenir des bugs (Rocq, sémantiques RISC-V et Linux) n'est pas négligeable, mais c'est une tâche bien plus gérable que de déboguer chaque ligne de code couverte par les preuves déployées à grande échelle—surtout que cette approche peut sécuriser un nombre arbitraire de projets sans augmenter la taille des composants de confiance.
Nous accueillons favorablement la vérification indépendante de nos preuves et encourageons le raffinement de notre approche. À cette fin, nous publions les composants de confiance (ci-dessus) créés pour ce projet qui ne sont pas déjà publics ; les preuves Rocq complètes de Claude pour les tests de fuzzing qui n'ont pas nécessité de correction ; et les spécifications d'autres tests de fuzzing que nous n'avons pas pu prouver.
Trouver et corriger des bugs
Ci-dessus, nous avons montré que l'on peut transformer les tests écrits par les développeurs de nombreuses bibliothèques open source (tests de fuzzing) en spécifications que Claude peut prouver comme étant toujours satisfaites, parfois après correction des bugs restants qu'il a trouvés. Pour cette raison, le processus de tentative de preuve de ces spécifications a permis de découvrir des centaines de bugs.
De nombreux bugs sont apparus lors des tentatives de Claude pour prouver des centaines de points d'entrée. Pour éviter que Claude n'ait à s'arrêter pour un humain chaque fois que cela se produisait, nous avons laissé Claude corriger les bugs qu'il trouvait : il corrigeait le code, ce qui entraînait la régénération de la spécification avec ce code corrigé, puis Claude procédait à la preuve de cette nouvelle spécification.6
Beaucoup des bugs que nous avons trouvés sont des bugs qu'un fuzzer aurait peu de chances de trouver un jour. Les fuzzers mutent de petites entrées, généralement plafonnées à 1 MB, et s'appuient généralement sur la couverture de code pour les guider vers les bugs. En prouvant un point d'entrée dans une bibliothèque, Claude a trouvé un sous-dépassement de compteur dans sa copie d'un décompresseur qui conduisait à une écriture hors limites, mais uniquement sur des entrées d'environ 20 MB ayant une disposition particulière et rare. D'autres bugs incluent une lecture hors limites dans un décodeur d'images nécessitant une entrée de 64 MB et plus de 2 GB de mémoire, une lecture hors limites dans une autre bibliothèque nécessitant une séquence particulière d'appels sur deux handles vers le même fichier, et la redécouverte de CVE-2026-56132 dans libexpat, qui nécessitait une entrée profondément imbriquée. Claude a également trouvé des bugs logiques qui ne provoquent jamais de crash. Par exemple, en prouvant qu'une bibliothèque était sûre en mémoire, il a remarqué qu'une fonctionnalité permettant de restreindre les fichiers qu'une application peut charger n'est pas toujours appliquée.
Le but ultime de ce projet était d'obtenir une preuve que les tests de fuzzing compilés en RISC-V n'avaient plus aucun crash à trouver. Cependant, des bugs comme ceux ci-dessus montrent que le processus a un autre avantage, que cet objectif soit atteint ou non : la simple tentative de ce processus révèle déjà de vrais bugs qui doivent être corrigés.
Prouver davantage que la sécurité mémoire
Prouver qu'un test de fuzzing n'a plus aucun crash à découvrir est plus significatif qu'il n'y paraît. Il est courant que les tests de fuzzing dans du code réel vérifient la violation de propriétés de haut niveau significatives, telles que le va-et-vient encodage-décodage, l'idempotence, les lois algébriques, les tests différentiels, l'auto-cohérence ou l'équivalence avec des implémentations de référence. Par exemple, un test de fuzzing pour l'algorithme de compression LZO affirme que si l'on compresse une entrée, puis qu'on la décompresse, le résultat est identique à l'original. Si la propriété n'est pas vérifiée, le programme plante—donc prouver que le test ne plante jamais équivaut à prouver la propriété elle-même.
Cela peut également se produire même lorsque les propriétés ne sont pas directement spécifiées par le développeur. Par exemple, pour que Claude puisse compléter sa preuve OSS-Fuzz pour cpp-httplib, il a fallu écarter la possibilité d'un débordement de pile dû à une récursion trop importante dans le destructeur de std::set. Cette profondeur de récursion est bornée par la profondeur maximale d'un arbre, de sorte que Claude a dû prouver (sur du code machine !) que l'algorithme de rééquilibrage de l'arbre rouge-noir de libc++ est correctement optimisé pour maintenir la profondeur de l'arbre bornée logarithmiquement.
Autres études de cas de vérification formelle
La vérification formelle est un domaine vaste. L'exemple de transformation d'un test de fuzzing en preuve ci-dessus est un cas où les LLM rendent la vérification formelle plus largement utilisable en appliquant directement des preuves au code machine.
Nous avons également connu du succès en utilisant les LLM avec la vérification formelle d'autres manières. Par exemple, nous avons demandé à Claude de rédiger une spécification formelle de la RFC 1950, le document technique qui définit le format de fichier de compression zlib. Ensuite, nous avons demandé à Claude de prouver que l'implémentation zlib dans le noyau Linux implémente correctement cette spécification. Comme dans les exemples ci-dessus, Claude a prouvé cette propriété au niveau binaire, mais au lieu de RISC-V, Claude a directement prouvé le binaire compilé pour x86 en utilisant une sémantique formelle de l'ISA x86 générée par Claude (et lourdement testée).7 Nous avons ensuite répété ce processus pour une demi-douzaine d'autres bibliothèques largement utilisées. Ce faisant, nous avons trouvé quelques bugs mineurs (non exploitables) dans des cas limites, qui sont en cours de signalement en amont. Nous tirons deux conclusions de cet exercice : (1) ces bases de code extrêmement bien testées sont déjà presque entièrement correctes, et (2) il est possible de prouver des propriétés de correction de bout en bout sur de vraies bases de code existantes.
Dans une autre expérience, nous avons demandé à Claude de développer un interpréteur pour un large sous-ensemble de Python en Rust, et de prouver (en utilisant Verus, un outil de vérification pour Rust) qu'il adhère à la sémantique de CPython décrite dans un article académique. Nous avons ensuite mesuré empiriquement l'adhérence au comportement de CPython, en exécutant plus de 1,7 million de programmes Python générés aléatoirement, et avons constaté un comportement identique à CPython dans 99,95 % des tests, les différences de tests restantes étant des cas limites connus et peu surprenants.
Nous avons également trouvé des problèmes dans plusieurs applications critiques et largement utilisées via des tentatives de vérification formelle de simples propriétés de sécurité. Dans l'une d'elles, nous avons découvert un bug logique jusque-là inconnu qui était latent depuis plus d'une décennie. Dans le cadre d'un effort pour vérifier un lecteur PDF largement utilisé, nous avons trouvé en une semaine autant de bugs de sécurité qu'il en est généralement signalé en un an.
Voir l'Appendice pour plus de détails sur certains de ces efforts.
Ce n'est que le début
L'une des principales limitations de la vérification formelle assistée par LLM est que les preuves peuvent nécessiter des centaines de millions de tokens pour être produites. L'efficacité des coûts est cruciale si notre objectif est de rendre ces méthodes accessibles à tout l'écosystème logiciel. Heureusement, il existe des raisons convaincantes de penser que l'efficacité va s'améliorer.
Les modèles plus récents ont besoin de moins de tokens
Nous avons construit 36 petites tâches de vérification à partir de code réel d'OSS-Fuzz. Opus 5.5 prouve la moitié d'entre elles avec environ 40 % de tokens en moins qu'Opus 5. Nous nous attendons à ce que cette tendance se poursuive à mesure que les modèles sont entraînés sur de longues tâches de vérification.
Les preuves peuvent être réutilisées
Lorsque les agents travaillent séparément, ils finissent souvent par dupliquer beaucoup d'efforts. Les preuves, comme les logiciels, sont construites récursivement à partir de preuves plus petites—et plus les preuves sont petites, plus elles tendent à être réutilisables. Pour mesurer l'impact de cela, nous avons laissé les agents copier les preuves des autres tandis qu'ils travaillaient à prouver leurs propres cibles. Lorsqu'ils avaient accès à cet espace de travail partagé, les agents avaient besoin de 17 % de tokens en moins que lorsqu'ils travaillaient seuls, et certains agents ont même réussi après avoir précédemment échoué dans une tentative en solo.
Nous avons observé le même phénomène se produire à grande échelle lors de notre effort de preuves sur OSS-Fuzz. L'essentiel d'une preuve concerne du code que tout programme contient (en particulier l'initialisation du runtime C et d'AddressSanitizer), si bien que des programmes très différents peuvent aboutir à des preuves présentant un chevauchement significatif. Les équipes d'agents ont exploité cela en copiant la preuve achevée d'une autre équipe, puis en l'adaptant à leur propre programme (Figure 6).
Cette réutilisabilité des preuves explique comment Mathlib, une bibliothèque partagée de mathématiques formelles en Lean, est parvenue à près de 300 000 théorèmes soumis par plus de 700 contributeurs : chaque nouvelle preuve s'appuie sur le corpus existant. Nous avons accumulé un corpus similaire de preuves au cours de notre effort sur OSS-Fuzz, dont certaines sont incluses dans notre version (nous ne publions pas les preuves qui pourraient révéler un bug non corrigé dans le logiciel open source).
Alors que nous passons de ces expériences initiales à des applications plus larges, nous avons besoin d'une stratégie pour vérifier l'énorme corpus de logiciels existants , en commençant par les dépendances les plus critiques. Comme nous l'avons montré, cela peut être réalisé à grande échelle en utilisant des spécifications génériques et en travaillant au niveau binaire, évitant ainsi de devoir réécrire des bases de code entières dans un autre langage.
Cette approche facilite également la réutilisation des preuves à une granularité de paquet, ce qui signifie que chaque dépendance n'a besoin d'être vérifiée qu'une seule fois. Les dépendances suivent une loi de puissance : prouver même un petit ensemble de bibliothèques partagées rend une immense partie des logiciels vérifiables. Pour plus de détails, voir la feuille de route de Theorem pour vérifier l'intégralité de l'écosystème Nix, qui inclut des infrastructures critiques comme glibc, OpenSSL et cURL.
Limitations
En pratique, la vérification formelle peut parfois prouver moins de choses sur la sécurité du code que nous le souhaiterions.
« Formellement vérifié » ne signifie pas « sans bug ». Claude peut écrire une preuve montrant que le comportement d'un programme compilé satisfait aux exigences d'une spécification formelle (qui est vérifiée par un vérificateur de preuves externe). Cependant, un vérificateur de preuves ne peut pas vous dire si votre spécification correspond à la réalité. Pour correspondre à la réalité, la spécification doit correctement englober et modéliser tout ce qui concerne la machine réelle sur laquelle le programme vérifié s'exécute, y compris le CPU et le système d'exploitation. Lorsque des bugs apparaissent dans du code vérifié, c'est parce que la spécification, ou les sémantiques supposées de la machine, diffèrent de la réalité. Heureusement, cela signifie aussi que nous savons où chercher les bugs restants, et comment concevoir un système où ces lacunes encore potentiellement boguées sont minimisées. Voici comment cela s'applique à nos preuves, ainsi que des pistes pour des travaux futurs qui permettraient de combler ces lacunes.
La machine réelle fait quelque chose que le modèle ne décrit pas. Nos preuves portent sur des binaires RISC-V statiques, mono-thread, liés contre musl libc. Cependant, la plupart des gens exécutent ces bibliothèques sur x86 ou ARM et les lient dynamiquement contre glibc. Pour combler cet écart, il nous faudrait des modèles système ressemblant davantage aux systèmes déployés. Par exemple, une étape dans cette direction serait de générer des sémantiques précises pour x86.
L'affirmation peut ne pas couvrir tout ce qui nous importe. Nous avons prouvé qu'aucun crash ne se déclenche pour aucune entrée de moins de 64 Mo sur de nombreux points d'entrée de fuzzing dans Google OSS-Fuzz, y compris les crashes ASan. Cependant, ASan ne détecte pas tous les bugs de sécurité mémoire, et nous n'avons pas vérifié tous les points d'entrée de chaque bibliothèque. Même si nous l'avions fait, la bibliothèque entière ne serait pas couverte par la vérification de tous les points d'entrée (surtout s'il existe du code mort). De plus, des programmes réels pourraient utiliser la bibliothèque de manière incorrecte, entraînant une corruption mémoire dans l' appelant. Pour combler cet écart, il nous faudrait spécifier ce que les appelants doivent faire pour chaque fonction publique, et les appelants devraient s'y conformer strictement.
Nous nous attendons à ce qu'à mesure que nous en apprendrons davantage sur l'exploitation des LLM pour les méthodes formelles, et à mesure que les modèles continueront de s'améliorer, ces limitations deviennent maîtrisables, et que nous puissions vérifier un pourcentage bien plus important du code sur lequel nous comptons.
Conclusion
La trajectoire est claire : la vérification formelle, qui n'était historiquement pratique que pour des garanties sur mesure élaborées par des experts dans le code le plus critique pour la sécurité, deviendra bientôt aussi pratique que le fuzzing l'est aujourd'hui pour presque tous les logiciels de production. Tout comme les types statiques, les cadres de test et autres outils de correction, la vérification mûrira d'un concept « ajouté après coup » en une fonctionnalité « intégrée », portée non seulement par les LLM mais aussi par les innovations dans la conception des langages et les flux de travail de développement.
Dans le monde d'aujourd'hui—où les LLM analysent automatiquement et trouvent un nombre croissant de vulnérabilités de code—nous devons utiliser des processus capables de garantir les propriétés de sécurité du code. La vérification formelle à l'échelle des LLM est une approche prometteuse pour sécuriser ces garanties à une portée et une échelle auparavant inaccessibles. Nous encourageons les autres à expérimenter afin que nous puissions collectivement construire un monde où les logiciels robustes se sont largement répandus et où les bugs logiciels sont une rareté bien comprise et rapidement traitable.
Notes de bas de page
01RISC-V est une conception de processeur, comme x86 ou ARM, qui définit les instructions d'assemblage (les commandes de base qu'un processeur exécute) dans lesquelles les logiciels sont compilés.
02Un point d'entrée est une porte d'entrée dans le code, fournie par ses auteurs à des fins de test. Toute entrée au point d'entrée qui provoque un plantage est un bug auquel les auteurs tiennent.
03Augmenter cela nécessite un effort humain trivial pour changer le paramètre et régénérer la spécification, puis faire re-preuver l'énoncé par Claude.
04AddressSanitizer est un outil de compilation qui ajoute des vérifications à un programme afin que les erreurs mémoire, telles que les dépassements de tampon et les use-after-free, soient détectées et signalées dès qu'elles se produisent à l'exécution.
05Cela signifie techniquement que nous devons également faire confiance au matériel, au système d'exploitation et au compilateur OCaml dont le vérificateur de preuves Rocq dépend.
06Notons que cela laisse la porte ouverte au reward hacking. Le reward hacking, c'est lorsqu'un modèle d'IA trouve un raccourci qui répond techniquement à l'objectif qui lui a été fixé sans faire ce qui était réellement prévu, comme un étudiant qui réussit un examen en mémorisant le corrigé au lieu d'apprendre la matière. Dans ce contexte, Claude pourrait rendre n'importe quel théorème prouvable en réécrivant le programme en un programme qui ne plante jamais trivialement. Pour décourager cela, nous avons pénalisé tout correctif et offert un bonus pour prouver quelles entrées il modifie et combien elles sont peu nombreuses. Nous avons également consigné et audité les correctifs pour ces modes de défaillance.
07Nous pensons que la capacité de Claude à—entièrement de manière autonome—générer la sémantique formelle d'une ISA est une leçon intéressante et distincte. Bien que nous ne puissions pas être certains que notre sémantique elle-même soit parfaite, nous avons constaté empiriquement que le pas-à-pas à travers notre sémantique permet de démarrer un espace utilisateur Ubuntu au-dessus d'un noyau Linux. La génération de cette sémantique a également permis d'identifier des centaines d'erreurs dans la documentation de référence officielle, ainsi qu'un plus petit nombre de bugs dans le matériel lui-même.