Source-linked AI summary
Are LLM-Generated Formal Specifications Faithful to Their Requirements? A Study on Bimodal Formal Specification Generation
Wenhan Wang, Shiming Chen, Zeyu Sun, Shenghua Feng
TL;DR
LLM specification generation often assumes implementation correctness, leaving open whether generated specifications faithfully represent requirements when code may be wrong. This study evaluates bimodal ACSL generation with Frama-C and finds that verifier success can be misleading on incorrect code; it concludes that requirement faithfulness needs greater focus.
Problem
Code-based specification generation often assumes correct implementations, although verification must assess whether code meets requirements when correctness is unknown.
Source: §1 · p. 2Method
The study evaluates LLM-generated ACSL specifications from requirements and implementations of unknown correctness, using a 1,403-program benchmark and Frama-C verification.
Source: §1 · p. 2, §3.1 · p. 4Results
For correct implementations, adding requirements does not consistently improve verification success over code-only prompting; on incorrect code, specifications may be weak or misled, and ACSL is less effective than HoarePrompt at predicting consistency.
Source: §6 · pp. 15–16Takeaways & Limitations
Future work should focus more on requirement-faithful specification generation and tighter integration between LLM reasoning and deductive verification feedback.
Source: §6 · p. 16The programming-contest benchmark uses relatively detailed, less ambiguous requirements and small programs, so findings may not directly generalize to large codebases or complex environmental assumptions.
Source: §5 · p. 15
Abstract
from arXiv · showhide
Formal specification generation is a critical step towards formal verification and correctness assurance of software. Recently, large language models have been widely adopted in automatic generation of formal specifications. However, existing LLM-based specification generation approaches often assume that the input program is correct, which deviates from the real purpose of formal verification---to figure out whether the program meets its requirements when its correctness is unknown. Therefore, we conduct an empirical study of LLM-based specification generation under the bimodal setting: given both the natural language requirement and its corresponding code implementation, whose correctness is unknown. We construct a benchmark of 1,403 C programs and evaluate ACSL specification generation with Frama-C verification. Our study reaches several interesting findings: first, when the code implementation is correct, providing the natural language requirement does not further improve the pass rate of generated specifications. Second, when the code implementation is incorrect, LLM-based specification generation may erroneously pass verification by producing weak or implementation-misled specifications, and this cannot be fully alleviated by advanced prompting approaches. Compared with the non-formal HoarePrompt approach, LLM-generated formal specifications are less effective in predicting requirement-code consistency. Our study takes a first look at applying LLM-based formal specification generation to verifying program correctness against requirements, and points to requirement-faithful specification generation as a new direction for future LLM-based formal specification research.
1 Introduction
The introduction identifies a gap in generating specifications from both requirements and implementations when implementation correctness is unknown. It frames requirement faithfulness—not verifier success alone—as central to using generated specifications to assess program correctness.
1 Introduction
- Specifications must capture intended behavior while including implementation-aware details, such as memory constraints, control-flow conditions, and loop invariants, for formal verification.Source: §1 · p. 2
- Prior code-based work often assumes correct implementations, while requirement-based generation lacks implementation context for proof-relevant components; neither directly addresses bimodal generation with unknown correctness.Earlier approaches also used non-verifiable assertions or specifications generated from correct programs to detect bugs in mutants.Source: §1 · p. 2
- The study evaluates ACSL generation on 1,403 programs from 500 contest problems, using both correct and incorrect implementations, and examines modality, prompting, and consistency prediction.Its benchmark pairs natural-language requirements with normalized C implementations checked using Frama-C.Source: §1 · pp. 2–3
- For correct implementations, requirements do not necessarily improve specification verification; for incorrect ones, weak or implementation-misled specifications may pass.Thus, a verifier pass on incorrect code is not always evidence that a specification captures the requirement.Source: §1 · pp. 2–3
- The study positions requirement faithfulness as an evaluation target alongside syntactic correctness and verifier pass rates.It frames bimodal specification generation as both a generation problem and a requirement-faithfulness problem.Source: §1 · p. 3
2 Related Work
Related work covers LLM specification generation from code and natural language, while noting that these lines address different languages, specification types, and verification settings.
2 Related Work
- Code-oriented work includes LLM-generated invariants, ACSL generation integrated with static analysis, verifier-feedback repair, and benchmarks for JML specifications [4] [11] [13] [14] [20] [21] [23].Source: §2 · p. 3
- Natural-language approaches include temporal logic, post-condition generation, multi-language specification studies, Rocq specifications, and joint Dafny code-and-specification generation [1] [3] [5] [6] [8] [15] [18] [22] [24].Source: §2 · p. 3
- The paper distinguishes its focus on formal specifications for program verification from much natural-language work centered on temporal logic [5] [6] [8].Source: §2 · p. 3
3 Methodology
The methodology defines bimodal specification generation as using the requirement as the semantic oracle and the implementation as proof-relevant context. It builds a 1,403-program benchmark and evaluates generation across four research questions.
3.1 Overview and Task Definition
- Bimodal generation takes a requirement and an implementation of unknown correctness as input; the specification should describe expected behavior in the requirement, using code only as proof-relevant context.The generated specification comprises a pre-condition, post-condition, and auxiliary elements such as loop invariants and assertions.Source: §3.1 · p. 4
3.2 Benchmark Construction
- The benchmark contains 1,403 programs from 500 contest problems, with up to one correct and two incorrect implementations per problem.Programs were filtered and rewritten for ACSL and Frama-C; rewritten return values were checked against the original programs using provided test cases.Source: §3.2 · pp. 4–5
3.3.1 RQ1: input modality.
- On correct implementations, RQ1 compares requirement plus complete code, code alone, and requirement plus function signature using syntactic correctness and verification pass rates.Source: §3.3.1 · p. 5
3.3.2 RQ2: performance on incorrect implementations.
- For incorrect implementations, generated specifications are classified using Frama-C verification and E-ACSL runtime checks to distinguish requirement-consistent, wrong, misled, and weak specifications.The runtime-checking procedure runs up to 40 test cases, prioritizing tests on which the original implementation fails.Source: §3.3.2 · p. 6, Table 2 · p. 6
3.3.3 RQ3: advanced prompting.
- RULER first infers expected pre- and postconditions from the requirement, then iteratively refines ACSL specifications using the implementation, verifier feedback, and an LLM judge.Unlike methods that stop when verification passes, RULER may stop after a verification failure if the judge considers the specification requirement-consistent.Source: §3.3.3 · pp. 6–7
3.3.4 RQ4: comparison with non-formal approaches.
- RQ4 reimplements HoarePrompt for C and compares it with basic prompting and RULER as program-level correctness classifiers, reporting balanced accuracy, true positive rate, false positive rate, and MCC.For the specification pipelines, Frama-C verification success is labeled Correct and other outcomes Incorrect.Source: §3.3.4 · p. 7
4 Evaluation
The evaluation tests ACSL generation across input modalities, incorrect implementations, prompting strategies, and requirement-code consistency prediction. Code-only generation verifies most often on correct programs, but formal-specification generation remains less effective than HoarePrompt at predicting consistency.
4.1 Evaluation Setup
- Three LLMs generated ACSL specifications that were checked with Frama-C 32.0 and WP, with proof obligations discharged by Alt-Ergo and Z3 under a 30-second timeout.A pair counted as verified only when all obligations were discharged; syntax errors and timeouts counted as failures.Source: §4.1 · p. 7
4.2 RQ1: input modality
- Among syntactically correct specifications, Code only reaches 38.19% Ver.|Syn., compared with 30.57% for Req.+Code and 19.61% for Req.+Sig.; control-flow complexity further lowers verification rates.Source: §4.2 · pp. 8–9
4.3 RQ2: performance on incorrect implementations
- Only about one quarter of incorrect implementations receive specifications classified as requirement-consistent, and verification failures alone are a coarse faithfulness signal.False positives are less frequent than failures, but misled specifications outnumber weak ones; complex GPT-5.5 specifications also leave many cases unclassified.Source: §4.3 · pp. 10–11, Table 6 · p. 10
4.4 RQ3: advanced prompting
- 24.27% vs. 18.47%: RULER (2-stage+refine) improves final success on correct implementations; on incorrect implementations, it reaches 29.49% vs. 24.95%, with model-level instability.RULER (2-stage) alone does not consistently improve results, and GPT-5.5's successful cases on incorrect implementations decrease after refinement.Source: §4.4 · pp. 12–13, Table 7 · p. 14
4.5 RQ4: comparison with non-formal approaches
- HoarePrompt averages 0.7916 BA and 0.5788 MCC, versus 0.2688 BA and -0.4452 MCC for Ours (RULER (2-stage+refine)) on all samples.The formal pipeline's low true-positive rate reflects specifications that are invalid, unverifiable, or unfaithful to requirements.Source: §4.5 · pp. 13–15, Table 8 · p. 14
5 Threats to Validity
The evaluation is limited by preprocessing and LLM nondeterminism, imperfect measures of semantic faithfulness, and a benchmark whose scale and requirements may not represent industrial software.
5 Threats to Validity
- Preprocessing may leave semantic changes undetected because validation relies on tests that may not cover all program behaviors.The study rewrites input/output logic into function arguments and return values for ACSL and Frama-C compatibility.Source: §5 · p. 15
- Syntactic correctness, Frama-C outcomes, and manual classifications only approximate specification quality and do not fully measure semantic faithfulness to requirements.Verification failure can reflect an unfaithful or ill-formed specification, while verification success can result from a weak or implementation-misled one.Source: §5 · p. 15
- Because the benchmark uses relatively small contest programs and typically clearer requirements, findings may not generalize directly to large codebases, domain-specific APIs, or complex environmental assumptions.The authors describe programming contests as a controlled setting for studying the core bimodal problem.Source: §5 · p. 15
6 Conclusion
The study finds that bimodal specification generation remains difficult: requirements do not consistently improve verification success on correct code, and incorrect code can mislead generation. ACSL specifications are less effective than non-formal HoarePrompt at predicting requirement–implementation consistency, motivating further focus on requirement faithfulness.
6 Conclusion
- Bimodal specification generation is substantially harder than generating specifications from correct code alone.Source: §6 · p. 15
- For correct implementations, adding requirements does not consistently improve verification success over code-only prompting.Source: §6 · p. 15
- For incorrect implementations, generated specifications may be weak or implementation-misled and fail to expose requirement–code mismatches despite advanced prompting.Source: §6 · p. 15
- LLM-generated ACSL specifications are less effective than non-formal HoarePrompt at predicting consistency between requirements and implementations.Source: §6 · p. 16
- The authors identify requirement-faithful specification generation as a future research focus, alongside tighter integration of LLM reasoning and deductive-verification feedback.Source: §6 · p. 16