Vitalik Buterin, cofundador de Ethereum, presentó una propuesta que podría redefinir la seguridad de toda la red: usar inteligencia artificial para verificar matemáticamente que el código funcione como debe, antes de que un hacker encuentre la falla.
El planteo parte de una premisa directa: todo programa es, en el fondo, un objeto matemático, y si se lo trata así, se pueden construir pruebas automáticas que demuestren que ese código cumple con reglas específicas de seguridad.
En un ecosistema donde los contratos inteligentes manejan millones de dólares y no se pueden modificar una vez publicados, esa capacidad cambia las reglas del juego.
Buterin conectó esta técnica (llamada verificación formal) con áreas críticas de Ethereum:
El rol de la IA es central. Según Buterin, los modelos actuales ya pueden escribir código y producir pruebas formales al mismo tiempo, lo que vuelve viables procesos que antes eran demasiado caros o directamente imposibles.
Mencionó herramientas como Claude, Deepseek 4 Pro y Leanstral (un modelo de código abierto especializado) como opciones para empezar.
El esquema funciona así: se genera una versión del software optimizada para velocidad y otra pensada para que los humanos la entiendan, mientras una prueba matemática demuestra que ambas son equivalentes. La IA se encarga de escribir tanto el código como las demostraciones, y el usuario solo necesita verificar una vez que todo sea correcto.
Buterin fue claro con las limitaciones. Admitió que la verificación formal no es infalible: se puede olvidar demostrar la propiedad más importante, asumir condiciones que en la práctica no se cumplen, o verificar solo una parte del sistema mientras el resto queda expuesto.
También recordó fallos históricos en software que había sido verificado, como problemas en compiladores de C y vulnerabilidades reportadas en 2026 en herramientas de Cryspen.
"La corrección demostrable no prueba, en el sentido humano más amplio, que un software sea correcto o seguro", advirtió. Lo que sí puede hacer, aclaró, es comparar versiones redundantes de las intenciones del desarrollador y verificar si son compatibles: una forma muy potente de reducir la ambigüedad, aunque no de eliminarla por completo.
Su visión de futuro apunta a dividir el software entre "bordes inseguros" (con permisos limitados y en entornos aislados) y un "núcleo seguro" que concentre las funciones críticas. Ese núcleo debería ser pequeño, auditable y protegido con herramientas formales.
En esa categoría ubicó al propio Ethereum, partes del kernel de los sistemas operativos, piezas de hardware e infraestructura del Internet de las Cosas (IoT).
El cierre de Buterin fue contundente: si internet quiere mantener un modelo de seguridad que no dependa de confiar ciegamente en unas pocas organizaciones, va a necesitar código verificable incluso frente a atacantes potenciados por IA. Y la verificación formal asistida por inteligencia artificial es, según él, el camino más serio para lograrlo.