EthLib

Formally verified Ethereum primitives, written in Lean. EthLib is intended to be the shared home for Ethereum definitions and proofs, so that Lean projects can build on a common implementation instead of each maintaining its own. Some of these primitives can also be used by Ethereum clients via bindings. Clients may use the bindings temporarily until a native implementation exists, or permanently if the performance of this library is sufficient.

Architecture

EthLib is organised in layers, from the bytes and integers every specification uses up to the two layers of the protocol. A module imports only from its own layer or from those below it, and the execution and consensus layers never import each other.

ARCHITECTURE.md gives the scope, the rules behind each layer, the types that modules share and how forks are written.

Where things live