For the past 18 months, we have been continuously developing Veil, an open-source framework for automated and interactive verification of transition systems, entirely embedded in the Lean proof assistant. Unlike traditional verifiers, which are implemented as standalone tools and (optionally) use proof assistants as backend certificate checkers, Veil is a Lean library, with all its functionality entirely embedded in the proof assistant. We believe this approach has significant advantages over traditional verifiers and that, in the near future, more verifiers will be built in this way. Nonetheless, Lean’s extraordinary meta-programming facilities—like all powerful tools—can prove to be both a blessing and a curse, and it is not at all difficult to create an unmaintainable mess. In this talk, we describe our vision for building verifiers in Lean, and share our experience of writing (and rewriting) Veil, and the lessons we have learned along the way.