Updates¶
Biweekly dev updates from the Ethereum Protocol Fellowship, cohort seven.
This section is a dated, linkable log of the fellowship work, with a post every two weeks.
Subscribe to the RSS feed to follow new updates in your reader.
Browse: Tags · Categories · Archive
EPF Week 6 - Ivan Anishchuk - the merkle-branch completeness proof goes upstream¶
2026-08-03
Categories: weekly-update
Tags: epf, lean4, formal-verification, merkleization
Short version:
EPF Week 5 - Ivan Anishchuk - a joint proposal with Raj and the verification roadmap upstream¶
2026-07-27
Categories: weekly-update
Tags: epf, lean4, formal-verification
Short version:
EPF Week 2 - Ivan Anishchuk - expanding etheorem with Heze/FOCIL and cross-client conformance harness experimentation¶
2026-07-03
Categories: weekly-update
Tags: epf, lean4, formal-verification
Week 2 I shifted off the Charon+Aeneas extraction experiments and onto etheorem's conformance layer, the Lean 4 spec-container models that get checked against the official test vectors. That work landed:
EPF Week 1 - Ivan Anishchuk - Rust to Lean, first proofs¶
2026-06-22
Categories: weekly-update
Tags: epf, lean4, formal-verification
Week 1, still scoping. I leaned harder into the formal-verification side, and most of the time went into one question: can you take Rust code, generate Lean 4 out of it automatically, and then prove the generated Lean matches a reference model (or, where there isn't one, just holds the property I'm after)? None of this is worth submitting anywhere yet, it's all still exploration, but it's holding together so far.
EPF Week 0 - Ivan Anishchuk - Getting Started¶
2026-06-17
Categories: weekly-update
Tags: epf, lean4, ancient history
I'm Ivan (@IvanAnishchuk), a backend engineer by trade, about fifteen years of it, mostly Python, mostly in web2 and some early AI before it was cool, the last few in applied cryptography and ZK. The one constant under all of it is math: I did discrete math and probability at university (although never graduated, I'm actually also currently catching up on academic things in parallel) and my first actual research was in abstract algebra (finite function algebras, k-valued logic, the sort of thing nobody asks you about at parties). That's probably most of why formal methods keep pulling me back. I came into cohort 7 drawn to the consensus layer but without a project picked, so Week 0 was mostly scoping.