license: mit
language:
- en
base_model:
- meta-llama/Llama-3.1-8B
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
Supported Formal Specification Languages
Data Preparation Pipeline
