Anthropic et Theorem ont déclaré le 22 octobre 2026 que Claude avait contribué à produire des preuves, vérifiées par machine, d’absence de plantage pour 239 points d’entrée OSS-Fuzz répartis sur 123 bibliothèques open source, selon le billet de recherche d’Anthropic.
Le travail a été réalisé au niveau de l’assembleur RISC-V compilé, avec des preuves vérifiées par Rocq plutôt que relues manuellement. Anthropic indique également que Claude a identifié et corrigé des bugs lors des tentatives de preuve, y compris des problèmes que le fuzzing n’avait pas détectés malgré des tests antérieurs.
La garantie est plus limitée que le titre ne le laisse entendre. La principale affirmation d’Anthropic sur l’absence de plantage s’applique aux entrées de moins de 64 MB et dépend d’hypothèses explicites, notamment des binaires Linux RISC-V statiques et monothread exécutés dans une limite de mémoire fixe. Le résultat ne s’étend donc pas automatiquement à d’autres architectures ou à des chemins de code non modélisés.
Anthropic indique publier publiquement une partie des preuves et de la sémantique, tandis que Theorem propose ce pipeline à d’autres projets open source.