Anthropic presentó el 22 de octubre de 2026 una colaboración con Theorem para desarrollar pruebas formales de propiedades concretas en software de producción, compilado para arquitectura RISC-V. Estas pruebas se aplican a nivel de código ensamblador y se centran en bibliotecas específicas, sin afirmar que todas las bibliotecas estén completamente certificadas. La investigación se enfoca en un conjunto limitado de 123 bibliotecas, pero no garantiza la ausencia de errores en todas ellas.
Limitaciones de las garantías
Las pruebas formales se aplican a ciertos puntos de entrada y entradas de menos de 64 MB. El contexto incluye binarios estáticos de un solo hilo, bajo entornos RISC-V y Linux, con supuestos modelados. No se cubren todos los puntos de entrada de todas las bibliotecas, ni todos los problemas de memoria. Además, la ejecución habitual en plataformas como x86/ARM, junto con el enlazado dinámico y glibc, difiere del entorno modelado, por lo que esas garantías no se trasladan automáticamente a esos despliegues.
Implicaciones prácticas
Para un equipo que procesa archivos, es necesario definir qué propiedad se cubre, qué binario se analiza y qué parte del sistema se asume. Por ejemplo, en un parser hipotético, demostrar un límite concreto bajo ciertas suposiciones no resuelve problemas de permisos, integraciones o errores del programa llamador. Es un ejemplo hipotético para interpretar el alcance de una garantía. No hemos replicado el experimento ni ejecutado sus verificadores.
El criterio práctico sería pedir la especificación y los supuestos junto con la prueba. Un equipo podría conservar sus controles de integración y revisar qué parte de una dependencia queda cubierta antes de adaptar su evaluación. Así se evita confundir una propiedad demostrada con una certificación de todo el producto.