Según un mensaje de Foresight News, a través de una publicación en el foro de Ethresearch, los equipos de investigación de Ethereum Protocol Fellowship (EPF) e Invisible Garden han dado a conocer los últimos avances del proyecto Etheorem. El objetivo de este proyecto es construir, mediante el lenguaje de demostración de teoremas Lean 4, un conjunto de especificaciones de consenso de Ethereum totalmente ejecutables. Para ello, se sustituye el enfoque tradicional de pruebas mediante código por una validación estricta y formal de carácter matemático, con el fin de identificar y eliminar fallos lógicos desde su raíz y evitar que implementaciones de múltiples clientes provoquen incidentes de bifurcación de cadena por discrepancias de interpretación. Actualmente, esta especificación ya ha superado todos los vectores de prueba correspondientes a tres versiones futuras de hard fork: Fulu, Gloas (incluye el mecanismo ePBS) y Heze, cubriendo elementos esenciales como la transición de estados y la selección de bifurcaciones. Toda la lógica se valida matemáticamente de manera independiente dentro del núcleo de Lean, y se está preparando para establecer un marco de verificación de alta seguridad en la capa base para las futuras y complejas actualizaciones de Ethereum.