A two-weekend fun project: Vermilion, an experimental Lean 4 backend for the Verus verifier for Rust. Verification conditions are readable Lean theorems, provable with an SMT solver, Lean’s grind, Mathlib lemmas, by hand, or by your favourite AI system.