Vitalik: la verificación formal asistida por IA es «la forma definitiva de desarrollo de software», Ethereum en el centro de la seguridad

Vitalik Buterin, cofundador de Ethereum, publicó el 18 de mayo un análisis en profundidad sobre el estado y las perspectivas de la verificación formal (Formal Verification). Considera que la verificación formal asistida por IA se convertirá en «la forma final del desarrollo de software» y señala que Ethereum será una parte importante de la futura arquitectura de «núcleo de seguridad».

Principios centrales y casos de uso de la verificación formal

Según la confirmación del artículo de Vitalik, la verificación formal es especialmente adecuada para escenarios en los que «el objetivo es mucho más difícil que lograrlo». También enumera claramente cuatro componentes tecnológicos clave para la próxima actualización de Ethereum:

Firmas resistentes a la cuántica: ya hay trabajo de verificación formal para variantes de firmas SPHINCS

Sistema de pruebas STARK: el proyecto Arklib se dedica a crear implementaciones STARK con verificación completamente formal

Algoritmo de consenso tolerante a fallos bizantinos: actualmente se trabaja en definir y demostrar formalmente propiedades de seguridad del consenso de Lean

ZK-EVM: el proyecto evm-asm tiene como objetivo construir una implementación EVM completa con verificación formal (escribiendo directamente en ensamblador RISC-V)

Vitalik cita a Yōichi Hirai, y denomina a este enfoque como «la forma final del desarrollo de software».

Dirección de evolución de la arquitectura de “núcleo de seguridad” descrita por Vitalik

Según la confirmación del artículo de Vitalik, describe el patrón de evolución futura de la arquitectura de software:

Núcleo de seguridad: se refuerza de manera continua mediante métodos formales, asumiendo la máxima confianza; Vitalik expresa claramente que Ethereum, el núcleo de los sistemas operativos y las aplicaciones relacionadas con IoT (Internet de las Cosas) se convertirán en el núcleo de seguridad.

Borde no seguro: los componentes del borde se ejecutan en un entorno sandbox, con los permisos mínimos necesarios para completar el trabajo; si fallan los componentes del borde, el núcleo de seguridad ofrece protección.

Limitaciones de la verificación formal y modos de fallo

Vitalik admite que la verificación formal no es una panacea. Citando el trabajo de investigadores como Nadim Kobeissi (Cryspen), confirma tres modos principales de fallo: omisiones de verificación (solo se verifica parte del código, y las porciones no verificadas contienen fallas críticas); lagunas en la especificación (la propia especificación de seguridad es incorrecta o la demostración incluye supuestos erróneos); ataques de canal lateral (los ataques por canales laterales en la frontera entre software y hardware son difíciles de capturar con los modelos existentes).

Vitalik enfatiza que «la corrección demostrable» en esencia verifica la coherencia interna entre diferentes intenciones expresadas, no una correspondencia absoluta con las verdaderas intenciones humanas.

Herramientas de verificación formal asistida por IA

Según la confirmación del artículo de Vitalik sobre herramientas disponibles: Lean (lenguaje de demostración matemática, que verifica automáticamente teoremas); Claude y Deepseek 4 Pro (Vitalik confirma que son suficientes para escribir demostraciones de Lean); Leanstral (modelo de código abierto de 1190 mil millones de parámetros, con pesos ajustados específicamente para escribir en Lean; puede ejecutarse localmente y su rendimiento en benchmarks es superior al de muchos modelos generales con escalas aún mayores).

Preguntas frecuentes

¿Por qué Vitalik cree que Ethereum debería convertirse en un “núcleo de seguridad”?

Según el artículo de Vitalik, Ethereum es similar al núcleo de un sistema operativo: soporta el más alto nivel de confianza en el proceso de digitalización de la sociedad. Indica que el objetivo de diseño del núcleo de seguridad es lograr un nivel de seguridad que impida que el código con vulnerabilidades se vuelva algo descontrolado, y que toda la capacidad de cómputo adicional aportada por la IA se destine a mejorar la seguridad del núcleo de seguridad.

¿Por qué la verificación formal es especialmente adecuada para tecnologías como STARK, ZK-EVM, etc.?

Según el análisis de Vitalik, estas tecnologías comparten una característica: «el objetivo es mucho más difícil que implementarlo». Sus propiedades de seguridad pueden definirse con claridad mediante un lenguaje matemático, pero la implementación concreta es extremadamente compleja; justo ahí es donde la verificación formal puede desempeñar su papel con mayor eficacia.

¿Cómo recomienda Vitalik que los desarrolladores usen en la práctica la verificación formal asistida por IA?

Según el artículo de Vitalik, recomienda que la IA escriba código de Lean y demostraciones matemáticas, y que el usuario solo necesite verificar que las sentencias demostradas coinciden con lo esperado, sin tener que redactar por su cuenta el engorroso código de demostración de bajo nivel. Confirma que Claude, Deepseek 4 Pro y Leanstral son las principales herramientas disponibles actualmente.