Specifications for cryptography in Ethereum, written in Lean.

• EthCryptographySpecs/Bls/, BLS12-381 curve arithmetic, hash-to-curve, and signatures.
• EthCryptographySpecs/Kzg/, KZG polynomial commitments.

• elan, for lean and lake.

lake build

python3 -m venv .venv
source .venv/bin/activate
pip install -e '.[test]'
pytest

Note: Pre-generated reference tests are written to tests/ at the project root. These tests are intended for use across implementations and may be pinned by downstream consumers.