Verificación de software: el muro que Turing alzó en 1936

Qué dice el ensayo: la corrección choca con la teoría de la computación

Stefan O’Rear construyó una máquina de Turing de 1.919 estados —equivalente a un programa de Python de 100 a 200 líneas— cuyo comportamiento no se puede demostrar jamás. No porque analizarla resulte caro, sino porque las matemáticas conocidas (el sistema ZFC) no alcanzan a probar si termina o no. Si un programa de un par de páginas no se puede entender del todo, la promesa de «software correcto garantizado» tiene un techo estructural, no tecnológico.

Un ensayo publicado en pron.github.io repasa los resultados de la computabilidad y la complejidad que explican por qué los programas y la comprensión completa están en conflicto permanente. La tesis incomoda a cualquiera que venda herramientas de verificación: el costo de la corrección es una consecuencia de las «leyes naturales» de la computación y no se puede evitar.

La historia arranca hace casi un siglo. El matemático David Hilbert propuso formalizar toda la matemática y demostrar tres cosas: consistencia (sin contradicciones), completitud (toda afirmación verdadera es demostrable) y decidibilidad (un algoritmo que determine si cualquier afirmación es un teorema). En su conferencia de retiro, en 1930, sostuvo que no existía problema irresoluble: Wir müssen wissen. Wir werden wissen. Un día antes, Kurt Gödel había anunciado su primer teorema de incompletitud, que demolía dos de los tres pilares. En 1936, Alonzo Church y Alan Turing derribaron el tercero con el teorema de la parada.

¿Y esto cómo se aplica en tu negocio?

Dueños de negocio de Latinoamérica y España usan un agente de IA para ganar más y recuperar su tiempo. El Kit «tu mano derecha con IA» te muestra cómo en un video de 11 minutos, con una ficha para armar el tuyo. CAR está cerrada por ahora; al anotarte, te avisamos cuando abra.

👥 Quiero el Kit →

¿Por qué la verificación de software es imposible en el caso general?

El teorema de la parada es la primera ley de la computación: no existe un algoritmo que, dado un programa cualquiera, determine si termina. Se demuestra por diagonalización —autorreferencia, la misma idea que usó Gödel— construyendo un programa que hace lo contrario de lo que el supuesto verificador predice.

De ahí se derivan tres consecuencias que golpean directo al negocio de las herramientas de verificación:

Alcanzabilidad: no existe un programa que determine si otro llega alguna vez a un estado concreto partiendo de ciertos estados iniciales.
Teorema de Rice: para cualquier propiedad no trivial de las funciones que un programa puede computar, no hay algoritmo capaz de decidir si ese programa tiene la propiedad. Por ejemplo, no se puede determinar automáticamente si la salida de un programa es siempre el cuadrado de su entrada.
El «teorema del castor ocupado»: la función que relaciona el tamaño de un programa con el número máximo de pasos que puede dar antes de detenerse no es computable, y cualquier función que se sepa mayor que esa tampoco lo es. Para n = 6, ese número supera 7,4 × 10^36534.

La misma barrera aparece en la vista estática del código: el tamaño de la prueba más corta de terminación, en función del tamaño del programa, tampoco es computable. Dicho de otro modo, no existe atajo matemático que reemplace entender el código.

El punto crítico para un founder es que estos límites no aplican solo a programas exóticos escritos por académicos. El ensayo describe un ejemplo de 10 líneas de Java o C, con bucles de contador decreciente —o sea, escrito para que siempre termine—, que falla si y solo si la conjetura de Goldbach es falsa. Los matemáticos llevan 270 años sin poder resolverla. El problema no es que el programa sea raro: es que su comportamiento es tan difícil de analizar como un problema abierto de teoría de números.

Si la imposibilidad no alcanza, la complejidad tampoco perdona

Hasta aquí el argumento es de imposibilidad. Pero incluso cuando un problema es decidible existe un muro de tiempo. Juris Hartmanis y Richard Stearns fundaron la teoría de la complejidad en 1965, y en su conferencia del Premio Turing de 1993 Hartmanis describió esas restricciones como leyes de la naturaleza, comparables a las de la física.

El resultado central para quien construye producto es el bounded halting: decidir si un programa se detiene dentro de n pasos no se puede resolver, en el peor caso, en menos de n pasos. Traducido: no se puede saber qué hará un programa más rápido que ejecutándolo. Y no se arregla acumulando análisis previo: el ensayo introduce una variante que llama amortized bounded halting y demuestra que tampoco hay ganancia por amortizar.

Hay un dato que conviene tener a mano ante cualquier proveedor de verificación: el ensayo demuestra que todo problema de decisión con cota de complejidad conocida se reduce a bounded halting. Es decir, la verificación es el problema más difícil de la computación, no un caso particular.

Pero mi lenguaje ya garantiza esto: por qué los lenguajes totales no ayudan

Uno de los mitos que el texto desarma es que basta con restringir el lenguaje. Los lenguajes totales obligan a que todos los bucles y llamadas recursivas tengan un contador que decrece, de modo que todo programa termina por construcción. Parece la solución: si nada no termina, la verificación debería volverse tratable.

No lo es. La prueba de diagonalización sigue funcionando dentro de un lenguaje total y el costo se mantiene en Ω(|S|), es decir, proporcional a la cantidad de estados del programa. Peor aún: cualquier programa real puede volverse total agregando un contador enorme —por ejemplo 2^100— a cada bucle, sin cambiar su comportamiento físico. Si los lenguajes totales ayudaran, ya podríamos asumir que todos los programas lo son.

El ensayo también menciona restricciones más agresivas, como los lenguajes donde todo programa es computable en tiempo polinomial (Bellantoni y Cook) o los autómatas de pila. Todas ayudan en nichos, ninguna convierte el problema general en barato.

¿Qué verificación de software sí funciona en producción hoy?

El ensayo no propone rendirse, y el ecosistema muestra resultados medibles. Kani, un model checker abierto para Rust —así se llama a las herramientas que exploran simbólicamente los caminos de un programa—, corre en la integración continua de proyectos de producción, según un paper publicado en arXiv: Firecracker, el monitor de máquinas virtuales detrás de AWS Lambda y AWS Fargate; s2n-quic, la implementación de Amazon del protocolo QUIC; y la campaña de verificación de la librería estándar de Rust, que verifica más de 16.748 arneses por cambio de código.

Los números que importan para decidir:

11 bugs encontrados en cuatro bases de código Rust en producción que los tests y el fuzzing no vieron.
En s2n-quic, el fuzzer corrió 16,7 millones de ejecuciones sobre una función sin encontrar nada; Kani detectó el fallo en 20 segundos. Otro bug comparable cayó en 2,8 segundos.
En Firecracker, Kani encontró un error de redondeo que permitía a un invitado exceder su cupo de E/S en hasta 0,01%, un fallo dependiente del tiempo que los tests no pueden controlar de forma determinista.
Los tiempos de CI del paper van de menos de un minuto a unos 69 minutos, con la mayoría por debajo de 25 minutos por pull request.

El esfuerzo también es medible, y es el dato más honesto sobre el «costo de la corrección». El mismo paper cita los casos de Verus presentados en SOSP 2024, con unas 5 líneas de prueba por cada línea de implementación (6.100 líneas de código y 31.000 de prueba). En Hifitime, una librería de gestión de tiempo de 9.500 líneas, se llegó a 153 pruebas funcionales con 125 anotaciones de contrato.

En resumen: la verificación existe y encuentra bugs reales, pero se compra por componente crítico y con esfuerzo de ingeniería, no como un interruptor.

¿Qué significa esto para tu startup?

Aplicar estas conclusiones no requiere un equipo de teoría de la computación. Requiere cambiar tres decisiones.

Deja de evaluar herramientas por la promesa. Cuando alguien te diga que su producto «garantiza» corrección, haz tres preguntas: ¿qué propiedad exacta se verifica?, ¿sobre qué parte del código?, ¿qué supuestos quedan afuera? Los contratos verificados son sólidos solo si el arnés cubre los inputs reales; Kani, por ejemplo, no modela hilos ni ejecución asíncrona. Si no hay respuesta concreta, la garantía es marketing.
Verifica por radio de explosión, no por cobertura. Firecracker aplicó model checking al limitador de E/S y a la emulación de dispositivos, no a todo el monitor. s2n-quic lo aplicó al parseo de paquetes, donde un byte de más o de menos importa. Identifica en tu producto los tres lugares donde un bug cuesta dinero, datos o seguridad —pagos, permisos, criptografía, límites de uso— y concentra ahí el presupuesto.
Suma verificación incremental en CI en lugar de un proyecto de verificación total. El material de Kani muestra que los arneses conviven con cargo test y con el fuzzing existente. Empieza por chequeos sin anotaciones (desbordes, pánicos, memoria) y sube a contratos solo donde el costo se justifique.

Y una advertencia específica sobre el código generado por IA. El paper relata que la especificación de Hifitime se escribió con asistencia de IA y que tres contratos generados automáticamente fallaron la verificación. Los tres fueron atrapados por el verificador, no por revisión humana. Dos conclusiones: la especificación es el nuevo cuello de botella, y la confianza no se delega, se verifica. Eso es lo contrario del atajo que muchos founders buscan cuando le piden a un modelo que «escriba código correcto».

Por último, un cambio de expectativa. Si la verificación es el problema más difícil de la computación, tu estrategia de calidad no puede depender de una sola técnica. Tipos fuertes, tests, fuzzing, revisión y model checking cubren cosas distintas y se complementan. La pregunta útil no es «¿cómo hago software 100% correcto?» —imposible en el caso general— sino «¿cuánto me cuesta el próximo nivel de garantía y vale la pena en este módulo?».

Conclusión

El ensayo es incómodo porque no deja espacio para el atajo. Turing y Church mostraron que la corrección completa choca con las leyes de la computación, y Hartmanis mostró que incluso donde existe decisión existe un costo que no se puede amortizar. La buena noticia es que esa misma teoría explica por qué las herramientas de verificación funcionan donde funcionan: en componentes acotados, con propiedades bien definidas y con presupuesto explícito de ingeniería.

Para un founder, la lectura práctica es sencilla. No compres certezas absolutas, compra cobertura donde el error duele. Y cuando alguien prometa verificación total sin costo, ya sabes que está vendiendo algo que las matemáticas no permiten.