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, Keccak-512, SHA-256, RIPEMD-160, the BLAKE2b compression function, CRC-32, CRC-32C, HMAC-SHA-256, HKDF, the Concatenation KDF |
| Cryptography | Secp256k1 |
the secp256k1 curve, ECDSA, public key recovery, addresses |
| Cryptography | Secp256r1 |
the secp256r1 curve, also called P-256, and ECDSA verification |
| Cryptography | AltBn128 |
the alt_bn128 curve of EIP-196 and EIP-197, also called BN254, and its pairing |
| Cryptography | Aes |
the AES block cipher for 128-bit and 256-bit keys, and the CTR and GCM modes |
| Cryptography | Ethash |
the proof of work before Paris: its sizes, seed, cache, dataset items and loop |
| Cryptography | Bls |
BLS12-381 and BLS signatures |
| Cryptography | Kzg |
KZG commitments to blobs and cells |
| Cryptography | Merkle |
the perfect binary Merkle tree that leanXMSS, leanSPHINCS, SSZ and the VRF share |
| Cryptography | Xmss |
leanXMSS, a hash-based signature for a post-quantum consensus layer |
| Cryptography | Sphincs |
leanSPHINCS, a stateless hash-based signature with FORS for 2^30 signatures |
| 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 | Enr |
Ethereum Node Records of EIP-778, their text form, the "v4" identity scheme, node IDs and the consensus entries |
| Networking | Snappy |
Snappy block decompression, a literal block encoder and the framing format |
| Networking | Gossip |
topic strings, the message ID, the size limits and gossipsub parameters, and the attestation subnets of a node |
| Networking | Discv5 |
the node distance, the "v4" handshake cryptography, the packets and the messages of discv5 |
| Networking | ReqResp |
the ssz_snappy encoding of requests and response chunks, with its size bounds |
| Networking | Discv4 |
the packets of discv4, with EIP-8 and EIP-868 |
| Networking | Rlpx |
the RLPx transport: its ECIES encryption, its handshake and its frames |
| Networking | Devp2p |
the Hello, Disconnect, Ping and Pong messages of the "p2p" capability |
| Execution | Fees |
the EIP-1559 base fee and the blob base fee |
| Execution | Evm |
the opcodes of each fork, the stack, frame and memory of the EVM, its stack and memory instructions, and the gas prices |
| Execution | Precompiles |
all 18 precompiles, from ECRECOVER to P256VERIFY, each run by address from the fork that adds it |
| Execution | State |
accounts, the state, the state and storage roots, and the writes of a block and a transaction with their rollback |
| Execution | Transactions |
the five kinds of transaction, their bytes and hashes, the sender at each fork, and the intrinsic gas and validity of one transaction |
| Execution | Blocks |
the header, withdrawals, logs, receipts and block of each fork, the logs bloom filter, the header hash, and before Paris the difficulty, the proof of work, the ommers, the rewards and the DAO Fork |
| Execution | Trie |
the root of the Merkle Patricia Trie, plain and secured, its Merkle proofs, and the hex-prefix encoding of its paths |
| Consensus | Consensus |
the configuration, presets and constants, slots and epochs, the fork of an epoch, signing domains, the swap-or-not shuffle and committees, containers with the execution payload, the custody of data columns, the gossip topics of each fork and the subnets of messages, the request and response messages, and models of Casper FFG and the LMD-GHOST fork choice |
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 rules and the terms under which you contribute.
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 pytest -n auto-n auto runs one test process per core.
Run 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.