{"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\/es\/blog\/news\/anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","title":{"rendered":"Anthropic desarrolla tecnolog\u00eda para la verificaci\u00f3n formal de software existente utilizando AI","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
La empresa Anthropic present\u00f3 los resultados de experimentos sobre el uso de modelos de IA para la verificaci\u00f3n formal de la fiabilidad y seguridad de proyectos existentes. Durante el experimento, se generaron pruebas matem\u00e1ticas de ausencia de errores en la gesti\u00f3n de memoria utilizando modelos de IA para 123 bibliotecas de c\u00f3digo abierto, probadas en la infraestructura de OSS Fuzz. <\/p>\n
La verificaci\u00f3n se realiz\u00f3 a nivel de c\u00f3digo ensamblador compilado para la arquitectura RISC-V. El volumen total de pruebas generadas ascendi\u00f3 a alrededor de 180 millones de l\u00edneas de c\u00f3digo para el sistema de verificaci\u00f3n Rocq Prover (aproximadamente 600 mil l\u00edneas para un archivo binario con 18 mil instrucciones RISC-V). Las pruebas se generaron a trav\u00e9s de la conversi\u00f3n autom\u00e1tica de pruebas de fuzzing existentes en especificaciones formales, tras lo cual el modelo de IA Claude demostr\u00f3 que, con cualquier entrada de hasta 64 MB, no se producen fallos en el programa. <\/p>\n
En el proceso de construcci\u00f3n de las pruebas, el modelo de IA pudo identificar y preparar correcciones para cientos de errores que no hab\u00edan sido detectados durante las pruebas de fuzzing. Entre otras cosas, se identificaron vulnerabilidades que provocan desbordamientos de b\u00fafer al procesar ciertos datos de entrada (por ejemplo, CVE-2026-56132 en libexpat), as\u00ed como errores l\u00f3gicos. Adem\u00e1s, se utiliz\u00f3 el modelo de IA para probar la conformidad de la implementaci\u00f3n del algoritmo zlib en el n\u00facleo de Linux con la especificaci\u00f3n RFC 1950.<\/p>\n
Tambi\u00e9n se gener\u00f3 un int\u00e9rprete en Rust para un subconjunto del lenguaje Python, para el cual se prepar\u00f3 una prueba formal de conformidad con la sem\u00e1ntica de CPython utilizando la herramienta Verus. Para comparar el comportamiento con CPython, se realizaron m\u00e1s de 1.7 millones de programas de Python generados aleatoriamente. En un 99.95% de los casos, los resultados de la ejecuci\u00f3n de estos programas en la nueva implementaci\u00f3n y en CPython coincidieron, y las discrepancias encontradas resultaron ser casos l\u00edmite conocidos.<\/p>\n
La verificaci\u00f3n formal realizada garantiza el cumplimiento de las especificaciones, pero no elimina completamente la posibilidad de problemas de seguridad, ya que los riesgos relacionados con problemas de multihilo, enlace din\u00e1mico y comportamientos an\u00f3malos del hardware real no quedan formalizados. La principal ventaja del enfoque propuesto es trabajar directamente con archivos binarios, lo que permite prescindir de la necesidad de reescribir el c\u00f3digo existente en lenguajes formalmente verificables. \n Fuente: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"