Harmonic amplía su IA Aristotle a la verificación formal de software en C y diseños de chips en Verilog

Harmonic, la startup cofundada por el consejero delegado de Robinhood, Vlad Tenev, anunció el 27 de octubre de 2026 que su sistema Aristotle da el salto de las demostraciones matemáticas a la verificación de software y hardware. Los dos primeros lenguajes compatibles son C, para programas, y Verilog, para el diseño de chips.

Qué comprueba ahora Aristotle

Aristotle se basa en pruebas comprobadas por máquina. Harmonic quiere demostrar que ciertas propiedades se cumplen para todas las entradas posibles de un sistema definido, en lugar de probar solo una muestra de casos. En C, la empresa dice que puede verificar el software frente a requisitos concretos, como la corrección funcional y la ausencia de algunos tipos de comportamiento indefinido. En Verilog, abarca propiedades de control, como seguridad y vivacidad, además de propiedades matemáticas de las rutas de datos.

El flujo de trabajo propuesto tiene cuatro pasos. Aristotle sugiere propiedades a partir del código y después indica cuáles ha logrado demostrar, cuáles no y en qué supuestos se apoya cada prueba. Una vez revisadas y guardadas en el repositorio por los ingenieros, se vuelven a comprobar en integración continua en cada commit.

Primeros resultados según la empresa

Harmonic ofrece dos ejemplos. En la empresa de chips Tensordyne, afirma que Aristotle encontró errores a hasta 110.000 ciclos de profundidad en el bloque que el equipo consideraba más difícil de verificar. En LibTomMath, una biblioteca de código abierto para números grandes que usan Tcl y Dropbear SSH, dice que corrigió tres errores y aceleró la exponenciación modular entre un 31 % y un 38 % en sus propias mediciones, con el código más rápido demostrado frente a la misma especificación. Reuters informa además de que el centro de fusión estadounidense DIII-D asegura que Aristotle reconstruyó parte de su software de control del reactor en cuatro horas, a partir de un artículo científico.

Ninguno de estos resultados se ha reproducido de forma independiente.

Por qué importa

La verificación formal sigue siendo cara y propia de especialistas. Harmonic sostiene que el aumento del código generado por IA convierte la revisión en un punto débil y que las pruebas comprobadas por máquina pueden cubrir parte de ese hueco. Su consejero delegado, Tudor Achim, lo ve como una nueva forma de detectar defectos y vulnerabilidades.

Aristotle ya está disponible en aristotle.harmonic.fun con pago por consumo, y los planes empresariales suman precios por volumen, soporte dedicado y despliegue local o en nube privada. El anuncio no detalla qué partes de C o Verilog se admiten ni qué lenguajes llegarán después.