LO ESENCIAL EN 30 SEGUNDOS

  • &Truth anunció el 29 de octubre una ronda semilla de 70 millones de dólares; solo describe a sus inversores como líderes en seguridad de la IA y capital riesgo.
  • La empresa desarrolla lo que llama una máquina de verificación universal, pensada para demostrar que el código es seguro y correcto, sobre el asistente de pruebas Lean.
  • Entre los cofundadores están Clark Barrett, profesor de Stanford, e Ilya Sergey, de la Universidad Nacional de Singapur; las mejoras de velocidad que promete no están verificadas de forma independiente.

Una nueva startup quiere sustituir la confianza en el código generado por IA por una demostración matemática. &Truth, una corporación de beneficio público fundada a principios de 2026, salió del modo sigiloso el 29 de octubre con 70 millones de dólares de financiación semilla, según un comunicado distribuido por Business Wire desde Palo Alto y Singapur. No ha revelado sus inversores, a los que presenta como referentes de la seguridad de la IA y del capital riesgo.

Qué está construyendo

&Truth asegura que desarrolla una "máquina de verificación universal" para software: un sistema que lee código escrito en cualquier lenguaje de programación, intenta demostrar que es seguro, protegido y correcto, y entrega pruebas que terceros pueden comprobar por su cuenta. Se apoya en Lean, un asistente de pruebas de código abierto, y en su extensa biblioteca de matemáticas formalizadas Mathlib, además de CSLib, una biblioteca de informática. La compañía describe también una "fábrica de especificaciones" que traduce requisitos de negocio en especificaciones formales contra las que se comprueban las pruebas. Afirma que publicará sus bibliotecas fundamentales como código abierto y que colabora con la Lean Focused Research Organization.

El equipo fundador procede sobre todo de la investigación en métodos formales. El codirector ejecutivo Clark Barrett es profesor de informática en Stanford y lidera el proyecto del motor de razonamiento cvc5; el director científico Ilya Sergey fundó el laboratorio VERSE en la Universidad Nacional de Singapur; y el codirector ejecutivo y presidente Chris Hsu fue consejero delegado de Kilometre Capital. La sede estadounidense está en Palo Alto y la internacional en Singapur, donde la empresa prevé crecer.

Promesas y salvedades

La propuesta parte de la distancia entre la velocidad con la que la IA escribe código y la lentitud de la revisión humana. Hsu lo resume sin rodeos: "In the AI era, even 99% safe is certainly broken". La empresa sostiene que la IA ya acelera la generación de pruebas 100 veces o más y que su propia automatización suma otro factor de 100, de modo que trabajos de meses o años pasarían a durar horas o minutos. No ha publicado resultados de referencia que respalden esas cifras.

TokenPost señala además un límite de fondo: una prueba solo garantiza lo que dice la especificación, dentro del modelo del sistema utilizado. No demuestra que los requisitos recojan todo lo que necesitan los usuarios ni que el modelo refleje todas las condiciones reales. La verificación formal ha sido históricamente costosa; Unite.AI recuerda que la prueba del núcleo seL4 requirió unos 20 años-persona para unas 8.700 líneas de código. Está por ver si &Truth logrará que estas garantías sean habituales en el software cotidiano.