LLMs Show Promise but Fall Short at Generating Verification Specifications

Researchers have conducted an extensive empirical evaluation of how well large language models can automatically generate specifications for VeriFast, a static verification tool that uses separation logic to reason about heap-manipulating programs.

Static verifiers promise industrial-scale software assurance, but writing the detailed specifications they require—especially for separation logic-based tools—demands significant manual effort. A new study on arXiv from the Software Engineering community investigates whether LLMs can help bridge this gap.

The Experiment#

The researchers tested eight different prompting strategies across ten LLMs on 303 C functions, examining three input types across two stages. They analyzed both quantitative metrics and qualitative patterns in the results.

Key Findings#

The results reveal a nuanced picture:

• Code preservation: LLMs maintained functional behavior in both source code and generated specifications at over 91%, suggesting they grasp the core logic reasonably well.
• Verification success: Only 31.4% of functions verified successfully, revealing the core challenge.
• Best performers: Gemini 2.5 Pro achieved the highest success rates, particularly when provided with formal contracts as input.
• Error patterns: Nearly 94% of failures traced back to domain-specific gaps—specifically LLMs' limited understanding of separation logic concepts that VeriFast requires.

Implications#

The findings suggest that generic prompting approaches have room for improvement when applied to specialized verification tools. The research provides actionable guidance for optimizing LLM-assisted specification generation, pointing toward the need for better instruction or fine-tuning approaches that capture the subtleties of formal verification systems.