Skip to content

EPF Week 1 - Ivan Anishchuk - Rust to Lean, first proofs

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.

The engine that does the Rust→Lean step is Charon+Aeneas. I got it set up with the stable Lean release (v4.29.1, after fighting some typical dependency hell a little) and spent the week playing with the stack, extracting Rust code and proving what came out.

On moonglass (experimental CL client) I worked up a handful of small slices. Cheapest first, and not even a proof: I fed moonglass's gloas test fixtures through etheorem's SSZ runner with no transpiler at all, just to see whether two independent implementations agree on the hashes, and they did, 5 out of 5 on what I tried. Then the extracted-and-proved slices, each one machine-checked and sorry-free (the Lean kernel actually checks them, no holes): the integer primitives, the u64 SSZ round-trip (Rust SSZ library encoder coming out byte-for-byte equal to etheorem's), the balance and slashing arithmetic, the attester-slashing latch, and LMD-GHOST head pick.

On leanVM (zkVM from the lean-Ethereum effort, its arithmetic running over a small prime field called KoalaBear) I was mostly exercising the tooling on something other than consensus. I got its arithmetic core to extract and proved it matches MeanVM (my partial, tool-generated model of leanVM), at least for add, subtract and multiply: those I grounded fully against the extracted low-level arithmetic, no field axiom assumed. The inverse I left on one clearly-labeled assumption, rather than pretend it comes for free.

What I learned... The low-level field arithmetic extracts transparently and proves with no trust assumptions at all, which is honestly great; the higher-level wiring (Rust traits) is where the extractor still kinda struggles. So the move is to prove at the level I can actually back up, instead of forcing the whole thing. The differential cross-check was the cheapest piece and maybe the highest-value, which surprised me a bit (no extraction needed, and it'd flag any divergence between the two).

Caveats/blockers. I hit two toolchain limitations on the full leanVM extraction that I'm holding as candidate/unconfirmed for now, could be real bugs, could be me holding it wrong tbh, I need to properly sit down and review before I know next steps. And a couple of the slices currently lean on a small faithful stand-in for a private upstream function, so those want a drift-check against source before I'd trust them long-term.

Next is grinding down that inverse assumption, chasing those two questions upstream, and probably checking in with the projects' devs for pointers. Exploration goes on, stay tuned.

Resources