{"id":"e4c0a34d-3b3a-40d8-9208-c8e18bc082ba","arxiv_id":"2411.13269","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":5,"one_line_summary":"A feasibility study in which GPT-4 and GPT-3.5 generated C code for three Scania automotive modules, and some of that code passed Frama-C verification against hand-derived ACSL specifications without iterative feedback.","lead":"This paper asks whether large language models can write safety-critical car software from specifications alone, and whether the generated code can pass formal proof-based verification. It presents a framework called spec2code and a first test on three real truck modules from Scania, where some generated code was fully verified against hand-written formal specs.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Ghost-variable conversion in all case studies changes the verified property; Frama-C proofs do not establish correctness with respect to the original ACSL specifications or intended behavior.","rationale":"The reader's weakest assumption was that the hand-derived ACSL specifications faithfully capture intended behavior. My concern is related but distinct: even if the ACSL specifications were complete, the verification results are compromised because ghost variables were converted to concrete variables in every case study. This directly undermines the load-bearing claim that Frama-C formally verified the generated code against the actual specifications. The paper itself acknowledges that conversion was necessary for compilation and that equivalence checking failed, but it does not draw the conclusion that the formal verification is no longer evidence of correctness relative to the original specification. This is a concrete, technical flaw rather than a matter of external validity. Despite its severity, the paper is explicitly a first feasibility study and the authors are transparent about the modification in Section 7. The appropriate verdict remains CONDITIONAL: the framework is plausible, but the empirical evidence needs to be re-examined by re-verifying at least one case with original ghost-variable specifications or by arguing that the conversion preserves the intended contract. Since the reader already reached CONDITIONAL, my read does not change the verdict, but it identifies a more specific condition that should be imposed.","tokens_in":12594,"tokens_out":6234,"duration_ms":65667,"concrete_test":"Take one successful generation, e.g., GPT-4-turbo with ACSL-only for SFLD (Table 1, 33/33 proved goals). Restore the original ACSL specification with ghost variables and the original function interface without the concrete gh_* globals. Run Frama-C WP on the generated code with ghost annotations that relate local variables to ghost variables as in the reference implementation. If the proof goals do not all close, or if ghost assignments would need to be inserted into the generated code, the reported verification is an artifact of the conversion. Alternatively, use diffkemp to compare reference and generated programs after masking writes to the converted ghost globals; if equivalence then holds, the extra side effects are the sole difference and integration would change observable behavior.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central empirical claim depends on Frama-C verification of LLM-generated code against ACSL specifications. However, Section 7 (Ghost variables) states that in all case studies the authors 'converted the ghost variables in the specification to concrete variables' so the generated code would compile. This changes the verification target. The original ACSL specifications used ghost variables to express behavior without making those values program-visible; the converted specifications make them concrete globals that the generated code must assign. The reference programs implement the same behavior with local variables hidden by scoping, so the generated code introduces additional side effects on these globals. The paper's equivalence checking failed in every case, and the authors explicitly attribute one reason to this ghost-variable conversion. Consequently, a Frama-C proof of the converted specification does not establish that the generated code satisfies the original ACSL specification, nor that it is behaviorally equivalent to the reference module. The statement that 'formally verified code' was generated is therefore true only with respect to an altered specification, and the feasibility evidence does not support the claim that formally correct code with respect to the intended behavior can be generated without iterative backprompting or fine-tuning.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes spec2code, a framework that combines LLM-based code generation with software verifiers and other critics in an iterative refinement loop, and then evaluates a minimalist instantiation of it on three industrial automotive modules from Scania (SFLD, BRAK, STEE). In the feasibility study, gpt-3.5 and gpt-4-turbo are prompted with combinations of high-level natural language, low-level natural language, and ACSL formal specifications; the generated C code is compiled with GCC, verified with Frama-C WP using Z3 and Alt-Ergo, checked for semantic equivalence with diffkemp against reference implementations, and manually assessed against the 'power of 10' rules. The results show that compilable code is produced for many specification combinations, and that fully verified code (all proof goals proved) is obtained for some combinations in two of the three case studies, but diffkemp equivalence failed in every case. The paper concludes that formally correct code can be generated from specifications without iterative backprompting or fine-tuning, while acknowledging that correctness is relative to the supplied specifications.","tokens_in":12818,"tokens_out":7480,"duration_ms":77098,"significance":"If substantiated, the result is a meaningful feasibility data point: it suggests that off-the-shelf LLMs can generate code that passes machine-checked formal verification from formal specifications in a single generation step, without iterative prompting or fine-tuning, in a safety-critical automotive context. The study has several strengths: the use of real, proprietary Scania modules avoids the well-known training-data leakage threat; the verification results are produced by external tools (Frama-C WP with Z3 and Alt-Ergo) rather than by the LLM itself; and the paper is transparent about important limitations. The spec2code framework itself is a useful conceptual contribution, though its general formulation is largely an adaptation of the LLM-Modulo framework. The significance is substantially tempered, however, by two issues: the ACSL specifications used in the experiments were altered (ghost variables converted to concrete variables), so the verification is not against the original hand-derived specifications; and the semantic equivalence checks with the reference programs failed in all cases.","major_comments":[{"comment":"The conversion of ghost variables to concrete variables, stated in the 'Ghost variables' paragraph, changes the verification target. The Frama-C proofs reported in Tables 1-3 are for these converted specifications, not for the original hand-derived ACSL specifications described in Section 4.2. Because the generated programs are required to assign concrete global variables that the reference programs keep local, the proof does not establish that the generated code satisfies the original ACSL specifications. The authors themselves report in the same section that diffkemp equivalence fails in all cases, partly for this reason. Therefore the conclusion in Section 8 that 'formally correct code' was generated is only justified with respect to the modified specifications, and the paper does not establish correctness with respect to the intended behavior of the reference modules. The authors should either rerun the verification against the original ghost-variable specifications (for example, using Frama-C's ghost-variable support with appropriate ghost statements), or provide a rigorous argument and evidence that the conversion preserves the intended functional behavior.","section":"Section 7 (Ghost variables)"},{"comment":"The term 'formally verified' is used without an explicit operational criterion. The 'Verified (Proved Goals)' columns in Tables 1-3 report ratios such as 33/33, 41/50, and 8/8, but the text does not state that a row is considered verified only when all proof goals are discharged, nor does it identify which specific rows support the conclusion that formal verification was achieved 'for some combination of specifications, in two of the three case studies.' A reader cannot unambiguously map that claim to the data; for example, BRAK shows 30/30 for HLNL+LLNL (a combination that includes no formal ACSL), while STEE shows 8/8 for several ACSL-inclusive combinations. Please define the verification criterion explicitly and list the exact (model, specification) combinations that are fully verified, and relate those to the conclusion.","section":"Section 6 and Section 8"},{"comment":"The paper reports that the program equivalence check failed for every generated program, and attributes this to unspecified behavior and the ghost-variable conversion. However, it does not provide a concrete analysis of whether the observed semantic deviations between generated and reference programs are benign (e.g., only additional writes to formerly ghost variables) or whether they could correspond to genuine functional differences. Without such an analysis, the statement in Section 8 that the generated code is of 'industrial quality' and 'could be hypothetically integrated in the Scania production code' is not supported by the presented evidence. At most, the study shows that generated code can satisfy the (modified) ACSL specifications; it does not show that the code would behave equivalently to the original production modules.","section":"Section 7 (Equivalence checking) and Section 8"}],"minor_comments":[{"comment":"The process of deriving ACSL specifications by hand from natural language specifications is a load-bearing step for the whole study, yet it is described in a single sentence. A short description of the derivation method, the expertise involved, and any consistency checks would help readers judge the quality and completeness of the formal specifications.","section":"Section 4.2"},{"comment":"The LLM hyperparameters are reported, but there is no sensitivity analysis for temperature or other parameters. Since the study relies on a single pass@1 output per configuration, the results may be sensitive to the chosen temperature (0.8); a small-scale variation study or a justification based on prior work would strengthen the comparisons.","section":"Section 5.2"},{"comment":"The column header 'Verified (Proved Goals)' mixes two pieces of information: the number of proved goals out of the total, and whether equivalence was shown. Consider splitting this into separate columns, e.g., 'Proved goals' and 'Equivalence', with a clear note on what 'Not Eq' means (equivalence could not be shown, not necessarily that the programs are inequivalent).","section":"Tables 1-3"},{"comment":"The term 'pass@1' is used in the LLM comparison paragraph but not defined; please define it or replace it with a standard metric name (e.g., 'first-attempt success').","section":"Section 7"},{"comment":"The prompt template is informative, but it is unclear how the ACSL specifications (including any ghost variables) are inserted into the prompt. Clarify the exact placement and formatting of ACSL annotations relative to the C header and function signature, since this directly affects the LLM's behavior.","section":"Appendix A"}],"recommendation":"major_revision","confidential_remarks":"The paper is a reasonable feasibility study with transparent limitations, and the empirical setup (external verifiers, proprietary industrial modules) is a strength. The main obstacle is the gap between the claim of 'formally verified code' and the fact that the verified specifications were modified by converting ghost variables to concrete variables. This is not a fatal flaw—it is a claim that can be repaired either by verifying against the original ghost-variable specifications or by carefully delimiting the conclusion. The failure of all equivalence checks further weakens the evidence, and the manuscript would benefit from an explicit criterion for what counts as 'verified.' I would support acceptance after a major revision that addresses these points, because the central idea is sound and the study is a useful contribution to the nascent area of LLM-based code generation for safety-critical software."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"First thing to know: this is a legitimate feasibility study with machine-checked proofs, but the central claim is weaker than it looks because the specs were changed. In Section 7 they admit they converted ghost variables to concrete variables in every case study so the LLM would produce compilable code. That changes the verification target. The original ACSL specs used ghost variables to express behavior without making values program-visible; the converted specs make them concrete globals the generated code must assign. The reference programs keep these as local variables, so the generated code has extra side effects. Unsurprisingly, diffkemp equivalence checking failed in every case, and the authors attribute one reason to this conversion. So \"formally verified code\" is true only against the rewritten ACSL, not the original specification or the intended behavior. That's a real soft spot, not a manufactured one.\n\nWhat's genuinely new: applying the LLM-Modulo idea to code generation, with Frama-C as critic, on proprietary Scania modules that aren't in training data. The framework itself is a reasonable adaptation, and the minimalist instantiation without backprompting is a fair first test. The Frama-C WP proofs with Z3 and Alt-Ergo are real, and the paper is honest about the small size and low complexity of the cases. The conclusion correctly notes that correctness is only relative to the specs and that complete specs are rare in industry—that's a good caveat.\n\nOther soft spots: the ACSL specs were hand-derived from natural language (Section 4.2), so the oracle isn't independent; no artifacts are provided; hyperparameters are given but no ablation. None of these are fatal, but they reinforce that this is a preliminary feasibility result.\n\nWho is this for? Researchers working on LLM-based code generation with formal verification, especially in automotive/embedded. They'll find the case study useful, not decisive. The paper deserves a serious referee—it has real data and real proofs—but the ghost-variable issue must be addressed, and the claims should be scoped to \"verified against a rewritten specification\" unless they can show the conversion is behavior-preserving in these cases. I'd recommend \"major revision\" with that as the central demand.","headline":"A real but modest feasibility study; the ghost-variable conversion in all cases means the Frama-C proofs target an altered specification, so the headline claim needs reining in.","tokens_in":13328,"tokens_out":1889,"would_cite":true,"duration_ms":19322,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A feasibility study shows LLMs can turn specifications into formally verified embedded C code without iterative repair, though only in two of three industrial cases.","keywords":["Code Generation","Formal verification","Large Language Models","Automated Software Engineering","ACSL","embedded software","deductive verification","spec2code"],"falsifier":"Have a second engineer independently translate the natural-language requirements of the three modules into ACSL specifications without seeing the original code or the paper's contracts, then rerun the same prompts; if any of the newly generated programs fails to compile or fails Frama-C verification, the original verified results were carried by the particular hand-written specifications rather than by the method itself.","tokens_in":12407,"feed_emoji":"🚗","tokens_out":7891,"duration_ms":70174,"temperature":0.7,"pith_summary":"This paper tries to establish that off-the-shelf large language models, guided only by specifications and checked by a compiler and a deductive verifier, can generate embedded C code of industrial quality. It introduces spec2code, a framework in which an LLM produces code from formal ACSL contracts and natural-language requirements, and critics (a compiler and a verification tool) assess the output. A deliberately weak instantiation of the framework, with no iterative backprompting and no fine-tuning, was applied to three production modules for truck electronics. The generated code compiled in all three case studies, and Frama-C formally verified the code against its ACSL specifications for at least one combination of specification types in two of the three modules. The paper argues this makes it plausible that specification-driven code generation can eventually shift the bottleneck of safety-critical software development from coding to the writing of complete formal specifications.","feed_headline":"Spec-only LLM C code passes formal proof in 2 of 3 cases","feed_subtitle":"Off-the-shelf models turn specs into compiled, formally verified C code on real truck modules, no backprompting needed.","key_machinery":"The load-bearing object is spec2code, a framework that wraps an LLM in a loop of critics: a verification engineer writes specifications in natural language and in ACSL, a prompt template (built on Zero-shot-CoT, i.e. the instruction 'Let's think step by step') asks the model to complete a given C function from the module interface, and the output must first survive compilation by GCC and then be checked by Frama-C's WP plugin against the ACSL contract. In the full framework the critics' feedback feeds iterative backprompting, supervised fine-tuning, and preference optimization; the feasibility study removes all of those and keeps only one-shot generation followed by the critics, which allows the experiment to isolate whether the LLM itself can carry the specification-to-code step. A notable detail is that ghost variables in the ACSL contracts were converted into ordinary concrete variables in the prompt, because the models tended to misuse them; this conversion is part of what makes the formal verification go through.","core_discovery":"The central discovery is a positive feasibility result for the 'minimalist' version of spec2code: without iterative backprompting and without fine-tuning, a single zero-shot chain-of-thought prompt fed with ACSL specifications, high-level natural-language specifications, low-level natural-language specifications, or their combinations produced C code that compiled with GCC in all three case studies (Steering Fluid Level Detection, Brake Light Activation, Power Steering Backup). Using Frama-C's weakest-precondition plugin, the paper reports fully proved verification goals for several specification combinations in the Brake Light and Power Steering modules, and partial proof obligations elsewhere, with GPT-4-turbo more consistently successful than GPT-3.5. The paper is careful to note that program-equivalence checking against the original hand-written reference programs did not succeed in any case; manual inspection attributes this to ghost variables being realized as concrete variables in generated code and to unspecified behavior, not necessarily to functional deviation. It also reports that every compilable generated program adhered to the 'power of 10' rules for safety-critical code and generated no compiler warnings. The conclusion the authors draw is that formally correct code can be generated from specifications alone, at least for small, single-function modules, and that the main remaining condition is completeness of the specifications.","pith_inferences":["An implication the authors leave implicit: if the bottleneck becomes specification completeness, then the cost of formalizing requirements may come to dominate the software life cycle, so the economic case for spec2code will hinge on whether spec-writing effort is smaller than the coding effort it replaces.","The same verification-backed loop could transfer to other safety-critical domains (e.g., avionics, medical devices) by swapping Frama-C for an equivalent deductive verifier, since the framework does not depend on automotive-specific features.","Because equivalence checking against the original code failed in every case, the paper's 'formally correct' means 'correct with respect to the hand-derived ACSL contract,' not 'behaviorally identical to the original module'; a stronger test would compare against a second, independently written specification.","The pass@1 evaluation under temperature 0.8 likely understates what the pipeline could achieve: sampling several candidates and verifying each would probably raise the success rate, which the paper notes as future work with pass@k."],"forward_implications":["If one-shot, specification-only generation can be formally verified on small modules, the same pipeline is a candidate for larger modules once iterative backprompting and fine-tuning are added, which the paper explicitly plans as future work.","The success of the minimalist instantiation depends on the completeness of the ACSL specifications; the paper concludes that complete specifications are rare in real industrial development, so the practical gain of LLM-based coding must be weighed against the extra effort of writing complete specs.","High-level natural-language specifications alone produced the weakest verification results, indicating that formal or low-level specifications are needed for reliable code generation.","Because all generated programs passed the 'power of 10' rules and compiled with no warnings, the approach is at least compatible with the coding standards used in safety-critical automotive software."],"supporting_citations":[{"why":"Defines the LLM-Modulo framework that spec2code adapts, supplying the core idea of coupling an LLM with external critics.","marker":"[17]"},{"why":"Frama-C is the deductive verification tool used as critic to check generated C code against ACSL specifications.","marker":"[7]"},{"why":"ACSL is the formal specification language in which the contracts and ghost-variable annotations are written.","marker":"[4]"},{"why":"Zero-shot-CoT prompting ('Let's think step by step') is the prompting strategy on which the system and user prompt template is based.","marker":"[19]"},{"why":"Introduces pass@1, the metric used to report first-attempt code-generation performance.","marker":"[5]"},{"why":"diffkemp is the program equivalence tool used to compare generated code with the reference programs.","marker":"[22]"},{"why":"'The power of 10' rules are the safety-critical coding standard against which generated code quality is judged.","marker":"[14]"},{"why":"Provides the Power Steering Backup module and its specifications, reused and modified as case study STEE.","marker":"[34]"}],"fun_headline_variants":["Zero-shot LLM turns specs into formally proven car code","No backprompting, no tuning: LLM specs-to-code passes proof","Spec-only prompt yields verified automotive C, says Scania study","LLM + formal check: verified C code from specs, no fine-tune","One-pass generation: formally verified embedded C from specs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The central claim depends on the assumption that the hand-written ACSL specifications fully and faithfully capture what the original Scania modules are supposed to do, since the formal verification only proves the generated code against those specifications, not against the original code's intent.","fun_headline_variants_meta":{"raw":{"variants":["Zero-shot LLM turns specs into formally proven car code","No backprompting, no tuning: LLM specs-to-code passes proof","Spec-only prompt yields verified automotive C, says Scania study","LLM + formal check: verified C code from specs, no fine-tune","One-pass generation: formally verified embedded C from specs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000318,"raw_usage":{"total_tokens":1791,"prompt_tokens":934,"completion_tokens":857,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":550,"completion_tokens_details":{"reasoning_tokens":766}},"tokens_in":550,"tokens_out":857,"duration_ms":8520,"temperature":1.0,"reasoning_tokens":766,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T16:37:26.649478+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Have a second engineer independently translate the natural-language requirements of the three modules into ACSL specifications without seeing the original code or the paper's contracts, then rerun the same prompts; if any of the newly generated programs fails to compile or fails Frama-C verification, the original verified results were carried by the particular hand-written specifications rather than by the method itself.","supporting_citations":[{"cited_title":"CEA LIST, Inria, http:// frama-c.com/download/frama-c-user-manual.pdf","cited_arxiv_id":null,"evidence_quote":"Frama-C is the deductive verification tool used as critic to check generated C code against ACSL specifications."},{"cited_title":"URL https://frama-c","cited_arxiv_id":null,"evidence_quote":"ACSL is the formal specification language in which the contracts and ghost-variable annotations are written."},{"cited_title":"In: 2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST)","cited_arxiv_id":null,"evidence_quote":"diffkemp is the program equivalence tool used to compare generated code with the reference programs."},{"cited_title":"Com- puter 39(6), 95–99 (2006)","cited_arxiv_id":null,"evidence_quote":"'The power of 10' rules are the safety-critical coding standard against which generated code quality is judged."},{"cited_title":"In: Accepted at 2024 IEEE 32nd International Requirements Engineering Conference (RE)","cited_arxiv_id":null,"evidence_quote":"Provides the Power Steering Backup module and its specifications, reused and modified as case study STEE."}],"review_version":1}