Our paper Velvet: A Foundational Multi-Modal Verifier for Imperative Programs in Lean has been accepted to CAV 2026!