{"id":183972,"date":"2026-10-23T11:41:12","date_gmt":"2026-10-23T09:41:12","guid":{"rendered":"https:\/\/prohoster.info\/blog\/news\/anthropic-razvivaet-tehniku-dlya-formalnoj-verifikaczii-sushhestvuyushhego-po-pri-pomoshhi-ai"},"modified":"2026-10-23T11:41:16","modified_gmt":"2026-10-23T09:41:16","slug":"anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","status":"publish","type":"post","link":"https:\/\/prohoster.info\/fr\/blog\/news\/anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","title":{"rendered":"Anthropic d\u00e9veloppe une technique de v\u00e9rification formelle des logiciels existants \u00e0 l'aide de l'IA","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
La soci\u00e9t\u00e9 Anthropic a pr\u00e9sent\u00e9 les r\u00e9sultats d'exp\u00e9riences sur l'utilisation de mod\u00e8les d'IA pour la v\u00e9rification formelle de la fiabilit\u00e9 et de la s\u00e9curit\u00e9 des projets existants. Au cours de l'exp\u00e9rience, des preuves math\u00e9matiques de l'absence d'erreurs de gestion de la m\u00e9moire ont \u00e9t\u00e9 g\u00e9n\u00e9r\u00e9es \u00e0 l'aide de mod\u00e8les d'IA pour 123 biblioth\u00e8ques open source test\u00e9es dans l'infrastructure OSS Fuzz. <\/p>\n
La v\u00e9rification a \u00e9t\u00e9 effectu\u00e9e au niveau du code assembleur compil\u00e9 pour l'architecture RISC-V. Le volume total des preuves g\u00e9n\u00e9r\u00e9es a atteint environ 180 millions de lignes de code pour le syst\u00e8me de v\u00e9rification Rocq Prover (environ 600 000 lignes pour un fichier binaire avec 18 000 instructions RISC-V). Les preuves ont \u00e9t\u00e9 \u00e9tablies par la conversion automatique des tests fuzzing existants en sp\u00e9cifications formelles, apr\u00e8s quoi le mod\u00e8le d'IA Claude a prouv\u00e9 qu'aucun plantage ne se produit dans le programme avec n'importe quelle entr\u00e9e allant jusqu'\u00e0 64 Mo. <\/p>\n
Dans le processus de construction des preuves, le mod\u00e8le d'IA a pu identifier et pr\u00e9parer des corrections pour des centaines d'erreurs qui n'avaient pas \u00e9t\u00e9 remarqu\u00e9es lors des tests fuzzing. Parmi celles-ci, des vuln\u00e9rabilit\u00e9s entra\u00eenant un d\u00e9passement de tampon lors du traitement de certaines entr\u00e9es (par exemple, CVE-2026-56132 dans libexpat), ainsi que des erreurs logiques. De plus, le mod\u00e8le d'IA a \u00e9t\u00e9 utilis\u00e9 pour prouver que l'impl\u00e9mentation de l'algorithme zlib dans le noyau Linux est conforme \u00e0 la sp\u00e9cification RFC 1950.<\/p>\n
Un interpr\u00e9teur pour un sous-ensemble du langage Python a \u00e9galement \u00e9t\u00e9 g\u00e9n\u00e9r\u00e9 en Rust, pour lequel une preuve formelle de conformit\u00e9 \u00e0 la s\u00e9mantique de CPython a \u00e9t\u00e9 pr\u00e9par\u00e9e \u00e0 l'aide des outils Verus. Pour comparer le comportement avec CPython, plus de 1,7 million de programmes Python g\u00e9n\u00e9r\u00e9s al\u00e9atoirement ont \u00e9t\u00e9 ex\u00e9cut\u00e9s. Dans 99,95 % des cas, les r\u00e9sultats d'ex\u00e9cution de ces programmes dans la nouvelle impl\u00e9mentation et dans CPython ont \u00e9t\u00e9 identiques, et les divergences observ\u00e9es se sont r\u00e9v\u00e9l\u00e9es \u00eatre des cas limites connus.<\/p>\n
La v\u00e9rification formelle r\u00e9alis\u00e9e garantit la conformit\u00e9 aux sp\u00e9cifications, mais n'exclut pas totalement l'\u00e9mergence de probl\u00e8mes de s\u00e9curit\u00e9, car les risques li\u00e9s \u00e0 la concurrence, au liage dynamique et au comportement anormal du mat\u00e9riel r\u00e9el ne sont pas formalis\u00e9s. L'avantage cl\u00e9 de l'approche propos\u00e9e r\u00e9side dans le travail direct avec les fichiers binaires, ce qui permet de se passer de la n\u00e9cessit\u00e9 de r\u00e9\u00e9crire le code existant dans des langages formellement v\u00e9rifiables. \n Source : opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"