La startup &Truth anunció que obtuvo 70 millones de dólares estadounidenses en financiación semilla para desarrollar herramientas de inteligencia artificial que ayuden a verificar software mediante pruebas matemáticas. Su objetivo es reducir el tiempo y el trabajo que exige la verificación formal, una técnica que comprueba si el código cumple requisitos definidos con precisión.
La empresa, que salió del periodo en que operaba de manera reservada el 29 de octubre de 2026, quiere llegar a verificar programas escritos en cualquier lenguaje. Es una meta de desarrollo. Según WIRED, aún no está claro si la IA permitirá extender esta técnica más allá de los sistemas críticos hasta un uso generalizado.
Qué demuestra una prueba matemática
Las pruebas convencionales ejecutan un programa con distintas entradas para detectar fallas. La verificación formal parte de un modelo y de una especificación, es decir, una descripción precisa de lo que se quiere comprobar. Con ella se intenta demostrar que una propiedad se cumple para todas las entradas contempladas bajo determinados supuestos.
Por ejemplo, si un programa ordena una lista, una propiedad verificable sería que la lista resultante conserve los mismos elementos. Esa prueba no demostraría por sí sola que el programa proteja correctamente los datos o que funcione como espera el usuario en todos los demás aspectos.
&Truth dice que trabaja tanto en la automatización de las pruebas como en una tecnología para traducir necesidades expresadas por personas a especificaciones formales. Entre sus fundadores están Clark Barrett, profesor de Stanford, e Ilya Sergey, investigador de la Universidad Nacional de Singapur. La empresa tiene sedes en Palo Alto, California, y Singapur.
Una prueba con IA y sus condiciones
Una investigación presentada por Chuyue Sun y otros autores, entre ellos Barrett, muestra por qué existe interés en automatizar este trabajo. Ambos figuran afiliados a Stanford y &Truth en la versión consultada del estudio, disponible como prepublicación. El trabajo presenta un sistema de investigación llamado CryptoProver; el anuncio de &Truth no lo identifica como su producto.
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 en uso de la API, según el artículo.
Los autores mencionan que una verificación humana previa implicó a tres personas durante cinco meses, pero advierten que los plazos no son directamente comparables. El reloj de CryptoProver empezó después de recibir contratos, una biblioteca de apoyo, la división de tareas y el orden de las pruebas. La cifra de la API tampoco equivale al costo total del proyecto.
La demostración 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.
Más empresas persiguen la misma idea
Harmonic anunció el 27 de octubre que su herramienta Aristotle admite verificación de software en C y diseños de hardware en Verilog. La empresa afirma que 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.
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 refleja lo que las personas necesitaban. Anthropic también advierte que el modelo de la máquina y el sistema operativo puede diferir del entorno real, por lo que una verificación formal no significa que el software esté libre de errores.
