Dafny is a verification-aware programming language that has native support for capturing specifications and is equipped with a static program verifier. By blending sophisticated automated reasoning with familiar programming idioms and tools, Dafny empowers you to write provably correct code w.r.t. its specifications. In addition to a verification engine to check implementations against specifications, the Dafny ecosystem includes several compilers (C#, Java, JavaScript, Go, Python) that help you integrate Dafny into your existing workflows. The Dafny ecosystem also supports you with a Visual Studio Code extension, powered by an LSP implementation, and a code formatter. Dafny is used in academia for teaching and research, as well as in industry, such as by teams at Amazon (e.g. AWS Encryption SDK).