2026-11-05 –, Lotus Stage 2
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!
evm-asm is an experiment to see if we can use LLMs + formal verification to write the EVM directly in Risc-V assembly. Why, you ask?
1. it removes a compiler (and compiler bugs) from our trust base,
2. because everything is formally proved, we can hand-optimize at the assembly level to get the fastest EVM implementation ever written, and
3. showcases the power of AI in modern software development
Come to the talk to find out more!
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.