An Empirical Study of LLM-Generated Specifications for VeriFast

Static verification tools are essential for ensuring the reliability of industrial-scale software, but they impose a significant "specification burden" on developers. Tools based on separation logic (SL), such as VeriFast, are particularly powerful for verifying heap-manipulating programs but require complex auxiliary specifications—such as loop invariants, inductive lemmas, and manual heap management (folds/unfolds)—to guide the verification process. This study investigates whether Large Language Models (LLMs) can automate the generation of these challenging specifications.

The researchers evaluated ten different LLMs across eight prompting strategies using a dataset of 303 C functions. The study was conducted in two stages: a pilot study to identify the most effective models and prompts, followed by a large-scale evaluation. The models were tasked with generating the necessary VeriFast specifications for C functions, given inputs ranging from natural language descriptions to formal contracts. The output was assessed based on the preservation of functional behavior, the ability to pass the VeriFast verification process, and a qualitative analysis of the errors encountered when verification failed.

The study reveals a significant gap between the models' ability to write code and their ability to perform formal verification. While LLMs successfully maintained the intended functional behavior in over 91% of cases, their verification success rate was modest at 31.4%. The researchers found that Gemini 2.5 Pro performed best, particularly when provided with formal contracts as input. Crucially, 94% of the failures were attributed to the models' lack of domain-specific knowledge regarding separation logic and VeriFast’s specific syntax and heap-reasoning requirements, rather than general logical errors.