hath995/DafnyGithub-Dataset

Dafny GitHub Dataset

A corpus of publicly available Dafny (.dfy) source code crawled from GitHub, packaged as JSONL for model training and analysis. Dafny is a verification-aware programming language with built-in specification constructs (pre/postconditions, invariants, assert/assume) checked by an SMT solver.

• —106,404 unique-by-content .dfy files
• —966 source repositories (of 1,018 discovered; forks excluded)
• —753 MB of source (stored as ~44 MB of zstd Parquet), median 5 files per repo
• —Crawled 2026-07-22

Dataset structure

One JSON object per line:

from datasets import load_dataset
ds = load_dataset("hath995/DafnyGithub-Dataset", split="train")
print(ds[0]["repo"], ds[0]["path"])
print(ds[0]["content"])

How it was built

1. 1.Discovery — union of two GitHub channels: repo search language:Dafny (747 repos) and code search extension:dfy sliced by file size to beat the 1,000-result cap (surfacing .dfy files in otherwise non-Dafny repos). Forks are excluded (GitHub search excludes them by default).
2. 2.Extraction — each repo shallow-cloned with a blobless partial + sparse checkout of *.dfy only (so a 2 GB repo pulls just its Dafny files). Repos that fail to check out on Windows (invalid paths, sparse-checkout edge cases) were recovered via the GitHub trees + raw-blob API.
3. 3.Deduplication — files are deduplicated by exact content (sha256); ~117k exact duplicates were dropped during the crawl. Near-duplicates are not collapsed.

Considerations for using the data

Licensing

All files are included regardless of license; the license field records each repo's SPDX id so you can filter per your needs. A `null` or `NOASSERTION` value does not grant redistribution or training rights — filter accordingly before releasing or training.

Files by license: null/NONE 47,205 · NOASSERTION 33,730 · MIT 20,552 · Apache-2.0 3,880 · GPL-3.0 725 · BSD-2-Clause 94 · AGPL-3.0 73 · GPL-2.0 61 · BSD-3-Clause 33 · CC0-1.0 22 · BSL-1.0 12 · Unlicense 11 · CC-BY-4.0 4 · ISC 2. (NOASSERTION = a LICENSE file GitHub could not map to an SPDX id.)

Synthetic / benchmark corpora dominate the tail

A handful of repos are auto-generated verification benchmarks or LLM / mutation study data. They account for a large share of files, and because each differs by only a token or two, exact-content dedup does not collapse them:

For human-authored Dafny, filter these out:

DROP = {
    "VeriFixer/DSpec2Test", "VeriFixer/DafnyFaultLoc",
    "ValentinaWu1112/Automated-Program-Repair-of-Arithmetic-Programs-in-Dafny-using-Large-Language-Models",
    "Beneficial-AI-Foundation/vericoding-benchmark", "MutDafny/mutdafny-study-data",
}
ds_human = ds.filter(lambda r: r["repo"] not in DROP)

Limitations

• —Snapshot of default branches at crawl time; no history, branches, or PRs.
• —mutdafny-study-data is partial (GitHub truncated its recursive tree).
• —Files larger than 2 MB were skipped.
• —Coverage reflects GitHub's code-search index, which does not include every repo exhaustively.

Provenance

Reproducible via the crawler scripts (discover_repos.py, fetch_files.py, retry_api.py). Content belongs to the original repository authors under their respective licenses.