Vitalik Buterin Propone Verificación Formal Asistida por IA Para Blindar Ethereum Contra Ciberataques

El cofundador de Ethereum Vitalik Buterin afirmó que el software matemáticamente verificado se está volviendo esencial para proteger a Ethereum y a la industria cripto en general de los ciberataques asistidos por IA y las vulnerabilidades de software.

En una publicación de blog divulgada el lunes, Buterin argumentó que la “verificación formal” asistida por IA podría ayudar a proteger las redes blockchain, los contratos inteligentes y los sistemas cripto contra fallas de software que pueden exponer a los usuarios a pérdidas financieras irreversibles.

“Si se hace correctamente, 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, señalando que el desarrollador Yoichi Hirai lo denomina la “forma final del desarrollo de software”.

La verificación formal es una manera de comprobar matemáticamente si un software funciona correctamente, con un enfoque que se remonta a los trabajos fundacionales de los años 50 y 60. Según Buterin, los recientes avances en IA están haciendo que la técnica sea más práctica para la ingeniería de software y la investigación en seguridad.

“Si verificas formalmente de extremo a extremo, entonces estás demostrando no solo que alguna descripción del protocolo es segura en teoría, sino que el fragmento específico de código que ejecuta el usuario es seguro en la práctica”, escribió. “Desde la perspectiva del usuario, esto mejora enormemente la confianza sin necesidad de terceros: para confiar plenamente en el código, no es necesario revisar todo el código, simplemente hay que verificar las afirmaciones que se demuestran sobre él”.

La publicación de Buterin llega en un momento en que investigadores y gobiernos advierten que los modelos avanzados de IA están mejorando rápidamente en el descubrimiento y la explotación de vulnerabilidades de software. Anthropic restringió el acceso a su modelo de ciberseguridad Claude Mythos tras pruebas que demostraron que el sistema podía identificar y explotar fallas de software de forma autónoma a niveles muy superiores a los de los modelos públicos de IA anteriores.

El modelo ha captado la atención de agencias de inteligencia y seguridad debido a estas capacidades. En abril, Claude Mythos de Anthropic identificó 271 vulnerabilidades en Mozilla Firefox durante pruebas internas, mientras que a inicios de este mes, investigadores de seguridad señalaron que una versión preliminar del modelo ayudó a desarrollar un exploit dirigido a las protecciones del chip M5 de Apple. Investigadores del Instituto de Seguridad de IA del Reino Unido también encontraron que el GPT-5.5 de OpenAI ha demostrado capacidades ofensivas avanzadas en ciberseguridad.

“Los errores en el código informático dan miedo”, escribió Buterin.

Los errores no descubiertos pueden ser devastadores para los proyectos cripto, donde las fallas de software pueden ser explotadas para robar de forma permanente los fondos de los usuarios con pocas posibilidades de recuperación.

En abril, atacantes del Grupo Lazarus, respaldado por Corea del Norte, lograron drenar $292 millones en tokens de la infraestructura de Kelp DAO tras “envenenar” los RPC internos utilizados por LayerZero Labs. En total, se estima que los hackers patrocinados por el Estado norcoreano han robado más de $6.000 millones en criptomonedas hasta la fecha.

Buterin señaló que la verificación formal también podría mejorar la confianza en el software generado por IA al demostrar que el código optimizado de bajo nivel coincide con una implementación de referencia más legible.

“Una gran parte del valor añadido es que las pruebas son verdaderamente de extremo a extremo”, escribió Buterin. “Con frecuencia, los errores más problemáticos son los de interacción que se encuentran en la intersección de dos subsistemas que se analizan por separado”.

Sin embargo, aunque Buterin ve el potencial de la IA para ayudar a proteger el código de las redes cripto, advirtió que la verificación formal no puede eliminar por completo los riesgos de seguridad.

“La verificación formal no es una panacea. Pero es particularmente adecuada para situaciones en las que el objetivo es mucho más simple que la implementación”, escribió. “Esto es especialmente cierto en algunas de las piezas tecnológicas más complejas que necesitaremos implementar en la próxima gran iteración de Ethereum: firmas resistentes a la computación cuántica, STARKs, algoritmos de consenso y ZK-EVMs”.

Buterin rechazó la idea de que los ciberataques cada vez más avanzados terminarán haciendo imposible proteger el software de código abierto o los sistemas descentralizados.

“Ese sería un futuro sombrío para la ciberseguridad. Es especialmente un futuro extremadamente sombrío para quienes nos preocupamos por la descentralización y la libertad en internet”, afirmó. “El ethos cypherpunk se basa fundamentalmente en la idea de que en internet, el defensor tiene ventaja”.

En cambio, Buterin argumentó que los sistemas futuros probablemente dependerán de una infraestructura “central” altamente protegida mediante verificación formal y entornos de seguridad restringidos.

“Cuando se trata del núcleo seguro, no dejamos que el código defectuoso se multiplique”, agregó. “Actuamos de manera agresiva para mantener pequeño el tamaño del núcleo seguro, e incluso reducirlo aún más”.