We present Velvet—a Dafny-style verifier for imperative programs embedded into Lean proof assistant. Like Dafny, Velvet supports reasoning about effectful programs featuring mutable state, loops, and non-determinism. Unlike Dafny, Velvet seamlessly combines automated SMT-based proofs with interactive proof mode of Lean proof assistant, to which it is embedded, thus, allowing for multi-modal proofs. By virtue of being implemented as a Lean library, Velvet enjoys interaction with the rest of Lean ecosystem, in particular, its rich library of mathematical theories. In this presentation, we will give a tour of Velvet’s main features and outline the techniques underlying its embedding into Lean.