Jaune is an independent executable specification of Ethereum's execution layer in Lean 4 — one artifact that passes the complete supported current-mainnet corpus (34,005 cases) and supports machine-checked proofs. Stories from building it: a merged EELS correction, transition-tool divergences filed upstream, and what a runnable, provable second spec is for.