Create README.md

README.md

@@ -0,0 +1,48 @@
+---
+license: mit
+language:
+- en
+base_model:
+- meta-llama/Llama-3.1-8B
+---
+
+<p align="center">
+  <img width=20%" src="figures/logo.png">
+</p>
+
+## Introduction
+
+We present a fine-tuned model based on llama-3.1-8B 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:
+
+The fm-alpaca (the fine-tuning dataset) will be released soon.
+
+- **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>
+