Tag: formal-verification¶

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.