2026-11-04 –, Workshop 2
Formalization of consensus spec in Lean4 and proving protocol invariants and rules. I will go over six months of proving work during EPF and explain the tool-assisted proving pipeline used.
A novel approach to the spec, a single artifact that can we run, test, and prove. Contributions included completeness theorem for merkle branch check widely used in consensus (deposits, lightclient sync, and PeerDAS sampling), protocol arithmetic and invariants proofs, and various spec model improvements (including modeling Heze fork with FOCIL).
Experienced dev and veteran of the Ethereum community, EPF cohort 7 fellow aspiring to do meaningful protocol work.
I'm a blockchain researcher and developer focused on Ethereum protocol research, zero-knowledge proofs, and cryptographic systems. i enjoys exploring consensus-layer mechanisms, building secure and verifiable protocols, and contributing to open-source projects that advance Ethereum’s technology.