SpecFault-Dafny

SpecFault-Dafny is a compact Dafny benchmark for verifier-passing specification faults. Each item pairs a stated intent with a Dafny candidate whose specification either matches the intent or verifies while missing it.

The release includes:

• a 45-item scored corpus under specfault-dafny/bench/items
• five baseline validators under specfault-dafny/src/specfault
• final scorecard artifacts under specfault-dafny/artifacts/results
• Markdown evidence cards under specfault-dafny/artifacts/cards
• the camera-ready hackathon report under submission

Quickstart

Prerequisites:

• Dafny 4.11.0 on PATH
• Python dependencies managed by uv

cd specfault-dafny
uv sync --extra dev
make smoke

make smoke runs the package-level sanity check without live LLM calls.

Reproduce The Submitted Scorecard

The submitted report uses prediction run 20260524T205027Z-llmfinal. The tracked prediction file is enough to regenerate the scorecard and audit tables:

cd specfault-dafny
uv run specfault score bench/items artifacts/results/predictions.jsonl \
  --out artifacts/results/scorecard.json \
  --markdown report/tables/scorecard.md
uv run specfault audit bench/items artifacts/results/predictions.jsonl \
  --out notes/corpus_audit.md
uv run python scripts/validate_roundtrip_cache.py \
  20260524T205027Z-llmfinal artifacts/results/predictions.jsonl

To rerun the LLM-backed round-trip validator instead of using the submitted predictions, export OPENAI_API_KEY and run make run. Live calls are not required for checking the submitted scorecard.

Repository Layout

• specfault-dafny/README.md - benchmark package instructions
• specfault-dafny/bench/items/ - scored Dafny corpus
• specfault-dafny/artifacts/results/ - final prediction, verification, and scorecard artifacts
• specfault-dafny/artifacts/cards/ - generated per-item evidence cards
• specfault-dafny/report/tables/ - generated report tables
• submission/ - report, rendered PDF/HTML, and demo script