Improve model card for Re:Form: add metadata, links, and usage example

This PR significantly enhances the model card for the `Re:Form` model by:

* Adding `pipeline_tag: text-generation` and `library_name: transformers` to the metadata, which improves discoverability and integration with the Hugging Face Hub features.
* Including relevant tags such as `code-generation`, `formal-verification`, `reinforcement-learning`, and `dafny` for better categorization.
* Providing a concise model description summarizing the paper's abstract.
* Including the project page link ([https://veri-code.github.io/ReForm-page](https://veri-code.github.io/ReForm-page)) and updating the GitHub repository link to point to the main project repository ([https://github.com/Veri-Code/Veri-Code](https://github.com/Veri-Code/Veri-Code)).
* Adding the overall pipeline image from the project's GitHub repository for visual context.
* Providing a runnable Python code snippet to demonstrate basic usage with the `transformers` library for Dafny code generation.
* Including the full BibTeX citation for proper academic attribution.
* Removing the unnecessary "File information" section to keep the model card clean and focused.

These updates greatly improve the model's documentation and user experience on the Hugging Face Hub.

README.md

@@ -1,3 +1,83 @@
----
-license: mit
----
+---
+license: mit
+pipeline_tag: text-generation
+library_name: transformers
+tags:
+- code-generation
+- formal-verification
+- reinforcement-learning
+- dafny
+---
+
+# Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny
+
+This repository hosts the `sft_0.5B` model, part of the **Re:Form** framework, which focuses on enhancing formal software verification using Large Language Models (LLMs) and Reinforcement Learning (RL).
+
+**Re:Form** addresses the limitations of informal language-based LLMs by grounding them in rigorous formal systems, such as Dafny. This approach enables automatic and mathematically provable verification of the LLMs' reasoning processes and outcomes, crucial for large-scale, reliable formal software verification. The framework introduces an automatic and scalable data curation pipeline and integrates RL designs with feedback from a formal language verifier to reduce reliance on human priors.
+
+-   **Paper**: [Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny](https://huggingface.co/papers/2507.16331)
+-   **Project Page**: [https://veri-code.github.io/ReForm-page](https://veri-code.github.io/ReForm-page)
+-   **Code**: [https://github.com/Veri-Code/Veri-Code](https://github.com/Veri-Code/Veri-Code)
+
+<p align="center">
+  <img src="https://github.com/Veri-Code/Veri-Code/raw/main/assets/pipeline.png" alt="Overall Pipeline" width="700"/>
+  <br>
+  <em>Overall Pipeline of Re:Form</em>
+</p>
+
+## Usage
+
+You can load and use the `Re:Form` model with the `transformers` library for Dafny code generation.
+
+```python
+from transformers import AutoModelForCausalLM, AutoTokenizer
+import torch
+
+model_id = "Veri-Code/sft_0.5B" # Example checkpoint; other available include sft_1.5B, sft_3B, sft_7B, sft_14B, 14B-RL-entropy
+
+tokenizer = AutoTokenizer.from_pretrained(model_id, trust_remote_code=True)
+model = AutoModelForCausalLM.from_pretrained(
+    model_id,
+    torch_dtype=torch.bfloat16, # Use bfloat16 for optimal performance if supported
+    device_map="auto",
+    trust_remote_code=True,
+)
+
+# Example prompt for Dafny code generation
+# This prompt asks the model to implement a simple Max method in Dafny.
+prompt = "method Max(a: int, b: int) returns (m: int)\
+  ensures m == a || m == b\
+  ensures m >= a && m >= b\
+{\
+"
+
+input_ids = tokenizer(prompt, return_tensors="pt").to(model.device)
+
+# Generate Dafny code
+generated_ids = model.generate(
+    **input_ids,
+    max_new_tokens=100,
+    temperature=0.7,
+    do_sample=True,
+    eos_token_id=tokenizer.eos_token_id,
+)
+
+generated_text = tokenizer.decode(generated_ids[0], skip_special_tokens=True)
+print(generated_text)
+```
+
+## Citation
+
+If you use this work in your research, please cite:
+
+```bibtex
+@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}, 
+}
+```