Contributing Lean 4 proofs to Ethereum's consensus specification in etheorem, focused on Gloas, Heze, and cross-fork fork-choice verification.
In progress
Heze ePBS–FOCIL compositional proofs
Notes on formal verification work
Lean proofs contributed upstream