Veil is a foundational verification framework embedded in the Lean 4 proof assistant that makes distributed protocol verification both powerful and accessible. In this hands-on tutorial, we will go step-by-step through the development, testing, and verification of a simple distributed protocol, introducing Veil’s features as we go along. Unlike existing tools such as TLA+ and Ivy, Veil provides a unified environment where automated push-button verification coexists with the full power of a modern proof assistant, all while maintaining foundational soundness guarantees. Participants will learn practical verification workflows including both concrete state and symbolic bounded model checking (BMC) for protocol validation, counterexample-guided invariant strengthening, and effective use of decidable logic fragments for automated proofs of safety. By the end of this tutorial, attendees will be equipped to verify their own distributed protocols using Veil and understand how a verifier fully embedded within a proof assistant opens new possibilities for formal methods. Whether you’re a researcher, practitioner, or student, this tutorial will give you hands-on experience with a cutting-edge verification technology.