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.
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.
| Layer | Module | What it specifies |
|---|---|---|
| Base | U256 |
the 256-bit word of the EVM, and its two's complement reading |
| Cryptography | Hash |
Keccak-256, SHA-256, RIPEMD-160, the BLAKE2b compression function, CRC-32C |
| Cryptography | Secp256k1 |
the secp256k1 curve, ECDSA, public key recovery, addresses |
| Cryptography | Bls |
BLS12-381 and BLS signatures |
| Cryptography | Kzg |
KZG commitments to blobs and cells |
| Cryptography | Xmss |
leanXMSS, a hash-based signature for a post-quantum consensus layer |
| Cryptography | Vrf |
the VRF tree, one verifiable random output per index |
| Serialization | Rlp |
Recursive Length Prefix, the encoding of the execution layer |
| Serialization | Ssz |
Simple Serialize and its merkleization, the encoding of the consensus layer |
| Networking | Encoding |
the protobuf varint of req/resp messages |
| Networking | Snappy |
Snappy block decompression |
| Networking | Gossip |
the gossip message ID of Phase 0 and Altair |
| Execution | Fees |
the EIP-1559 base fee and the blob base fee |
| Execution | Evm |
the arithmetic, comparison and bitwise instructions of the EVM |
| Execution | Precompiles |
ECRECOVER, RIPEMD-160, MODEXP and BLAKE2F |
The theorems about a module live under Proofs/ in its layer, and the C exports that the bindings call under Exports/.
SOUNDNESS.md says what the proofs establish, and what each use of EthLib trusts on top of them.
Read CONTRIBUTING.md first. It sets the terms under which you contribute, and points to the rules in AGENTS.md.
Install uv for repository Python checks. CI uses uv 0.13.6. The soundness checks select Python 3.12, which uv downloads if needed.
Install elan:
curl https://elan.lean-lang.org/elan-init.sh -sSf | shDownload Mathlib:
lake exe cache getCompile the primitives and check every proof:
lake buildBUILDING.md covers module boundaries, CI caching and build timing reports.
When you refresh the dependencies, use lake --keep-toolchain update, so that the toolchain stays the one Mathlib expects.
From the repository root, run the soundness checks used by CI:
uv run --no-project --python 3.12 python scripts/soundness_facts.py --check
uv run --no-project --python 3.12 python -m unittest scripts/test_soundness_facts.pyThese checks use only the standard library.
--no-project runs them without installing the native bindings.
Run the binding test suite:
uv sync --frozen --extra test
uv run --no-sync pytestRun uv sync --frozen --extra test again after changing Lean or C sources.
Sync rebuilds the native extension when its source or build inputs change.
uv run --no-sync tests that build.