At last we have Etheorem: complete executable Consensus Specs written in Lean4!! Etheorem started in May, now a team of 7 independent Engineers and Researchers has been working on this (@invisiblgarden and @ethereum Protocol Fellows). It passes all the official test vectors, for Fulu, Gloas and Heze (has not modeled light clients and gossip). It is based on a framework that abstracts from the spec writer most technical details, uses monadic state machines, allows inheritance between forks and makes adding proofs simpler, and spec code readable. Currently, Etheorem has only 8 spec functions fully characterized and 29 partially. The SSZ proofs are mostly complete. Etheorem invites the community to work on an open source effort to add more proofs. The base for this is already implemented. More information at: Repo: Discord: Team: @0x_flwr @IvanAnishchuk @0xRajGill @leolarav