Las herramientas de IA generativa que escriben software se han convertido en una especie de copiloto para programadores: sugieren funciones, completan archivos enteros y proponen soluciones en segundos. El atractivo es evidente: tareas repetitivas que antes consumían horas pasan a resolverse en minutos. El inconveniente también empieza a serlo: ese mismo copiloto a veces “se inventa” detalles, comete fallos sutiles o introduce código con errores que no se detectan hasta que el proyecto ya ha crecido.
El fallo no siempre se ve como un “crash” inmediato. Puede ser una condición mal manejada, un límite no contemplado o una función que parece correcta hasta que llega el caso raro. Es como montar un mueble con un manual muy convincente, pero con un tornillo puesto donde no toca: el armario se sostiene al principio y se tambalea semanas después. Con el software ocurre algo parecido: un pequeño error se convierte en deuda técnica, ralentiza nuevas funciones y multiplica el trabajo de mantenimiento.
Lo que ya está viendo la investigación: velocidad sí, calidad no siempre
Un estudio publicado en enero por investigadores de Carnegie Mellon University, citado por The New York Times, analizó el uso de sistemas que generan código por sí mismos y encontró una tensión clara: pueden acelerar el desarrollo, pero también degradar la calidad del código, lo que termina frenando proyectos a medio plazo. Dicho sin dramatismos: el ahorro inicial puede pagarse con intereses si el equipo hereda un código menos robusto, más difícil de entender o con más fallos escondidos.
Este punto es clave porque cambia el debate. Ya no se trata solo de si la IA “programa bien” o “programa mal”, sino de cómo afecta al ciclo completo de vida del software. Si el objetivo es entregar hoy, la IA puede brillar; si el objetivo es mantener y evolucionar durante años, la historia se vuelve más compleja.
La apuesta nueva: verificación de código como hacen los matemáticos
Aquí aparece una idea que suena ambiciosa y, a la vez, muy pragmática: si la IA va a escribir más código, también necesitamos IA que lo revise con un rigor distinto al de las pruebas habituales. Varias start-ups de Silicon Valley están intentando construir sistemas de verificación de código inspirados en el método de los matemáticos cuando demuestran un teorema: no basta con que “parezca correcto”, hay que poder justificar por qué lo es, bajo ciertas reglas.
La comparación ayuda a entender el enfoque. Un test unitario es como comprobar que una receta sale bien en tu horno con tus ingredientes; la verificación formal pretende algo más parecido a demostrar que la receta funciona para cualquier horno dentro de unas condiciones definidas. En software, eso significa razonar sobre el comportamiento del programa: qué garantiza, qué no permite, qué ocurre en los bordes, y si ciertas clases de errores quedan descartadas por construcción.
Axiom, Harmonic y Logical Intelligence: el auge de los “auditores” de código
Según The New York Times, una de las compañías más visibles en esta ola es Axiom Math, con sede en Palo Alto. A pesar de su tamaño reducido, la empresa ha atraído atención e inversión: anunció una ronda de financiación de 200 millones de dólares, con participación de firmas como Menlo Ventures, Greycroft y Madrona, y una valoración de 1.600 millones de dólares. Es un contraste llamativo: una start-up de alrededor de 20 personas con cifras de “liga mayor”. La lectura que hace el mercado es clara: el problema es real y quien lo resuelva puede convertirse en pieza central del desarrollo moderno.
En el mismo tablero aparecen otras compañías como Harmonic (también en Palo Alto) y Logical Intelligence (San Francisco), que comparten una hipótesis: el gran cuello de botella del futuro no será “escribir” código, sino confiar en él. Si los generadores tipo OpenAI Codex o Anthropic Claude Code facilitan producir software a gran velocidad, alguien tendrá que garantizar que esa velocidad no se traduce en fragilidad.
Cómo podría funcionar esta “prueba de realidad” para el software
La promesa de estas soluciones no es sustituir a los ingenieros, sino ofrecer una capa de seguridad y rigor que hoy es costosa. En la práctica, la verificación formal suele requerir especialistas y tiempo, y por eso se utiliza sobre todo en sistemas críticos: sectores como aeronáutica, hardware, criptografía o componentes donde un fallo es inasumible. Lo que quieren estas start-ups es reducir ese coste usando IA, de modo que verificar sea casi tan accesible como generar.
Imagina un corrector ortográfico, pero para lógica: no solo subraya lo “mal escrito”, sino que intenta demostrar que una función cumple su contrato. Si una función promete “ordenar una lista”, el verificador no se conforma con ver un par de ejemplos correctos, sino que intenta asegurar que el resultado siempre queda ordenado y que contiene los mismos elementos. Si un módulo maneja permisos, el sistema buscaría demostrar que no existe una ruta por la que un usuario sin privilegios pueda colarse.
Este enfoque encaja bien con una realidad del trabajo diario: muchos errores no vienen de no saber programar, sino de no haber imaginado un caso límite. La IA generativa puede acelerar la escritura, pero también puede “pasar por alto” precisamente esos casos. Un verificador diseñado para cazar excepciones, contradicciones y supuestos falsos actuaría como un revisor meticuloso que nunca se cansa.
Por qué el capital riesgo está entrando con fuerza
El entusiasmo inversor tiene una lógica industrial. Si el software se produce más rápido gracias a la IA, los fallos se producirán más rápido también. El mercado busca herramientas que mantengan la confianza: reducir bugs, evitar incidentes de seguridad, y recortar el tiempo que un equipo dedica a perseguir errores en producción. En términos de negocio, es menos glamuroso que “la IA escribe apps”, pero puede ser más rentable: las empresas pagan por fiabilidad.
También hay un motivo estratégico: estas capas de verificación de código pueden convertirse en estándar dentro de la cadena de herramientas. Igual que hoy es difícil imaginar un equipo sin control de versiones o sin integración continua, mañana podría ser raro entregar código sin una “prueba” automatizada de ciertas garantías. Si una solución se integra bien con flujos ya existentes y reduce sustos, su adopción puede crecer rápido.
Los límites: lo que todavía no está resuelto
Conviene mantener los pies en el suelo. La verificación formal no es magia y depende de cómo se definan las propiedades que se quieren demostrar. Verificar “todo” es inviable; verificar “lo importante” es la clave. Un riesgo evidente es la ilusión de seguridad: creer que por tener un sello automático el sistema es infalible. Otro reto es el rendimiento: demostrar propiedades complejas puede ser computacionalmente caro. También está la cuestión de la interpretabilidad: si la IA afirma que algo es correcto, los equipos querrán entender por qué, no solo recibir un “aprobado”.
Existe un matiz práctico: muchas bases de código reales son grandes, heredadas, con dependencias y requisitos cambiantes. Llevar la verificación a ese terreno requiere herramientas que toleren la imperfección del mundo real, no solo demos limpias. La promesa de estas start-ups se pondrá a prueba ahí: en el barro cotidiano de los proyectos.
Qué puede hacer hoy un equipo que usa Codex o Claude Code
Mientras este mercado madura, hay una idea útil: separar la velocidad de la confianza. La IA generativa puede ser excelente para prototipos, para explorar alternativas o para tareas repetitivas, pero el listón de revisión debe subir cuando el código va a producción. Si la generación te da un “borrador”, la verificación y la revisión humana son la corrección ortotipográfica y la edición final.
La llegada de herramientas centradas en verificación de código sugiere un futuro donde pedirle a una IA “escribe esto” irá acompañado de “demuestra que cumple esto otro”. Suena exigente, pero también suena a madurez: como pasar de escribir rápido a escribir bien, sin renunciar a la productividad.