All datasets / Veri-Code

Veri-Code/ReForm-DafnyComp-Benchmark

234 downloads in 30 days1 likesLast modified 7 May 2026View on Hugging Face

Use restrictions

The declared licence (cc-by-nc-4.0) is classified as having use restrictions.

Declared licence: cc-by-nc-4.0, from the tagEvidence: README.md at 10750d1
Licence files: No licence file at the top level of the repositoryEvidence: file list at 10750d1
Declared sources: None listed in the card metadata
Access gated on Hugging Face: No

Each cell links to what was checked: a file, a file list or a Hub record.

Tasks

text-generation

Citation text from the card

@misc{yan2025reformreducinghuman,
      title={Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny}, 
      author={Chuanhao Yan and Fengdi Che and Xuhan Huang and Xu Xu and Xin Li and Yizhi Li and Xingwei Qu and Jingzhe Shi and Zhuangzhuang He and Chenghua Lin and Yaodong Yang and Binhang Yuan and Hang Zhao and Yu Qiao and Bowen Zhou and Jie Fu},
      year={2025},
      eprint={2507.16331},
      archivePrefix={arXiv},
      primaryClass={cs.CL},
      url={https://arxiv.org/abs/2507.16331}, 
}

@misc{xu2025localsuccessdoescompose,
      title={Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification}, 
      author={Xu Xu and Xin Li and Xingwei Qu and Jie Fu and Binhang Yuan},
      year={2025},
      eprint={2509.23061},
      archivePrefix={arXiv},
      primaryClass={cs.PL},
      url={https://arxiv.org/abs/2509.23061}, 
}

All datasets marked Use restrictions | JSON

The same facts for your agent

A free MCP server at mcp.datalicense.uk/mcp. Connect it from an MCP client such as Claude or Cursor.

dataset_licence({ "id": "Veri-Code/ReForm-DafnyComp-Benchmark" })
signal: "restrictive"
stated_licence: "cc-by-nc-4.0"
sources: 0