Loading...
Serie: Serie de verificación formal · Parte 1 de 3 Público: personas completamente nuevas. No se presupone conocimiento de matemáticas, programación ni criptografía. Con qué te quedarás: una comprensión clara de lo que significa demostrar que un software es correcto, por qué eso es fundamentalmente distinto de probarlo, qué es una prueba verificada por una máquina y los límites precisos (y honestos) de lo que dicha prueba puede prometer.
La mayor parte del software es confiable porque ha sido probado: lo ejecutamos con muchas entradas y observamos su comportamiento. La verificación formal plantea una pregunta más audaz. ¿Podemos demostrar, con certeza matemática, que un sistema hace lo que debe para cada entrada posible, incluidas aquellas que a nadie se le ocurrió intentar? Este artículo desarrolla esa idea desde cero. Primero la intuición, sin símbolos hasta que sean necesarios.
Aquí tienes una historia real, y es la razón por la que existe esta serie.
En 2022, la criptomoneda centrada en la privacidad Zcash lanzó un nuevo pool blindado llamado Orchard, que permitía a las personas realizar transacciones con los importes ocultos. Durante cuatro años funcionó sin problemas y superó repetidas auditorías profesionales. Luego, en mayo de 2026, un investigador de seguridad que razonaba cuidadosamente sobre las matemáticas subyacentes (con ayuda de herramientas de IA) encontró un único punto con restricciones insuficientes en las matemáticas del sistema. Esa única brecha podría haber permitido a un atacante crear una cantidad ilimitada de dinero falsificado y, como los importes estaban ocultos, nadie habría visto que ocurría. El fallo había estado presente todo el tiempo.
No fue detectado mediante pruebas. Todas las pruebas habían pasado durante cuatro años. Fue detectado por alguien que razonó sobre las matemáticas. Y cuando el equipo lo corrigió, no se limitó a aplicar un parche y seguir adelante. Escribieron una prueba matemática verificada por una máquina, con más de 2.700 teoremas individuales, de que el reemplazo no podía contener en absoluto esa clase de fallo.
Eso es la verificación formal, y esto es lo que te ofrece: no «probamos muchos casos y funcionaron», sino «demostramos que se cumple para cada caso». Para sistemas en los que un solo caso omitido es catastrófico (dinero, aeronaves, dispositivos médicos, criptografía), esa diferencia lo es todo.
El punto ciego de las pruebas fue señalado hace décadas por el científico informático Edsger Dijkstra, y sigue siendo cierto:
Las pruebas pueden mostrar la presencia de errores, pero nunca su ausencia.
Si una prueba pasa, has aprendido que el sistema funciona con esa entrada. No has aprendido nada sobre las entradas que no probaste, y los errores peligrosos casi siempre están en los casos que nadie intentó.
Imagina que eres responsable de un edificio con mil puertas y que tu trabajo es garantizar que todas las puertas estén cerradas con llave por la noche.
La diferencia está entre muestrear la realidad y demostrar una propiedad del diseño. Las pruebas muestrean. La verificación formal demuestra. Esa es toda la idea, y todo lo demás es la maquinaria para hacerlo rigurosamente.
Toda verificación formal, sin importar lo avanzada que sea, se construye con exactamente tres ingredientes. Compréndelos claramente y el resto son detalles.
| Pilar | Significado sencillo | Analogía del edificio |
|---|---|---|
| Especificación | Una declaración precisa de lo que significa «correcto» | «Todas las puertas deben estar cerradas con llave por la noche» |
| Sistema | La cosa real que se está comprobando (un programa, un circuito, un protocolo) | El edificio y su mecanismo de cierre |
| Prueba | Un argumento riguroso de que el sistema siempre cumple la especificación | La demostración lógica de que pulsar «cerrar» cierra todas las puertas |
Y un cuarto ingrediente, más silencioso, hace que todo el conjunto sea fiable:
Entre los asistentes de pruebas que quizá escuches mencionar están Lean, Rocq (antes Coq) e Isabelle. Son, en efecto, motores extraordinariamente estrictos para comprobar lógica. La prueba de Zcash de nuestra historia inicial se escribió en Lean. Cabe destacar que los modelos modernos de IA se usan cada vez más para ayudar a escribir estas pruebas, guiados por personas, lo que ha reducido esfuerzos que antes llevaban años a semanas. La máquina sigue comprobando cada paso, de modo que la aceleración no sacrifica ninguna certeza.
La palabra «prueba» puede parecer intimidante, así que desmitifiquémosla con un ejemplo concreto y comprobable. Sin criptografía, solo aritmética escolar.
Afirmación: para cada número entero no negativo n, la suma 0 + 1 + 2 + ... + n es igual a n(n+1)/2.
Podrías probar esto. n = 5 da 0+1+2+3+4+5 = 15, y 5 × 6 / 2 = 15. ✓ Coincide. Prueba n = 10: la suma es 55 y la fórmula da 10 × 11 / 2 = 55. ✓ (Estos valores se calculan y confirman; de hecho, la afirmación se cumple para cada n de 0 a 999 al comprobarse directamente).
Pero probar valores, incluso mil de ellos, nunca alcanza «para cada número entero no negativo». Hay infinitos. Una prueba cierra esa brecha infinita con un argumento finito, mediante una técnica llamada inducción:
n = 0, la suma es simplemente 0 y la fórmula da 0 × 1 / 2 = 0. Coinciden. ✓k. Ahora suma el siguiente número, k+1. La suma hasta k+1 es (sum up to k) + (k+1) = k(k+1)/2 + (k+1). Una línea de álgebra reordena esto como (k+1)(k+2)/2, que es exactamente la fórmula con k+1 en lugar de k. ✓Como se cumple al inicio (0) y cada paso la lleva al siguiente número, se cumple para todos los números enteros no negativos, para siempre, en un único argumento finito. Eso es una prueba. Un asistente de pruebas realiza exactamente este razonamiento, pero verifica mecánicamente que cada paso, incluida la «línea de álgebra», se siga realmente de lo anterior.
El salto que vale la pena interiorizar: una prueba convierte «infinitos casos» en un argumento finito y comprobable. Esa es la superpotencia que las pruebas carecen estructuralmente.
La verificación formal es poderosa en parte por una idea esclarecedora sobre dónde surgen los errores en primer lugar. Cualquier fallo en un sistema que comprueba reglas se remonta a uno de tres lugares:
| Origen de un error | Qué significa | ¿Podemos eliminarlo mediante una prueba? |
|---|---|---|
| La especificación | Las matemáticas o las reglas mismas son erróneas (falta una condición, hay una mala definición) | Sí, directamente; este es el terreno propio de la verificación formal |
| La implementación | El código no ejecuta fielmente una especificación correcta | En parte; a menudo tales fallos dejan evidencias detectables |
| Una suposición rota | Algo de lo que depende todo el sistema resulta ser falso | No; las suposiciones son el fundamento irreducible |
Esta taxonomía importa más de lo que parece, y las Partes 2 y 3 giran en torno a ella. Los errores más profundos y peligrosos, los que pueden permanecer ocultos para siempre, suelen vivir en la especificación: la descripción matemática de lo que se supone que debe hacer el sistema. Y la especificación es exactamente lo que una prueba verificada por una máquina puede examinar directamente, todos los casos a la vez. Por eso los esfuerzos serios de verificación formal apuntan primero allí.
La verificación formal es poderosa, pero su promesa es precisa, y malinterpretarla desvía a las personas. Así que expresémosla con cuidado:
Una prueba garantiza que el sistema cumple la especificación, bajo las suposiciones declaradas. Nada más.
De ello se siguen cuatro consecuencias, y cada una importa:
Lejos de debilitar la verificación formal, esta precisión es su fortaleza. Te dice exactamente lo que estás obteniendo. Como veremos en la Parte 3, el equipo de Zcash que declara claramente su alcance y sus suposiciones («demostramos la solidez del suministro, bajo estas suposiciones nombradas, y no la privacidad») es un modelo de esa honestidad.
Para mantener esto legible, simplificamos. Las especificaciones reales se escriben en lenguajes formales precisos, no en frases en inglés; existen varios estilos de verificación formal (demostración interactiva de teoremas, comprobación de modelos, métodos basados en SMT) adecuados para distintos problemas; y escribir estas pruebas sigue siendo un trabajo especializado y exigente incluso con ayuda de IA. También omitimos cómo un asistente de pruebas representa internamente la lógica. Nada de esto cambia el núcleo: una especificación, un sistema y una prueba verificada por una máquina de que ambos coinciden, bajo suposiciones declaradas. Los detalles regresarán cuando los necesitemos.
| Término | Significado en lenguaje sencillo |
|---|---|
| Formal verification | Demostrar matemáticamente que un sistema cumple una especificación en todos los casos |
| Specification | Una declaración precisa de lo que significa «comportamiento correcto» |
| System | El programa, circuito o protocolo real que se está comprobando |
| Proof | Una cadena finita de pasos lógicos que establece una afirmación para todos los casos |
| Proof assistant / theorem prover | Software (Lean, Rocq, Isabelle) que comprueba cada paso de una prueba |
| Machine-checked | Verificado paso a paso por una computadora, no solo mediante lectura humana |
| Induction | Una técnica de prueba: es verdadera al inicio y cada paso la lleva al siguiente |
| Assumption | Una condición de la que depende la prueba; si es falsa, la garantía puede no cumplirse |
¿La verificación formal reemplaza las pruebas? No. Se complementan. Las pruebas detectan problemas prácticos y suposiciones erróneas de manera económica; la verificación descarta clases completas de errores que las pruebas quizá nunca muestreen.
Si es tan poderosa, ¿por qué no todo se verifica formalmente? Es costosa y exige habilidades especializadas, aunque la ayuda de IA está reduciendo ese coste. Se reserva para sistemas en los que un error poco frecuente sería catastrófico, que es precisamente donde su coste compensa.
¿Un sistema verificado formalmente aún puede fallar? Sí, si la especificación era errónea, una definición estaba mal formulada, una suposición no se cumplía o el fallo se encuentra fuera de lo especificado. La prueba solo cubre aquello que afirma cubrir.
¿Una prueba verificada por una máquina es más fiable que una humana? Para pruebas grandes e intrincadas, generalmente sí. Una máquina no pasará por alto una brecha sutil ni aceptará una afirmación sin justificación, aunque sigue confiando en la especificación y las definiciones que recibió.
Si la IA ayuda a escribir la prueba, ¿por qué confiar en ella? Porque el asistente de pruebas comprueba mecánicamente cada paso. La IA propone pasos; la máquina los verifica. Un paso erróneo simplemente se rechaza, por lo que la IA acelera el trabajo sin debilitar la garantía.
Demuestras que el software de un banco «nunca permite que el saldo de una cuenta sea negativo». Un año después, el dinero sigue desapareciendo. ¿Cómo pueden ser ciertas ambas cosas a la vez? (Respuesta abajo.)
La prueba garantizaba exactamente una propiedad: que los saldos nunca fueran negativos. El dinero puede desaparecer de formas que esa propiedad nunca abordó, por ejemplo, por un error que mueve fondos a la cuenta equivocada (que aun así no queda en negativo), o por un fallo en una parte del sistema que nunca se especificó. La verificación hizo exactamente lo que prometía y nada más. Esta es la advertencia de la Sección 6 en acción: una prueba cubre la especificación, no toda noción concebible de «correcto».
Parte 2 · El error de Orchard: nos adentramos en la historia real de 2026 en su totalidad. Un sistema de privacidad ocultaba importes mediante pruebas criptográficas, y una línea con restricciones insuficientes en sus matemáticas significaba que esas pruebas podían hacerse mentir, permitiendo falsificación invisible ilimitada. Veremos exactamente qué significa «un circuito con restricciones insuficientes», por qué esta clase de error puede ocultarse para siempre y por qué ha ocurrido más de una vez.
Parte de la serie de verificación formal para ZecHub.