El cofundador de Ethereum publicó el 18 de mayo un ensayo donde argumenta que combinar inteligencia artificial con verificación formal podría ser “la forma final del desarrollo de software”. Su tesis va en contra de la narrativa dominante: la misma tecnología que facilita encontrar bugs puede usarse para probar matemáticamente que no existen.
La preocupación en el ecosistema cripto es real y creciente: si la inteligencia artificial puede encontrar vulnerabilidades en código de forma automática y a velocidad máquina, los contratos inteligentes y la infraestructura blockchain se vuelven blancos cada vez más fáciles.
Vitalik Buterin, cofundador de Ethereum, publicó el 18 de mayo el artículo “A shallow dive into formal verification”, en el que reconoció ese miedo directamente. No obstante, plantea una visión positiva a este fenómeno.
“Tengo una visión mucho más optimista, y la verificación formal asistida por IA es una gran parte de la razón.”
El argumento central: verificar de punta a punta
La verificación formal es la práctica de escribir pruebas matemáticas sobre software que una computadora puede verificar automáticamente, confirmando que el código se comporta exactamente como fue diseñado. La técnica existe desde hace décadas, pero nunca se adoptó masivamente porque generar esas pruebas manualmente era extremadamente tedioso para los desarrolladores.
La IA cambió esa ecuación. En lugar de que el desarrollador escriba las pruebas, puede pedirle a un modelo que escriba tanto el código como las pruebas que lo verifican. El desarrollador solo necesita revisar que el enunciado final probado es efectivamente lo que quería probar.
“Si se hace bien, esto tiene el potencial de producir código extremadamente eficiente y ser mucho más seguro que la forma en que se ha programado antes”, escribió Buterin, quien también mencionó que el investigador Yoichi Hirai la describe como “la forma final del desarrollo de software”.
La clave del planteamiento de Buterin es que la verificación formal funciona mejor cuando el objetivo que se quiere probar es más simple que la implementación que lo logra. Ese es exactamente el caso de las piezas más críticas de la infraestructura de Ethereum.
“A menudo, los bugs más peligrosos son los de interacción, que se encuentran en el borde de dos subsistemas considerados por separado. Para un humano, es demasiado difícil razonar sobre el sistema completo de punta a punta. Pero un sistema automatizado de verificación de reglas sí puede hacerlo.”
Esto es especialmente relevante para las áreas más complejas del roadmap de Ethereum: firmas resistentes a computación cuántica, STARKs, algoritmos de consenso y ZK-EVMs. Proyectos como Arklib trabajan hacia una implementación de STARK completamente verificada formalmente.
La eficiencia como beneficio inesperado
Buterin también señala una dimensión que va más allá de la seguridad: la eficiencia. Hoy, el código debe equilibrar legibilidad y velocidad de ejecución en un mismo objeto. Con verificación formal asistida por IA, esa tensión desaparece.
La IA puede escribir código ensamblador optimizado al máximo para velocidad, y en paralelo escribir una prueba que demuestre que ese código hace exactamente lo mismo que una implementación legible por humanos. El desarrollador verifica la prueba una vez y desde ese momento ejecuta la versión rápida con la certeza matemática de que es correcta. Dos objetos separados: uno optimiza velocidad, el otro optimiza legibilidad, y una prueba garantiza que son equivalentes.
Buterin fue explícito en que la verificación formal no es una solución absoluta. “Es fácil olvidar probar los aspectos que realmente importan. Es fácil colar suposiciones en las pruebas que resultan no ser verdaderas. Y es fácil decidir que solo una parte del sistema necesita verificación formal, pero aun así ser golpeado por un bug crítico en las otras partes.”
La verificación formal sigue siendo una capa de seguridad más, no un reemplazo de todas las demás. Buterin señaló que el objetivo es reducir la brecha entre la intención del desarrollador y el comportamiento del sistema, y que la seguridad perfecta sigue siendo imposible porque la intención humana es difícil de formalizar con precisión.
La visión de largo plazo
Buterin también escribió que “la gente debería estar abierta a la posibilidad, no certeza, de que el roadmap de Ethereum termine mucho más rápido de lo que se espera, con un estándar de seguridad mucho más alto de lo que se espera”, aunque advirtió que los desarrolladores seguirán enfrentando bugs y casos límite incluso en un futuro de IA más verificación formal.
La tesis central es clara: la IA que amenaza con hacer el código inseguro es la misma que puede hacer el código más seguro que nunca, si se combina con las herramientas correctas. Para el ecosistema cripto, donde un solo bug puede costar cientos de millones de dólares sin posibilidad de reversión, esa posibilidad no es menor.