- Ethereum ha nombrado una tecnología que podría fortalecer la seguridad de los contratos inteligentes en la era de la IA.
- Según un desarrollador de Vyper, la verificación formal se está volviendo críticamente importante.
- Ayuda a encontrar errores que las pruebas no detectan.
El equipo de la red Ethereum publicó una serie de entradas invitadas del desarrollador principal de Vyper bajo el seudónimo big_tech_sux, centradas en el papel de la verificación formal en una era de rápido desarrollo de la IA.
0/ A medida que los sistemas de IA se vuelven más potentes, la verificación formal, que es la disciplina de usar matemáticas para demostrar que los programas informáticos son correctos, muestra cada vez más potencial.
— Ethereum (@ethereum) August 5, 2026
Un hilo invitado de @big_tech_sux, desarrollador principal de @vyperlangpic.twitter.com/3T6H76AVrL
El autor argumenta que el progreso en los LLM está haciendo que las pruebas matemáticas de la corrección de programas sean más accesibles, y para los contratos inteligentes que gestionan miles de millones de dólares, la verificación formal se está volviendo gradualmente una necesidad.
La IA cambia el enfoque de la verificación de software
La serie de publicaciones explica que la verificación formal es un método matemático que permite demostrar que un programa funciona correctamente en todos los escenarios de ejecución posibles, no solo en aquellos cubiertos por las pruebas.
Como ejemplo, el autor citó la función f(x) = x/2, para la cual se puede demostrar matemáticamente que el resultado nunca superará el valor de entrada.
Según él, esta metodología puede encontrar errores extremadamente raros que son prácticamente imposibles de detectar mediante pruebas convencionales.
“La verificación formal puede detectar 1 de cada 1 cuatrillón de casos límite que nunca surgirían durante las pruebas – y ese caso límite es el que puede provocar un fallo catastrófico”, señaló el autor.
Al mismo tiempo, reconoció que hasta hace poco, utilizar este enfoque requería grandes equipos de expertos que construían modelos matemáticos de programas y realizaban pruebas complejas.
Desde la perspectiva del desarrollador, los LLM modernos simplifican significativamente este proceso a medida que nos acercamos a la IAG.
Al mismo tiempo, el autor enfatizó que, incluso con IA, la verificación formal sigue siendo un proceso complejo y intensivo en recursos. En particular, convertir el código fuente en un modelo formal puede introducir inexactitudes que afectan la confiabilidad de los resultados.
El desarrollo de la IA cambia el equilibrio entre el ataque y la defensa
La pieza señala que el desarrollo de la inteligencia artificial aumenta simultáneamente la efectividad de defensores y atacantes.
El autor recordó un incidente en el que un modelo de OpenAI no lanzado pudo encontrar vulnerabilidades de día cero que permitieron eludir múltiples capas de protección.
En este contexto, la verificación formal, según el autor, permite desplazar la ventaja a favor de los defensores.
“Mientras que los atacantes solo necesitan encontrar una secuencia de entradas que les permita vulnerar (entrar en) un sistema, los defensores pueden usar verificación formal para probar la robustez contra todos los inputs,” enfatizó.
Por eso, para software crítico para la misión — incluyendo contratos inteligentes que gestionan miles de millones de dólares en fondos de usuarios — la verificación formal se está convirtiendo en "no una opción, sino un prerequisito necesario".
Es importante destacar que esto continúa una discusión previamente iniciada por el cofundador de Ethereum, Vitalik Buterin, sobre el uso de la IA para la verificación formal de código.
El mensaje Ethereum Explained How AI Changes Approach to Smart Contract Security apareció primero en INCRYPTED.