Foresight News reports that, according to a post on the Ethresearch forum, the research teams from the Ethereum Protocol Fellowship (EPF) and Invisible Garden have announced the latest progress on the Etheorem project. The project aims to build a fully executable Ethereum consensus specification using the theorem-proving language Lean 4, replacing traditional code testing with rigorous mathematical formal verification. This is intended to identify logical vulnerabilities at their root and prevent chain-splitting incidents caused by discrepancies in how multiple clients interpret the specification. Currently, the specification has passed all test vectors for three planned future hard-fork versions: Fulu, Gloas (including the ePBS mechanism), and Heze, covering core areas such as state transitions and fork choice. All logic is independently mathematically verified by the Lean kernel. It is now working to establish an underlying verification framework to set high security standards for Ethereum’s increasingly complex future upgrades.