Ethereum: comienza una semana de trabajo sobre redes entre pares verificadas con Lean

Un trabajo de red todavía en construcción

Invisible Garden anuncia Machine-Checked Devcon Week en línea del 2 al 7 de noviembre de 2026. El trabajo gira alrededor de leanp2p, un proyecto en Lean 4 para componentes de comunicación destinados especialmente al consenso Ethereum. Es una actividad de desarrollo, no el lanzamiento de una nueva versión de Ethereum.

El repositorio todavía describe su implementación principal como una fase inicial. Indica que ya existen el árbol de paquetes, las comprobaciones de importaciones y la infraestructura de pruebas, mientras el código debe incorporarse progresivamente. Otra rama contiene un prototipo de referencia. Esta organización distingue un experimento funcional de la biblioteca final que se está reescribiendo. Los objetivos arquitectónicos no deben presentarse como funciones íntegramente entregadas a los usuarios.

Propiedades concretas frente a seguridad absoluta

El diseño separa el núcleo lógico de un protocolo de las operaciones realizadas con el sistema. El primero recibe un estado y un evento y produce un estado nuevo y las acciones esperadas. Las lecturas de red, el reloj y los valores aleatorios llegan como entradas explícitas. Esto facilita reproducir escenarios: una prueba puede repetir los mismos eventos sin depender de una conexión exterior ni de un instante imposible de reproducir exactamente.

Las propiedades buscadas son concretas. El documento cita una ventana de recepción que nunca sea negativa, el respeto de las reglas de numeración de flujos y la prohibición de reutilizar un identificador retirado. Las demostraciones se refieren a esos mecanismos y sus modelos. No significan que todo el programa, sus dependencias y el sistema anfitrión sean invulnerables. Se busca hacer comprobables garantías específicas, con un alcance más preciso que una afirmación general de robustez.

Las demostraciones complementan la interoperabilidad

La arquitectura prevé controles complementarios: teoremas sobre funciones puras, datos de referencia de otras implementaciones, pruebas con entradas variadas y repetición de intercambios de red registrados. Las comparaciones con go-libp2p deben comprobar que otra pila de software entiende los mensajes producidos. También se prevén ensayos con pares silenciosos o lectores lentos. Una propiedad matemática y una comunicación compatible responden a preguntas distintas; el programa de verificación conserva ambas.

La primera meta anunciada es la capa de consenso Ethereum, con comunicaciones TCP, el protocolo Noise y multiplexación yamux. La arquitectura también prioriza intercambios de petición y respuesta y difusión mediante gossipsub. Otras funciones se aplazan, limitando el alcance de la primera versión prevista. La semana busca producir elementos comprobables e integrarlos progresivamente. El comienzo del taller no demuestra que la pila esté terminada ni que los clientes Ethereum la hayan adoptado.