fm-universe/llama3.1-8b-fma

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