Skip to content

EPF Week 0 - Ivan Anishchuk - Getting Started

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.

A bit of background

No core-client work yet, I'll be honest. The closest thing I've built is ETH Consensus Neotrace, which started as a consensus-spec study at Invisible Garden and turned into a tool that generates cross-client test vectors by tracing the spec (the upstream spec PR out of it got closed unmerged, so I file it under "study" rather than "contribution"). Before being accepted to EPF I mostly dabbled in applied crypto: NoZKash, privacy eCash on the EVM with no zk-SNARKs (just BLS blind signatures over the EIP-2537 precompiles), plus some zkML research, a little bit of decentralized AI development and a few smaller things in other ecosystems.

What I did this week

Got oriented and scoped. I read wide first, the study-group tracks (Lean/zkEVM, cryptography, protocol fundamentals) and the kickoff, then went through the cohort project board and open issues from client teams to see what's actually being asked for, beyond what I happen to find interesting.

Surveyed the formal-verification work, since that's the part I keep coming back to. I mapped what already exists on the consensus layer: ConsenSys's Dafny effort (archived now), pieces from Runtime Verification, the etheorem project in Lean 4, and the EF consensus team's model-checking work (arXiv:2501.07958). etheorem is the one I went deepest on. It formalizes SSZ, Ethereum's serialization and Merkleization layer, and already proves the core encoding properties for the simpler cases, with the harder ones still open. I also kept half an eye on the recent lean-Ethereum interop devnets, where serialization bugs keep turning up (leanSpec #327, zeam #942).

Got hands-on with etheorem. On top of an overall review of the repo, I got it building on its pinned toolchain (Lean v4.29.1, Lake) and ran the conformance suite for a clean baseline, then did a tool-assisted audit I drove myself: 24 findings awaiting triage, 4 high-severity across three root causes (subgroup checks in the BLS code, deserializer offset validation, and an out-of-bounds path in the Merkle cache), plus a fork that's implemented but not yet wired into conformance. Enough to feel the shape of the codebase, and what actually picking it up would involve. Yeah, I did some catching up on Lean4 too in the weeks leading to this.

Areas, tools, and what's next

What I'm drawn to, and happy to be pointed at: formal verification and the consensus layer most of all, but plain implementation and tooling too. I work mostly in Python (my strongest) and Rust, with the applied-crypto and ZK background sitting underneath. Over the next couple of weeks I'll keep surveying (open issues, the project ideas the teams have posted, the formal-methods efforts, and what proposing my own would actually take, etheorem being the one I've gone deepest on), then commit to one. It might end up a proof-heavy project, a hands-on implementation task, plain bug-fixing, or my own proposal; I'd rather make that call with the survey done than guess at it now. Either way: small and concrete to start. We'll see.

Resources