Derek Sorensen
Derek is a research engineer at the Ethereum Foundation focused on formal verification in Lean. He builds and maintains cryptography specifications, formally verifies Rust code, and has been working on formally verified production code for the ecosystem written directly in Lean.
Sessions
Devcon 8 Opening Ceremony, where we'll set the stage for an incredible event ahead! Join us as we kick off four days of talks, workshops, and community gatherings in Mumbai. This session sets the scene for the days ahead introducing the host city, the venue, and everything the event has to offer.
evm-asm is an experiment to see if we can use LLMs + formal verification to write the EVM directly in Risc-V assembly. I will share what we've done, what we've learned, and how this will help us secure Ethereum in protocol upgrades to come!
Formal verification is exploding in accessibility and relevance, and is securing more critical code than ever due in part to advancements in LLM-assisted proofs. At this workshop on formal verification in Lean, expect to learn: what guarantees you can (and cannot) expect from formal verification, what a formally verified codebase looks like, and hands-on, practical experience to start formally verifying code in Lean today.