La IA ya escribe código funcional en cuestión de segundos. El problema no es que lo haga mal — es que nadie lo verifica matemáticamente. Y eso, según el arquitecto del lenguaje Lean, es la grieta que puede partir todo.
Leonardo de Moura, arquitecto jefe del Lean Focused Research Organization (FRO), publicó en febrero un argumento que viene ganando tracción en el debate técnico: si los modelos de lenguaje se convierten en el motor de producción de software del mundo, la humanidad necesita construir urgentemente una infraestructura que pruebe que ese código funciona correctamente — no solo que pasa los tests.
¿Qué pasó exactamente?
El contexto inmediato son dos señales que convergieron en semanas:
Claude Desbloqueado
Mi curso avanzado para aprender a sacarle mucho más provecho a Claude en el trabajo y en el día a día, con funciones y usos más potentes. Comienza el 23 de marzo.
→ Inscríbete hoy 🚀La primera: el Lean FRO demostró un experimento concreto. Tomaron zlib, la librería de compresión en C incrustada en casi todos los dispositivos del mundo, y usaron un agente de IA (Claude) para reescribirla en Lean — un lenguaje diseñado para producir código matemáticamente verificable. El resultado no solo pasó los tests de equivalencia, sino que el equipo generó una prueba formal: un teorema verificable por máquina que garantiza que descomprimir lo que comprimes siempre devuelve los datos originales. Esto, según de Moura, “no se esperaba que fuera posible todavía.”
La segunda: la startup Axiom acaba de levantar $200 millones con exactamente este enfoque — entrenar sistemas de IA para que generen salidas verificadas en Lean, atacando el mercado de código crítico donde un bug puede costar millones o vidas.
Y en la newsletter Import AI 449 (Jack Clark, ex OpenAI), de Moura fue citado directamente: “La fricción de escribir código manualmente antes forzaba un diseño cuidadoso. La IA elimina esa fricción, incluyendo la fricción beneficiosa. La respuesta no es frenar a la IA. Es reemplazar la fricción humana con fricción matemática: que la IA se mueva rápido, pero que demuestre su trabajo.”
¿Por qué la verificación formal era irrelevante antes?
Durante décadas, la verificación formal fue territorio de académicos y casos muy específicos: microchips de Intel, protocolos criptográficos, sistemas de vuelo. El motivo del abandono masivo era simple: escribir código verificable formalmente era mucho más lento que escribir código normal. Un equipo que dedicara tiempo a pruebas en Lean o Coq avanzaba a una fracción de la velocidad del equipo de al lado que escribía Python y confiaba en los tests unitarios.
Ese equilibrio cambió. Cuando la IA puede generar cientos de líneas de código en segundos, el cuello de botella ya no es la implementación — es saber si ese código hace lo que dice. De Moura lo articula así: “La verificación, el testing y la especificación han sido siempre el cuello de botella, no la implementación.”
Y añade algo que conecta con la deuda de verificación en la adopción de IA que ya discutimos en descubre.ai: el código generado por IA parece correcto pero tiene una tasa de error silenciosa que los benchmarks industriales no capturan bien.
El plan concreto: qué se quiere verificar
De Moura no propone verificar todo el software del mundo — propone una estrategia por capas, atacando primero la base crítica:
- Criptografía — porque todo lo demás le tiene fe encima
- Librerías core — estructuras de datos, algoritmos de compresión como zlib
- Motores de almacenamiento — SQLite está en literalmente cada dispositivo
- Parsers y protocolos — JSON, HTTP, DNS, validación de certificados
- Compiladores y runtimes — porque construyen todo lo demás
La idea es crear un “stack de software verificado” que sea open source, libre y con pruebas matemáticas incluidas — como hoy elegimos librerías open source por su reputación, en este futuro las elegiríamos porque traen una garantía formal.
Por qué importa ahora
Hay un patrón que se repite en la historia de la ingeniería: cuando la velocidad de producción salta un orden de magnitud, los accidentes escalan hasta que la infraestructura de seguridad atrapa el ritmo. Pasó con la aviación, los automóviles, la electricidad.
Lo que describe de Moura — y lo que Axiom está intentando comercializar — es el equivalente del código de seguridad eléctrica: un estándar de verificación que acompañe la velocidad de generación.
El timing es importante. Los agentes de IA para programar (Cursor, Claude Code, Codex, Unleash) están logrando adopción masiva en equipos de producción. Las empresas están deployando código que ningún humano leyó línea por línea. El momento de construir la infraestructura de verificación es antes de que ese código esté en sistemas críticos — no después.
La pregunta no es si la verificación formal va a importar. Es si van a llegar a tiempo de construirla.
