✨︎ Resumen (TL;DR):
- &Truth consiguió 70 millones de dólares en financiación semilla para desarrollar IA que automatice pruebas matemáticas del software.
- CryptoProver generó especificaciones internas y pruebas de corrección funcional para curve25519-dalek en 11.4 horas, con 466.99 dólares registrados en uso de API.
- La startup quiere verificar programas en cualquier lenguaje, pero la especificación y el entorno determinan qué puede garantizar cada prueba.
&Truth obtuvo 70 millones de dólares en financiación semilla para desarrollar herramientas de inteligencia artificial que automaticen la verificación formal de software. La startup dejó atrás el periodo en que operaba de manera reservada el 29 de octubre de 2026 y quiere reducir el tiempo y el trabajo que requieren las pruebas matemáticas, con la meta de revisar programas escritos en cualquier lenguaje.
Qué comprueba una prueba matemática
La verificación formal es una técnica de análisis que intenta demostrar, mediante pruebas matemáticas, que una propiedad del software se cumple para todas las entradas contempladas bajo determinados supuestos.
Las pruebas convencionales ejecutan un programa con distintas entradas para buscar fallas. La verificación formal parte de un modelo y de una especificación, una descripción precisa de lo que se quiere comprobar.
Si un programa ordena una lista, una propiedad verificable sería que el resultado conserve los mismos elementos. Esa prueba no demostraría por sí sola que el programa proteja correctamente los datos ni que funcione como espera el usuario en todos los demás aspectos.
El plan de &Truth
&Truth trabaja en dos frentes: automatizar las pruebas y desarrollar una tecnología que traduzca necesidades expresadas por personas a especificaciones formales. La empresa presenta la posibilidad de verificar programas en cualquier lenguaje como una meta de desarrollo, no como una capacidad ya demostrada.
Entre sus fundadores están Clark Barrett, profesor de Stanford, e Ilya Sergey, investigador de la Universidad Nacional de Singapur. La startup tiene sedes en Palo Alto, California, y Singapur.
WIRED reportó que todavía no está claro si la IA permitirá extender esta técnica más allá de los sistemas críticos hasta un uso generalizado.
CryptoProver pone cifras a la automatización
Una investigación presentada por Chuyue Sun y otros autores, entre ellos Barrett, describe un caso concreto. El estudio está disponible como prepublicación y, en la versión consultada, Chuyue Sun y Clark Barrett aparecen afiliados a Stanford y &Truth.
El trabajo presenta CryptoProver, un sistema de investigación. El anuncio de &Truth no lo identifica como un producto de la startup.
Los investigadores aplicaron CryptoProver a curve25519-dalek, una biblioteca criptográfica utilizada en Signal. El sistema generó especificaciones internas y pruebas de corrección funcional en 11.4 horas, con un gasto registrado de 466.99 dólares por uso de la API, según el artículo.
El dato requiere contexto. Los autores mencionan que una verificación humana previa involucró a tres personas durante cinco meses, pero advierten que ambos plazos no se pueden comparar directamente.
La medición de CryptoProver comenzó después de recibir contratos, una biblioteca de apoyo, la división de tareas y el orden de las pruebas. Además, la cifra de la API no equivale al costo total del proyecto.
Lo que la prueba sí y no demostró
El experimento comprobó la corrección funcional frente a los requisitos suministrados. Los autores señalan que no probó, por ejemplo, la seguridad criptográfica ni la resistencia a ciertas filtraciones de información.
La calidad de la especificación sigue siendo decisiva. Una prueba puede confirmar que el código cumple lo que se pidió formalmente, pero no determinar por sí sola si ese requisito representa lo que las personas necesitaban.
Anthropic también advierte que el modelo de la máquina y el sistema operativo pueden diferir del entorno real. Por eso, una verificación formal no significa que el software esté libre de errores.
Otras herramientas buscan la misma automatización
El 27 de octubre, Harmonic anunció que su herramienta Aristotle admite la verificación de software en C y de diseños de hardware en Verilog. Según la empresa, el sistema propone propiedades para revisar y comunica cuáles pudo demostrar y bajo qué supuestos.
Por separado, Anthropic y la startup Theorem informaron que usaron Claude para probar propiedades de seguridad en partes de más de 100 bibliotecas de código abierto. Sus resultados se limitaron a puntos de entrada y condiciones concretas; no abarcaron todas las funciones ni todos los entornos en que se usan esas bibliotecas.
&Truth quiere reducir el tiempo y el trabajo de la verificación formal, pero el resultado de cada prueba seguirá dependiendo de la especificación suministrada, los supuestos y el entorno de ejecución. Los casos descritos muestran automatización en escenarios delimitados, no una garantía de que cualquier software esté libre de errores. La pregunta pendiente es si la IA permitirá extender esta técnica más allá de los sistemas críticos hasta un uso generalizado.
