dafny

{
  "aliases": [],
  "alternatives": [],
  "build_dependencies": [
    "gradle@8",
    "openjdk"
  ],
  "categories": [],
  "caveats": null,
  "conflicts_with": [],
  "dependencies": [
    "dotnet@8",
    "z3"
  ],
  "deprecated": 0,
  "deprecation_reason": null,
  "desc": "Verification-aware programming language",
  "disable_reason": null,
  "disabled": 0,
  "enrichment_fetched_at": "2026-06-20T23:36:48+00:00",
  "first_seen": "2026-06-20T23:34:18+00:00",
  "full_name": "dafny",
  "github_default_branch": "master",
  "github_last_commit_at": "2026-06-15T23:26:22Z",
  "github_readme_excerpt": "# Dafny\n\n[![Build and Test](https://github.com/dafny-lang/dafny/workflows/Build%20and%20Test/badge.svg)](https://github.com/dafny-lang/dafny/actions?query=workflow%3A%22Build+and+Test%22) [![Gitter](https://badges.gitter.im/dafny-lang/community.svg)](https://gitter.im/dafny-lang/community?utm_source=badge\u0026utm_medium=badge\u0026utm_campaign=pr-badge)\n\nDafny is a **verification-ready programming language**. As you type in your program, Dafny\u0027s verifier constantly looks over your shoulder, flags any errors, shows you counterexamples, and congratulates you when your code matches your specifications. When you\u0027re done, Dafny can **compile your code to C#, Go, Python, Java, or JavaScript** (more to come!), so it can integrate with your existing workflow.\n\n![vs-code-dafny-2 0 0-demo](https://user-images.githubusercontent.com/3601079/140799975-f3ac0925-10d9-4c14-b1a9-cd449854c6ae.gif)\n\nDafny 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.\n\nDafny has support for common programming concepts such as [classes and trait inheritance](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-class-types), [inductive datatypes](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#181-inductive-datatypes) that can have methods and are suitable for pattern matching, [lazily unbounded datatypes](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#182-co-inductive-datatypes), [subset types e.g. for bounded integers](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-subset-types), [lambdas](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-lambda-expressions), and [immutable and mutable data structures](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-collection-types).\n\nDafny also offers an extens",
  "github_repo": "dafny-lang/dafny",
  "github_stars": 3436,
  "github_topics": [
    "programming-language",
    "verification"
  ],
  "homepage": "https://github.com/dafny-lang/dafny/blob/master/README.md",
  "homepage_og_description": null,
  "homepage_og_image": null,
  "homepage_title": null,
  "installs_30d": 40,
  "installs_365d": 506,
  "installs_90d": 131,
  "keg_only": 0,
  "keg_only_reason": null,
  "last_seen": "2026-06-20T23:34:18+00:00",
  "license": "MIT",
  "llm_generated_at": null,
  "llm_model": null,
  "name": "dafny",
  "oldnames": [],
  "one_liner": null,
  "optional_dependencies": [],
  "rank_30d": 5175,
  "rank_365d": 5090,
  "rank_90d": 4989,
  "raw_hash": "b38dd04114777676",
  "recommended_dependencies": [],
  "revision": 0,
  "ruby_source_path": "Formula/d/dafny.rb",
  "tap": "homebrew/core",
  "test_dependencies": [
    "openjdk"
  ],
  "uses_from_macos": [],
  "version_head": null,
  "version_stable": "4.11.0",
  "versioned_formulae": [],
  "why_use_this": null
}