Anthropic : Claude prouve l'absence de crash sur 239 points d'entrée de 123 bibliothèques OSS-Fuzz

Anthropic publie le 22 octobre avec Theorem une démonstration à grande échelle de vérification formelle assistée par Claude : conversion des suites fuzz en spécifications, génération de preuves en Rocq au niveau assembleur RISC-V. Claude a patché puis prouvé l'absence de crash jusqu'à 64 Mo d'entrée pour 239 points d'entrée répartis sur 123 bibliothèques OSS-Fuzz, soit environ 180 millions de lignes Rocq. Au passage, le processus révèle des underflows, des accès mémoire hors bornes et des bugs logiques inédits.