README.md

---
license: mit
language:
- en
base_model:
- deepseek-ai/deepseek-coder-7b-instruct-v1.5
---

<p align="center">
  <img width=20%" src="figures/logo.png">
</p>

## Introduction

We present a fine-tuned model for formal verification tasks. It is fine-tuned in five formal specification languages (Cog, Dafny, Lean4, ACSL, and TLA) on six formal-verification-related tasks:

- **Requirement Analysis**: given requirements and description of the verification or modeling goals, decomposing the goal into detailed verification steps

- **Proof/Model Generation**: given requirements and description of the verification or modeling goals, writing formal proofs or models that can be verified by verifier/model checker.

- **Proof segment generation**

- **Proof Completion**: complete the given incomplete proofs or models

- **Proof Infilling**: filling in the middle of the given incomplete proofs or models

- **Code 2 Proof**: (Currently only support for ACSL whose specification is in form of code annotations) given the code under verification, generate the proof with the specifications

## Application Scenario

<p align="center">
  <img width=100%" src="figures/application.png">
</p>


## Supported Formal Specification Languages

<p align="center">
  <img width=100%" src="figures/examples.png">
</p>

## Data Preparation Pipeline
<p align="center">
  <img width=60%" src="figures/data-prepare.png">
</p>


## Citation
```
@misc{fmbench25jialun,
      title={From Informal to Formal--Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs}, 
      author={Jialun Cao, Yaojie Lu, Meiziniu Li, Haoyang Ma, Haokun Li, Mengda He, Cheng Wen, Le Sun, Hongyu Zhang, Shengchao Qin, Shing-Chi Cheung, Cong Tian},
      year={2025},
      eprint={2501.16207},
      archivePrefix={arXiv},
      primaryClass={cs.AI},
      url={https://arxiv.org/abs/2501.16207}, 
}

```