&Truth recauda 70 millones de dólares en una ronda semilla para crear una máquina universal de verificación de código

&Truth, una corporación de beneficio público que desarrolla tecnología para demostrar matemáticamente que el software es seguro, salió del modo sigiloso el 29 de octubre de 2026 y anunció una financiación semilla de 70 millones de dólares y un plan para crear lo que denomina una máquina universal de verificación de código.

En su anuncio de lanzamiento, la empresa dijo que se fundó a principios de 2026 y que recibió 70 millones de dólares de capital semilla de un grupo que describió como líderes pioneros en seguridad de la IA y capital de riesgo. La empresa afirmó que está creando su máquina de verificación para que pueda leer código en cualquier lenguaje de programación y demostrar matemáticamente que es seguro, protegido y correcto, con pruebas que cualquier persona pueda verificar de forma independiente.

Automatización de pruebas basada en Lean

La verificación formal existe desde hace décadas, pero antes era inaccesible y costosa, según el anuncio, porque los expertos tenían que formular las pruebas manualmente, lo que limitaba su aplicación a un puñado de sistemas críticos. La empresa afirmó que ahora la IA acelera el trabajo de demostración formal en un factor de 100 o más, y que su tecnología de automatización de pruebas acelera el proceso en otro factor de 100, reduciendo la generación de pruebas de años o meses a horas o minutos.

La empresa también describió lo que denomina tecnología de «fábrica de especificaciones», que, según afirmó, permite a empresas y desarrolladores traducir a gran escala la intención humana y los requisitos empresariales en especificaciones formales precisas, y ofrecer garantías que puedan verificarse de forma independiente, en lugar de depender de pruebas o afirmaciones de los proveedores.

&Truth está desarrollando su tecnología sobre Lean, un sistema de demostración de teoremas de código abierto, y Mathlib, una biblioteca con más de dos millones de líneas de definiciones y teoremas matemáticos, junto con tecnologías de código abierto como CSLib. Según la empresa, el objetivo es crear un vocabulario formal universal para el software: modelos matemáticos de lenguajes de programación y sistemas, técnicas de demostración y especificaciones precisas que permitan la verificación automatizada en distintos lenguajes. &Truth dijo que colabora con Lean Focused Research Organization y que tiene previsto publicar sus bibliotecas fundamentales como código abierto.

El cofundador y codirector ejecutivo Clark Barrett afirmó que Lean y Mathlib proporcionaron a la IA un lenguaje preciso para razonar en matemáticas, mientras que el software carecía de una base equivalente. El cofundador y director científico Ilya Sergey dijo que la confianza en el software debería basarse en pruebas verificables de forma independiente, no en la palabra de ninguna empresa.

Fundadores y sedes centrales en dos países

Barrett ocupa la cátedra Corbel de Informática en Stanford University, es codirector fundador del Stanford Center for AI Safety, director del Stanford Center for Automated Reasoning, cocreador de CSLib y responsable del proyecto del motor de razonamiento automatizado cvc5. Sergey fundó VERSE Lab en National University of Singapore y cocreó los verificadores de código abierto Veil y Velvet. El cofundador, codirector ejecutivo y presidente ejecutivo Chris Hsu forma parte del consejo asesor estratégico de Lean FRO y preside Infinitude Foundation; anteriormente fue director ejecutivo de Kilometre Capital y director gerente de Citadel Investment Group.

El anuncio también mencionó a Gregory Malecha, quien anteriormente dirigió el área de métodos formales en BlueRock Security y fue uno de los principales arquitectos del marco de verificación BRiCk; Sebastian Ullrich, coarquitecto de Lean 4 y cofundador de Lean Focused Research Organization; Linus Lee, exsocio gerente de Kilometre Capital; y Drew Harman, exdirector comercial de Fastino Labs y socio operativo de Insight Partners y Shasta Ventures. &Truth afirmó que se basa en décadas de investigación sobre verificación formal y razonamiento automatizado en Stanford University y National University of Singapore.

La sede de &Truth en Estados Unidos está en Palo Alto y su sede internacional, en Singapur, donde, según la empresa, su oficina ampliará considerablemente sus actividades de investigación, ingeniería, desarrollo de productos y comercialización. Low Jin Yong, vicepresidente sénior y codirector de Industria Digital de Singapur, dijo en el anuncio que la sede profundizará las capacidades de confianza y seguridad de Singapur y reforzará la posición del país como base para empresas que desarrollan IA confiable.

El sitio web de la empresa también incluye una mesa redonda con Leonardo de Moura, inventor de Lean, vicepresidente y científico distinguido de AWS, y Simone Severini, miembro del consejo asesor estratégico de Lean FRO e ingeniero distinguido de Google.

Ensayos complementarios explican los motivos de la empresa

En un ensayo complementario fechado el 29 de octubre de 2026, Hsu detalló las tendencias que, según la empresa, hacen urgente la verificación. Citó unas declaraciones del director ejecutivo de Google, Sundar Pichai, según las cuales el 75 % del código nuevo de Google ya lo genera la IA y lo aprueban los ingenieros, así como las pruebas de Veracode de 2026, que revelaron que los modelos de IA fallaron en casi la mitad de las tareas de programación en las que la seguridad era importante. El ensayo también cita una campaña de septiembre de 2026 en la que un atacante desplegó cientos de agentes de IA para vulnerar 395 organizaciones de 48 países mediante fallos en un software de gestión de impresión ampliamente utilizado, y un récord de 14.959 vulnerabilidades de software publicadas en septiembre de 2026, cifra que, según el ensayo, equivale a 3,5 veces el número publicado un año antes.

El ensayo repasa hitos anteriores de la verificación formal: la prueba original del micronúcleo seL4 requirió aproximadamente 20 años-persona de trabajo experto para unas 8.700 líneas de código; en 2015, en el marco del programa HACMS de DARPA, se integró seL4 en el helicóptero Unmanned Little Bird de Boeing, cuyos controles de vuelo un equipo rojo profesional, pese a disponer de semanas de acceso, no pudo vulnerar; y, en septiembre de 2026, un modelo de IA desarrollado por Anthropic formalizó en Lean, en 11 días, la demostración completa del último teorema de Fermat. También señala que, a principios de 2026, Kim Morrison, ingeniero sénior de software de investigación en Lean FRO, utilizó Claude, de Anthropic, con una guía humana mínima para crear una versión en Lean de la biblioteca de compresión zlib y demostrar que siempre restaura exactamente los datos que comprimió.

El ensayo cita al creador de Lean, Leonardo de Moura: «Las pruebas generan confianza. Las demostraciones ofrecen una garantía».

En un segundo ensayo publicado el 29 de octubre de 2026, Sergey explica los mecanismos de la verificación de programas y comienza con el artículo de Alan Turing de 1949, «Checking a Large Routine», que proponía que los programadores acompañaran su código de afirmaciones precisas que un verificador pudiera comprobar individualmente. El ensayo describe las especificaciones, los invariantes de bucle y las demostraciones verificadas en Lean, y afirma que el objetivo de &Truth es que los desarrolladores obtengan pruebas verificables de forma independiente —como una demostración formal en Lean— a un costo que permita integrar la verificación como una práctica habitual del desarrollo.

&Truth describe su visión a largo plazo como una transición de la «programación por intuición» a la «programación verificable», en la que el código generado por IA se verifica matemáticamente antes de su implementación, los agentes de IA operan en entornos cuya contención puede demostrarse, el software heredado se moderniza de forma segura y las infraestructuras críticas se protegen mediante garantías matemáticas verificables de forma independiente.