Một nhóm nghiên cứu từ Ethereum Protocol Fellowship và Invisible Garden đã công bố những tiến triển mới cho dự án Etheorem, theo một bài đăng trên diễn đàn Ethresearch. Theo Foresight News, dự án hướng tới việc xây dựng một đặc tả đồng thuận Ethereum hoàn toàn có thể thực thi trong Lean 4, sử dụng xác minh toán học hình thức thay vì kiểm thử mã truyền thống để giảm thiểu các lỗi logic và ngăn chặn tình trạng tách chuỗi (chain splits) do khác biệt trong triển khai.

Đặc tả đã vượt qua tất cả các bộ kiểm thử (test vectors) cho ba phiên bản hard fork trong tương lai, Fulu, Gloas, bao gồm cơ chế ePBS, và Heze, bao phủ các khu vực cốt lõi như chuyển trạng thái và lựa chọn fork. Tất cả logic được xác minh độc lập bởi hạt nhân Lean (Lean kernel), và dự án nhằm cung cấp một khung xác minh có mức độ bảo mật cao cho các nâng cấp giao thức tương lai của Ethereum.