# Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast

arXiv: https://arxiv.org/abs/2411.02318 · HTML: https://mlsanity.com/paper/2411.02318/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 26 references that are in the map.
- First posted on arXiv 4 Nov 2024.

## Builds on (most cited first, 9 of 9)

- [A Systematic Survey of Prompt Engineering in Large Language Models: Techniques and Applications](https://mlsanity.com/paper/2402.07927/) (2024)
- [CodeT: Code Generation with Generated Tests](https://mlsanity.com/paper/2207.10397/) (2022)
- [An Empirical Evaluation of Using Large Language Models for Automated Unit Test Generation](https://mlsanity.com/paper/2302.06527/) (2023)
- [Software Testing with Large Language Models: Survey, Landscape, and Vision](https://mlsanity.com/paper/2307.07221/) (2023)
- [Automatic Generation of Programming Exercises and Code Explanations using Large Language Models](https://mlsanity.com/paper/2206.11861/) (2022)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [LLMSTEP: LLM proofstep suggestions in Lean](https://mlsanity.com/paper/2310.18457/) (2023)
- [CAT-LM: Training Language Models on Aligned Code And Tests](https://mlsanity.com/paper/2310.01602/) (2023)
- [Laurel: Unblocking Automated Verification with Large Language Models](https://mlsanity.com/paper/2405.16792/) (2024)

## Built on by (most cited first, 5 of 5)

- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [PCN-Rec: Agentic Proof-Carrying Negotiation for Reliable Governance-Constrained Recommendation](https://mlsanity.com/paper/2601.09771/) (2026)
- [Evaluating LLM-Generated ACSL Annotations for Formal Verification](https://mlsanity.com/paper/2602.13851/) (2026)
- [Working Document -- Formalising Software Requirements with Large Language Models](https://mlsanity.com/paper/2506.14627/) (2025)
- [TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation](https://mlsanity.com/paper/2607.23425/) (2026)

## Abstract (arXiv)

Static verification is a powerful method for enhancing software quality, but it demands significant human labor and resources. This is particularly true of static verifiers that reason about heap manipulating programs using an ownership logic. LLMs have shown promise in a number of software engineering activities, including code generation, test generation, proof generation for theorem provers, and specification generation for static verifiers. However, prior work has not explored how well LLMs can perform specification generation for specifications based in an ownership logic, such as separation logic. To address this gap, this paper explores OpenAI's GPT-4o model's effectiveness in generating specifications on C programs that are verifiable with VeriFast, a separation logic based static verifier. Our experiment employs three different types of user inputs as well as basic and Chain-of-Thought (CoT) prompting to assess GPT's capabilities. Our results indicate that the specifications generated by GPT-4o preserve functional behavior, but struggle to be verifiable. When the specifications are verifiable they contain redundancies. Future directions are discussed to improve the performance.