Vitalik: La verificación formal asistida por IA promete mejorar tanto la eficiencia como la seguridad del código.

Según Foresight News, Vitalik Buterin publicó un artículo en el que explora las perspectivas de la verificación formal en el ámbito de la seguridad blockchain. El texto señala que en el desarrollo avanzado de Ethereum está surgiendo un nuevo paradigma: escribir código directamente en EVM bytecode, ensamblador o Lean, y verificar su corrección mediante pruebas matemáticas comprobables automáticamente en Lean. El investigador Yoichi Hirai denomina a este paradigma la "forma final del desarrollo de software". Vitalik considera que la verificación formal asistida por IA podría mejorar la eficiencia y seguridad del código al mismo tiempo, siendo especialmente útil para módulos centrales de seguridad como STARK, ZK-EVM, firmas resistentes a la computación cuántica y algoritmos de consenso. El artículo también subraya que la verificación formal no es universal, ya que puede verse limitada por el alcance de las pruebas, especificaciones incorrectas o vulnerabilidades por canales laterales de hardware. En el futuro, el software podría dividirse entre "núcleos de seguridad" y "bordes no seguros", y Ethereum se convertiría en uno de los núcleos de seguridad más importantes.