https://github.com/dafny-lang/dafny Skip to content Navigation Menu Toggle navigation Sign in * Product + Actions Automate any workflow + Packages Host and manage packages + Security Find and fix vulnerabilities + Codespaces Instant dev environments + Copilot Write better code with AI + Code review Manage code changes + Issues Plan and track work + Discussions Collaborate outside of code Explore + All features + Documentation + GitHub Skills + Blog * Solutions For + Enterprise + Teams + Startups + Education By Solution + CI/CD & Automation + DevOps + DevSecOps Resources + Learning Pathways + White papers, Ebooks, Webinars + Customer Stories + Partners * Open Source + GitHub Sponsors Fund open source developers + The ReadME Project GitHub community articles Repositories + Topics + Trending + Collections * Pricing Search or jump to... Search code, repositories, users, issues, pull requests... Search [ ] Clear Search syntax tips Provide feedback We read every piece of feedback, and take your input very seriously. [ ] [ ] Include my email address so I can be contacted Cancel Submit feedback Saved searches Use saved searches to filter your results more quickly Name [ ] Query [ ] To see all available qualifiers, see our documentation. Cancel Create saved search Sign in Sign up You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert {{ message }} dafny-lang / dafny Public * Notifications * Fork 249 * Star 2.7k * Dafny is a verification-aware programming language dafny.org License View license 2.7k stars 249 forks Branches Tags Activity Star Notifications * Code * Issues 1k * Pull requests 132 * Discussions * Actions * Projects 0 * Wiki * Security * Insights Additional navigation options * Code * Issues * Pull requests * Discussions * Actions * Projects * Wiki * Security * Insights dafny-lang/dafny This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository. master BranchesTags Go to file Code Folders and files Last commit Last Name Name message commit date Latest commit History 6,468 Commits .github .github Binaries Binaries Scripts Scripts Source Source docs docs .editorconfig .editorconfig .gitattributes .gitattributes .gitignore .gitignore .gitmodules .gitmodules .pre-commit-config.yaml .pre-commit-config.yaml CODE_OF_CONDUCT.md CODE_OF_CONDUCT.md CONTRIBUTING.md CONTRIBUTING.md DAFNY.ORG.txt DAFNY.ORG.txt INSTALL.md INSTALL.md LICENSE.txt LICENSE.txt Makefile Makefile NOTICES.txt NOTICES.txt README.md README.md RELEASE_NOTES.md RELEASE_NOTES.md SECURITY.md SECURITY.md customBoogie.patch customBoogie.patch dotnet-tools.json dotnet-tools.json View all files Repository files navigation * README * Code of conduct * License * Security Dafny Build and Test Gitter Dafny is a verification-ready programming language. As you type in your program, Dafny's verifier constantly looks over your shoulder, flags any errors, shows you counterexamples, and congratulates you when your code matches your specifications. When you're done, Dafny can compile your code to C#, Go, Python, Java, or JavaScript (more to come!), so it can integrate with your existing workflow. vs-code-dafny-2 0 0-demo Dafny will give you assurance that your code meets the specifications you write, while letting you write both code and specifications in the Dafny programming language itself. Since verification is an integral part of development, it will thus reduce the risk of costly late-stage bugs that are typically missed by testing. Dafny has support for common programming concepts such as classes and trait inheritance, inductive datatypes that can have methods and are suitable for pattern matching, lazily unbounded datatypes, subset types e.g. for bounded integers, lambdas, and immutable and mutable data structures. Dafny also offers an extensive toolbox for mathematical proofs, such as unbounded and bounded quantifiers, calculational proofs, pre- and post-conditions, termination conditions, loop invariants, and read/ write specifications. Dafny This github site contains these materials: * sources * binary downloads for Windows, macOS, GNU/Linux, and FreeBSD * the issue tracker * the wiki, including frequently asked questions Documentation about the dafny language and tools is located here. A reference manual is available both online and as pdf. (A LaTeX version can be produced if needed.) Community You can ask questions about Dafny on Stack Overflow or participate in general discussion on Dafny's Gitter. Try Dafny The easiest way to try out Dafny is to install Dafny on your own machine in Visual Studio Code and follow along with the Dafny tutorial. You can also download and install the Dafny CLI if you prefer to work from the command line. Read more Here are some ways to get started with Dafny: * 4-part course on the Basics of specification and verification of code: + Lecture 0: Pre- and postconditions (19:08) + Lecture 1: Invariants (20:56) + Lecture 2: Binary search (21:14) + Lecture 3: Dutch National Flag algorithm (20:33) * New overview article: Accessible Software Verification with Dafny , IEEE Software, Nov/Dec 2017 * Online tutorial, focusing mostly on simple imperative programs * 3-page tutorial notes with examples (ICSE 2013) * Dafny Quick Reference * Language reference for the Dafny type system, which also describes available expressions for each type * Cheatsheet: basic Dafny syntax on two pages * Dafny Reference Manual [html] [pdf] * Dafny libraries, a standard library of useful Dafny functions and lemmas * Dafny Power User * Videos at Verification Corner * Blog The language itself draws pieces of influence from: * Euclid (from the mindset of a designing a language whose programs are to be verified), * Eiffel (like the built-in contract features), * CLU (like its iterators, and inspiration for the out-parameter syntax), * Java, C#, and Scala (like the classes and traits, and syntax for functions), * ML (like the module system, and its functions and inductive datatypes), and * Coq and VeriFast (like the ability to include co-inductive datatypes and being able to write inductive and co-inductive proofs). External contributions * Haskell-to-Dafny translator, by Duncan White * Vim-loves-Dafny mode for vim, by Michael Lowell Roberts * Boogie-Friends Emacs mode Contributors Information and instructions for potential contributors are provided here. License Dafny itself is licensed under the MIT license. (See LICENSE.txt in the root directory for details.) The subdirectory Source/Dafny/Coco contains third party material; see Source/Dafny/Coco/LICENSE.txt for more details. About Dafny is a verification-aware programming language dafny.org Topics programming-language verification Resources Readme License View license Code of conduct Code of conduct Security policy Security policy Activity Custom properties Stars 2.7k stars Watchers 80 watching Forks 249 forks Report repository Releases 45 Dafny 4.6.0 Latest Mar 28, 2024 + 44 releases Packages 0 No packages published Contributors 89 * @RustanLeino * @keyboardDrummer * @davidcok * @MikaelMayer * @robin-aws * @cpitclaudel * @fabiomadge * @qunyanm * @wuestholz * @atomb * @lukemaurer * @danmatichuk * @alex-chew * @markusschaden + 75 contributors Languages * C# 60.4% * Dafny 31.4% * Java 2.1% * F# 1.5% * SMT 1.5% * Go 0.8% * Other 2.3% Footer (c) 2024 GitHub, Inc. Footer navigation * Terms * Privacy * Security * Status * Docs * Contact * Manage cookies * Do not share my personal information You can't perform that action at this time.