Un equipo de investigación de Ethereum Protocol Fellowship e Invisible Garden ha anunciado nuevos avances en el proyecto Etheorem, según una publicación en el foro de Ethresearch. De acuerdo con Foresight News, el proyecto tiene como objetivo construir una especificación completa y ejecutable del consenso de Ethereum en Lean 4, utilizando verificación matemática formal en lugar de pruebas tradicionales de código para reducir fallos de lógica y prevenir divisiones de la cadena causadas por diferencias de implementación.

La especificación ha superado todos los vectores de prueba para tres versiones futuras de bifurcaciones duras, Fulu, Gloas, incluidas el mecanismo ePBS, y Heze, cubriendo áreas fundamentales como las transiciones de estado y la elección de la bifurcación. Toda la lógica está verificada de forma independiente por el kernel de Lean, y el proyecto pretende proporcionar un marco de verificación de alta seguridad para las futuras actualizaciones del protocolo de Ethereum.