Vitalik Buterin de Ethereum explica cómo la IA podría hacer los Smart Contracts verdaderamente seguros

La publicación Vitalik Buterin de Ethereum explica cómo la IA podría hacer que los Smart Contracts sean verdaderamente seguros apareció primero en Coinpedia Fintech News

El cofundador de Ethereum, Vitalik Buterin, ha publicado un argumento detallado en el que sostiene que la verificación formal asistida por IA podría cambiar fundamentalmente la forma en que se construye el software seguro, contradiciendo el creciente pesimismo en la comunidad de ciberseguridad sobre si los sistemas sin confianza pueden sobrevivir a ataques cada vez más potentes impulsados por IA.

"Mucha gente ha afirmado que con la búsqueda de errores asistida por IA, el código seguro será imposible", escribió Buterin. "Tengo una visión mucho más optimista, y la verificación formal asistida por IA es una parte importante de la razón."

Qué es realmente la verificación formal

La verificación formal es la práctica de escribir pruebas matemáticas sobre el código que pueden ser comprobadas automáticamente por un ordenador. En lugar de probar el software y esperar que no aparezcan errores, los desarrolladores escriben pruebas que garantizan matemáticamente que un fragmento de código se comporta exactamente como se pretende bajo todas las condiciones.

La tecnología existe desde hace décadas, pero se mantuvo como nicho porque escribir estas pruebas a mano es extremadamente difícil y lleva mucho tiempo. El argumento de Buterin es que la IA cambia esta ecuación de forma drástica. La IA puede escribir tanto el código como las pruebas, mientras que los humanos simplemente verifican que las declaraciones que se demuestran coinciden con lo que realmente quieren que haga el software.

Describió esta combinación como lo que el investigador Yoichi Hirai denomina "la forma final del desarrollo de software".

Por qué es importante para Ethereum

Buterin señaló varias áreas donde la verificación formal ya se está aplicando dentro del ecosistema de desarrollo de Ethereum. Entre ellas se incluyen las firmas resistentes a la computación cuántica, los sistemas de prueba STARK, los algoritmos de consenso y los ZK-EVM, todas áreas donde las propiedades de seguridad son simples de definir aunque el código subyacente sea extraordinariamente complejo.

Proyectos como Arklib están trabajando hacia una implementación STARK completamente verificada de manera formal. El proyecto evm-asm está construyendo una EVM completa escrita directamente en ensamblador RISC-V, verificada matemáticamente frente a una implementación de referencia legible por humanos. Los protocolos de consenso tolerantes a fallos bizantinos también están siendo formalmente especificados y verificados en Lean.

La idea principal es que para estos sistemas la brecha entre lo que el código hace y lo que se supone que debe hacer puede cerrarse con certeza matemática en lugar de con pruebas probabilísticas.

Los límites que reconoce

Buterin tuvo cuidado de no exagerar el caso. La verificación formal tiene modos de fallo reales. Las pruebas pueden escribirse sobre solo una parte de un sistema mientras que los errores críticos se ocultan en secciones no verificadas. Los desarrolladores pueden olvidar especificar propiedades importantes. La especificación formal en sí puede ser incorrecta. Las vulnerabilidades de hardware, como los ataques de canal lateral, pueden eludir incluso el software matemáticamente correcto.

"La corrección demostrable no prueba que el software sea correcto en la forma en que la mayoría de los seres humanos entienden la corrección", escribió. Lo que realmente hace la verificación formal es permitir a los desarrolladores expresar sus intenciones de múltiples formas redundantes diferentes y comprobar automáticamente que todas esas expresiones son compatibles entre sí.

La visión más amplia

Buterin describió un futuro optimista en el que el software se divide en dos capas. Una capa perimetral insegura maneja funciones de menor riesgo, se ejecuta en entornos aislados y opera con permisos mínimos. Un núcleo seguro maneja todo lo crítico, incluido el propio Ethereum, los kernels del sistema operativo y la infraestructura IoT sensible.

El núcleo seguro se mantiene deliberadamente pequeño y se somete a una verificación formal exhaustiva. La IA aporta la potencia computacional para hacer que la verificación sea práctica a escala. El resultado no es software sin errores, sino software donde los componentes más críticos pueden ser confiables con certeza matemática en lugar de esperanza.

"Los defensores finalmente tienen la oportunidad de ganar, de manera decisiva", concluyó, citando la propia experiencia de Mozilla al fortalecer su base de código frente a herramientas de ataque asistidas por IA.