以太坊：围绕Lean验证的点对点网络开发周启动

仍处于建设阶段的网络工作

Invisible Garden宣布，Machine-Checked Devcon Week于2026年11月2日至7日在线举行，围绕leanp2p开展工作。该项目使用Lean 4构建面向以太坊共识等用途的通信组件。这是开发活动，不是以太坊网络新版本上线。

仓库仍将主要实现描述为启动建设阶段。文档称，包结构、导入检查和测试基础设施已就位，代码将逐步加入。另一个分支保留参考原型。这种安排区分了已能工作的实验与正在重写的最终库。因此，不能把架构目标描述成已完整交付给用户的功能。

证明具体性质，而非绝对安全

方案将协议逻辑核心与系统操作分开。核心接收状态和事件，再产生新状态及预期动作。网络读取、时钟和随机值都作为明确输入传入。这便于重放场景：测试可重复相同事件，不依赖外部连接或无法精确复现的某一时刻。

目标性质相当具体。文档举例包括接收窗口永不为负、流编号遵循规则，以及已退役标识符不能再次使用。证明针对这些机制及其模型，并不代表整个程序、依赖组件与宿主系统都不会受到攻击。其意义在于让部分保证能够被检查和验证，而不是笼统宣称软件很稳健。

证明还须配合互操作测试

架构安排了互补检查：纯函数定理、来自其他实现的参考数据、生成多样输入的测试，以及已记录网络交互的重放。与go-libp2p比较，旨在确认另一套软件仍能理解所生成的消息。项目还计划测试沉默对端或读取缓慢的场景。数学性质与实际兼容通信回答不同问题，因此两类检查都予以保留。

首要目标是以太坊共识层，使用TCP通信、Noise协议和yamux多路复用。架构还优先安排请求与响应，以及gossipsub消息传播。其他功能仍被推迟，限制了拟议首个版本的范围。因此，这周工作的重点是产出可核验组件并逐步整合。活动开始既不证明整套网络栈已经完成，也不证明以太坊客户端已经采用它。