---
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>