2026-11-05 –, Workshop 2
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.
This workshop will introduce software developers who are curious about formal verification to practical examples and tutorials on formal verification in Lean. It will include a short introductory lecture, followed by hands-on practical examples. Attendees can clone the lecture repo and follow along with the examples on their own machines.
Agenda:
1. What is formal verification, and what does it (not) guarantee? (5 minutes)
2. Proofs in Lean (10 minutes)
3. Formally verifying Rust (and other) code in Lean, practical examples (35 minutes)
4. Q&A (10 minutes)
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.