Anthropic affirme que Claude a généré des preuves formelles au niveau assembleur pour 123 bibliothèques open source

Anthropic a collaboré avec la société de vérification formelle Theorem pour convertir les tests par fuzzing existants de projets open source en spécifications mathématiques, rédigées ensuite par Claude sous forme de preuves vérifiées par le vérificateur de preuves Rocq. Anthropic a déclaré que l'équipe a achevé en quelques semaines la preuve de 123 bibliothèques open source et de 239 points d'entrée de test, représentant au total environ 180 millions de lignes de code. La conclusion principale est que, pour des entrées inférieures à 64 Mo, dans les conditions de réponse Linux et de disposition mémoire définies, les points d'entrée de test corrigés et compilés en programmes RISC-V spécifiques ne plantent pas en raison d'erreurs de sécurité mémoire ou d'échecs d'assertions. Lors de la rédaction des preuves, Claude a également identifié et corrigé des problèmes non détectés par les tests antérieurs, notamment des lectures et écritures hors limites déclenchées uniquement par des entrées rares. Contrairement au fuzzing, qui repose sur un échantillonnage répété, les preuves formelles couvrent toutes les entrées dans le périmètre défini ; toutefois, la validité des conclusions dépend de l'exactitude des spécifications, du modèle machine et du vérificateur. Actuellement, les preuves principales concernent des conditions d'exécution spécifiques telles que le monofil et l'édition de liens statique, et ne couvrent pas l'intégralité du code de chaque bibliothèque. Anthropic a publié certaines preuves afin de permettre une vérification et une réutilisation par la communauté. Cette étude démontre le potentiel de l'IA pour réduire la charge de travail de la vérification formelle, mais ne permet pas de conclure que les 123 bibliothèques sont « exemptes de vulnérabilités ».