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.
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 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.
Run the test suite:
python3 -m venv .venv
source .venv/bin/activate
pip install -e '.[test]'
pytest