PaperlayerView exact revision on arXiv

Source-linked AI summary

From Natural Language to Verified C: Verification-Guided Generation with ACSL Specifications

Zian Wang, Qin Li, Weisong Sun, Haibin Cai

arXiv:2610.30725v1cs.SE

TL;DR

Generated C must be not only executable but formally verifiable against specifications that preserve the natural-language requirement, while separate code and specification generation does not explicitly co-design them for verification. VeriGen-C jointly generates C and ACSL around shared proof anchors, routes repair using verifier evidence, and checks requirement alignment. Across three benchmarks, it improves WP-verified, requirement-aligned success over an interface-compatible baseline.

  • Problem

    C verification must establish conformance to ACSL, but independently generated code and specifications may lack shared proof anchors or preserve too little requirement content.

    Source: §I · pp. 1–2

  • Method

    VeriGen-C jointly generates C and ACSL around shared proof anchors, routes bounded repair using WP outcomes, and checks requirement alignment after verification.

    Source: §I · p. 2, §III · p. 4, C. Requirement-Alignment Check · p. 6

  • Results

    WP-verified, requirement-aligned success rose from 5.5% to 44.5% on HumanEval-X, 44.3% to 80.0% on FM-Bench, and 6.5% to 58.7% on LiveCodeBench Lite versus an interface-compatible one-shot baseline.

    Source: §I · p. 2

  • Takeaways & Limitations

    Across the three benchmarks, verification knowledge and diagnosis-routed repair help preserve requirement alignment, while backend choice shifts proof, alignment, and cost trade-offs.

    Source: §VI · p. 11

    The results are bounded by Frama-C/WP’s automatic proof capabilities and function-level benchmarks, limiting claims about larger systems, concurrency, floating-point kernels, complex heap manipulation, and interactive I/O.

    Source: §V · pp. 10–11

Abstract

from arXiv · show

AI-assisted code generation amplifies the demand for automated formal verification. Generated programs must not only be executable but also accompanied by machine-checkable evidence of correctness. Existing approaches can synthesize functionally plausible code or plausible-looking specifications from natural-language prompts; however, they do not explicitly co-design the implementation and specification as a unified artifact optimized for verification. Consequently, automated verifiers often fail to discharge proof obligations. Typical failure modes include missing or implicit proof anchors, program structures that are hostile to automated reasoning, and inconsistencies between code-level state and specification-level requirement facts arising from the independent generation of code and specifications. Even when verification succeeds, it may only establish weak specifications that omit requirement-critical behavior. This paper introduces VeriGen-C, a formal-verification-friendly framework for the joint synthesis of C programs and ACSL specifications from natural-language requirements. Code generation and repair are constrained to expose proof-relevant state, to streamline control flow for deductive verification, and to eliminate implementation patterns that hinder automated proof search. Specification generation and refinement are similarly constrained to mitigate verification timeouts and to ensure alignment with the user requirements. Empirical evaluations on HumanEval-X, FM-Bench, and LiveCodeBench Lite demonstrate that VeriGen-C substantially improves the rate of verified and requirement-aligned solutions relative to an interface-compatible baseline, from 5.5% to 44.5%, from 44.3% to 80.0%, and from 6.5% to 58.7%, respectively.

I. INTRODUCTION

Formal verification of generated C requires a jointly suitable implementation and ACSL specification, yet existing approaches typically generate them separately. VeriGen-C co-designs both around shared proof anchors and checks that verified specifications remain requirement-aligned.

I. INTRODUCTION

  • Formal verification of C targets a composite C/ACSL artifact, which can be unverifiable or verified against a too-weak specification if either component is unsuitable.AI-generated redundant or proof-irrelevant structures can also create superfluous proof obligations and degrade tool performance.Source: §I · p. 1
  • In the first-index example, pointer arithmetic and an early return time out, while a missing invariant prevents proving firstness; a shared processed-prefix anchor lets the verifier discharge all obligations.The coupled implementation and specification expose the state and bridge properties needed for proof.Source: §I · p. 2
  • VeriGen-C jointly generates C and ACSL, uses verifier outcomes to route bounded repair, and checks conformance and non-vacuous requirement content.Its shared proof-anchor interface links exposed implementation state, contract clauses, and repair.Source: §I · p. 2
  • 44.5% vs. 5.5%, 80.0% vs. 44.3%, and 58.7% vs. 6.5% WP-verified, requirement-aligned success for VeriGen-C versus the baseline on HumanEval-X, FM-Bench, and LiveCodeBench Lite, respectively.The evaluation was conducted without manual post-editing.Source: §I · p. 2

A. C/ACSL Verification Background

C/ACSL verification establishes conformance to a specification, so proof depends on the relationship between the implementation’s exposed state and the contract. VeriGen-C frames generation as a coupled code-and-specification task organized around proof anchors.

A. C/ACSL Verification Background

  • Frama-C/WP computes verification conditions from C implementations and ACSL annotations, then attempts to discharge them with automated theorem provers.A successful analysis establishes that the implementation satisfies the given ACSL specification under the chosen configuration.Source: A. C/ACSL Verification Background · p. 3
  • Verification is specification-relative: code must expose proof-relevant state, and specifications must align with control flow, memory footprint, and intermediate states.Obscured anchors or unsupported contract properties can cause WP verification to fail even when intended behavior is simple.Source: A. C/ACSL Verification Background · p. 3
  • A proof anchor is named, observable program state that both loop invariants and function contracts can reference.In the first-index example, i anchors the processed prefix and res the returned witness.Source: A. C/ACSL Verification Background · p. 3

B. Problem Formulation

The paper formulates natural-language-to-verified-C generation as producing a C implementation and ACSL specification that pass verification while preserving requirement content. It positions this task as distinct from formalizing requirements, annotating existing programs, or repairing proofs in other settings.

B. Problem Formulation

  • The input is a natural-language requirement, and the intended output is C code with an ACSL specification that can be statically verified while preserving substantive requirement content.The output pair is treated as one annotated program.Source: B. Problem Formulation · p. 3
  • The automated generation procedure runs under a bounded repair budget and terminates without human intervention on the generated artifact.Its output includes the C+ACSL artifact, WP outcome, and requirement-alignment report.Source: B. Problem Formulation · p. 3
  • The success criterion requires both a passing WP result and an accepted requirement-alignment report, making it stricter than code generation or WP success alone.The verified specification must preserve non-trivial content from the original requirement.Source: B. Problem Formulation · p. 3

C. Related Work

  • Table I distinguishes artifact-generation problem formulations by primary artifact and formal verification’s role, rather than ranking systems across heterogeneous settings.The paper characterizes VeriGen-C as coupling implementation, ACSL, verifier feedback, and alignment evidence.Source: C. Related Work · p. 3, Table I · p. 4
  • Requirement-formalization work includes consistency checking and translations into models or formal statements, but typically does not produce executable C, ACSL contracts, and Frama-C/WP proofs end to end.Source: C. Related Work · p. 3
  • Specification-generation systems such as SpecGen, AutoSpec, and NL2ACSL address existing programs or formal targets, whereas VeriGen-C co-designs implementation structure and ACSL before an implementation exists.Source: C. Related Work · p. 3
  • Verifier-in-the-loop work uses automated feedback for proof generation or repair; VeriGen-C applies that principle to jointly generated C/ACSL artifacts whose code and contracts can be revised together.Related efforts also address verification and specification synthesis for existing infrastructures.Source: C. Related Work · pp. 3–4

III. METHODOLOGY

VeriGen-C jointly constructs C code and ACSL specifications around proof-relevant state, then verifies and refines the coupled artifact. Its bounded workflow combines verification-knowledge constraints with deterministic control and requirement-alignment checking.

III. METHODOLOGY

  • VeriGen-C treats code, ACSL, verifier feedback, and alignment evidence as coupled parts of a bounded workflow that returns the artifact, WP report, and alignment decision.Passing artifacts proceed to alignment checking; non-passing artifacts are repaired until the budget is depleted or a terminal failure occurs.Source: §III · p. 4

A. Verification-Knowledge-Guided Joint Construction

  • Verification-knowledge policies jointly constrain C implementation and ACSL specification before repair, and ablations test the effect of removing those policies.The implementation exposes proof anchors, while the specification expresses requirement-bearing behavior through those anchors using supported, automation-friendly forms.Source: A. Verification-Knowledge-Guided Joint… · p. 4

1) Verifier-Aware Implementation Guidance:

  • Explicit bounds, named counters or witnesses, state flags, monotonic loops, and low-aliasing updates expose anchors for loop invariants and contracts.These choices avoid reconstructing behavior from complex expressions, pointer offsets, or repeated library calls.Source: 1) Verifier-Aware Implementation… · p. 4

2) Proof-Oriented Specification Guidance:

  • Loop annotations supply induction facts over exposed anchors, while function contracts state observable requirement behavior through parameters, globals, \result, and output buffers.ACSL normalization canonicalizes annotations and routes unsupported helper definitions to repair while preserving requirement content.Source: 2) Proof-Oriented Specification Guidance · pp. 4–5

B. Diagnosis-Routed Verification Repair

VeriGen-C diagnoses non-pass WP outcomes and routes bounded repair to the specification, the coupled code and specification, or terminal failure. Joint repair is conservative and requires prior specification-only attempts plus evidence that implementation shape blocks proof.

B. Diagnosis-Routed Verification Repair

  • Non-pass outcomes can reflect annotation form, missing proof bridges, or implementation structure, so diagnosis and routing aim to preserve alignment between program state and contract clauses.Filtered verifier output and failure categories guide specification repair, joint repair, or termination.Source: B. Diagnosis-Routed Verification Repair · p. 5

1) Diagnosis Knowledge Policy:

  • Invalid ACSL routes to specification repair, while joint repair becomes eligible only after minimum specification-only attempts and persistent evidence that implementation shape blocks proof.Deterministic failure categories and routing guards remain authoritative even when diagnosis summarizes root causes and targets.Source: 1) Diagnosis Knowledge Policy · p. 5

2) Diagnosis-Conditioned Specification Repair:

  • Specification repair keeps the implementation fixed, repairing invalid annotations or targeting failing proof obligations through loop facts, frames, postconditions, and quantifier-heavy claims.When a semantic clause is too strong, repair reshapes it around implementation-exposed anchors while preserving requirement-bearing content; success also requires WP passage and alignment acceptance.Source: 2) Diagnosis-Conditioned Specification… · pp. 5–6
  • Joint repair may change code and ACSL only after specification-only attempts and code-shape evidence, targeting hidden witnesses, repeated library calls, unbounded scans, or break-heavy control flow.Each repair is followed by extraction, ACSL normalization, and recording of the updated artifact and verifier evidence.Source: 2) Diagnosis-Conditioned Specification… · p. 6

C. Requirement-Alignment Check

The requirement-alignment check prevents WP passage alone from counting as success when the proved contract lacks task-specific behavior. It classifies contract coverage and rejects shell-only, inconsistent, or unclear specifications.

C. Requirement-Alignment Check

  • WP success is specification-relative, so the alignment check rejects contracts containing only safety, frame, nullability, range, or shape clauses without task-specific functional ensures.A contract has non-trivial requirement-bearing behavior when a functional clause relates an observable output to a stated input condition.Source: C. Requirement-Alignment Check · p. 6
  • Accepted alignment buckets are slice for at least one branch or direction, core for the main input–output relation, and full for all stated task-specific properties.The checker returns an outcome bucket, clause-level coverage evidence, detected mismatches, and a textual explanation.Source: C. Requirement-Alignment Check · p. 6
  • Alignment prescreens contracts, maps requirement clauses to covered, missing, contradictory, or ambiguous records, and applies deterministic rules to assign an outcome bucket.Frama-C/WP establishes proof; the checker determines whether the proved contract retains task-specific content, and rejected artifacts remain outside the repair loop.Source: C. Requirement-Alignment Check · p. 6

IV. EVALUATION

The evaluation measures both whether Frama-C/WP proves generated C+ACSL artifacts and whether their contracts preserve non-trivial requirement behavior. It uses fixed workflow and verifier settings across three benchmark datasets.

IV. EVALUATION

  • The evaluation distinguishes proof reachability from requirement alignment because WP proves conformance to generated ACSL, not directly to the original natural-language requirement.WP-passing artifacts count as useful only when the verified contract preserves meaningful requirement intent.Source: §IV · p. 6
  • The research questions cover overall effectiveness, verification-knowledge guidance, diagnosis-routed repair, and model sensitivity and cost.The workflow comparisons isolate guidance and repair components, while the model-sensitivity analysis varies the backend.Source: §IV · p. 6

A. Experimental Setup

  • All methods share the task interface, verifier configuration, alignment checker, execution protocol, and GPT-5.4 at temperature 0.0 for the main comparisons.WP uses Alt-Ergo and Z3 with an 8-second timeout per obligation; the repair budget allows up to five specification-only and, when eligible, three joint attempts.Source: A. Experimental Setup · pp. 6–7

B. Datasets

  • HumanEval-X contributes 164 normalized C++ prompts, FM-Bench retains 70 of 90 function-level records, and LiveCodeBench Lite retains 201 of 342 tasks.The pre-specified filter excludes tasks outside the function-level C/ACSL setting, with source IDs and exclusion reasons recorded.Source: B. Datasets · p. 7

C. Metrics

The evaluation reports both WP reachability and the stricter rate of tasks whose final artifacts pass WP and retain non-vacuous requirement content. The requirement-alignment checker is audited against WP-passing artifacts for coverage and agreement.

C. Metrics

  • WP-verified requirement-aligned success counts tasks that pass WP and whose final artifacts meet accepted requirement-content buckets; it does not measure complete requirement formalization.Accepted buckets are slice, core, and full; WP reachability is reported separately.Source: C. Metrics · p. 7

D. Validation of the Requirement-Alignment Check

  • The checker covered all 298 WP-passing main-run artifacts and produced clause-level reports auditable against each source requirement.One experienced C/ACSL auditor labeled the artifacts without seeing checker outputs.Source: D. Validation of the… · p. 8
  • Auditor and checker agreed on 289/298 category labels (97.0%, κ = 0.96) and 290/298 accept/reject decisions (97.3%, κ = 0.91).Disagreements included four contradictory contracts accepted by the checker and four slice-level contracts rejected.Source: D. Validation of the… · p. 8
  • The audit used a single expert auditor, so κ measures auditor–checker agreement; 51 rejected WP-passing artifacts illustrate why WP success alone could over-count weak contracts.The authors support using the checker as an evaluation filter based on its coverage, auditability, and manual-audit stability.Source: D. Validation of the… · p. 8

E. Experimental Results

VeriGen-C improves WP-verified, requirement-aligned success over an interface-compatible one-shot baseline on all three benchmarks. Ablations show that verification guidance and diagnosis-routed repair help preserve requirement-bearing contracts, while model choice shifts quality and cost trade-offs.

RQ1: Overall Effectiveness

  • 5.5% to 44.5% on HumanEval-X, 44.3% to 80.0% on FM-Bench, and 6.5% to 58.7% on LiveCodeBench Lite for WP-verified requirement-aligned success with VeriGen-C versus one-shot.The comparison used the same task interface, base model, verifier configuration, and requirement-alignment checker.Source: Table IV · p. 8, E. Experimental Results · p. 8
  • The one-shot baseline ends with front-end invalid outcomes on 142/164 HumanEval-X, 33/70 FM-Bench, and 132/201 LiveCodeBench Lite tasks; VeriGen-C obtains 53, 13, and 89 WP passes after repair.On HumanEval-X, 95 artifacts pass WP but only 73 are accepted after requirement-alignment checking.Source: E. Experimental Results · p. 8

RQ2: Effect of Verification Knowledge Guidance

  • VeriGen-C exceeds No-KG in success by 31.1, 35.7, and 33.8 percentage points on HumanEval-X, FM-Bench, and LiveCodeBench Lite, respectively.Removing guidance increased shell-only WP artifacts from 9.5% to 37.8%, 0.0% to 19.0%, and 5.6% to 27.9% on those benchmarks.Source: E. Experimental Results · p. 9

RQ3: Effect of Diagnosis and Routed Repair

  • Diagnosis and routed repair yield larger Success-rate than WP-rate gaps over No-diagnose: 20.7, 67.1, and 31.8 percentage points across the three datasets.No-diagnose produced shell-only WP artifacts at 45.0%, 79.3%, and 45.3%; on FM-Bench, only 9 of its 58 WP-passing artifacts remained requirement-aligned.Source: E. Experimental Results · p. 9, Table VI · p. 10

RQ4: Model Sensitivity and Cost

  • GPT-5.4 versus GPT-4.1 raises HumanEval-X WP pass rate from 47.0% to 57.9% and Success Rate from 32.3% to 44.5%, with comparable token use.Across providers, Gemini has the highest WP pass rate (75.6%) and most Success cases (77), but a 37.9% shell-only WP share; DeepSeek has the highest token use.Source: Table VII · p. 10, E. Experimental Results · p. 10

V. DISCUSSION

VeriGen-C’s results depend on the joint interface among C, ACSL, and Frama-C/WP: artifacts must expose proof-oriented state while retaining requirement-level content. The discussion also bounds the findings to automated proof and function-level tasks, and treats requirement-alignment acceptance as a filter rather than a formal equivalence proof.

Implications

  • Natural-language-to-verified-C generation depends on the joint C, ACSL, and Frama-C/WP interface; staging alone is insufficient, as the No-KG control shows.Successful artifacts must be valid C/ACSL, expose proof-oriented state, use verifier-supported annotations, and retain requirement-level specification content.Source: §V · p. 10

Repair

  • Diagnosis-routed repair separates specification refinement from joint code–specification revision, escalating only when verifier evidence indicates code-shape blockers.RQ3 shows repair improves verified-code generation only when constrained not to erase functional contract content.Source: §V · p. 10

Interpreting WP-verified requirement-aligned success

  • WP success establishes satisfaction of the generated contract, not full formalization of natural language; accepted artifacts are non-vacuous specification slices.The alignment checker rejects shell-only and inconsistent contracts, but acceptance is not mechanically proved equivalence.Source: §V · p. 10

Scope

  • Findings are bounded by Frama-C/WP’s automatic proof capability and function-level tasks, limiting claims about larger systems, concurrency, floating-point kernels, and complex heap code.Model choice can change proof reachability, requirement alignment, and cost; the framework is positioned as offline verified-code generation.Source: §V · pp. 10–11

Construct validity

  • Requirement-alignment acceptance may miss subtle omissions or penalize conservative contracts, and the manual audit was conducted by a single auditor.The checker is an evaluation filter, not a mechanically proved equivalence between natural language and ACSL.Source: §V · p. 11

Model and reproducibility validity

  • The main experiments use one default model, while sensitivity results cover only backends with complete local outputs; provider updates and decoding behavior may affect future runs.The study mitigates reproducibility risks by fixing verifier settings and preserving run artifacts and alignment evidence.Source: §V · p. 11

VI. CONCLUSION

The conclusion frames natural-language-to-verified-C generation as a joint code–specification problem requiring both proof reachability and requirement alignment. VeriGen-C improves verified, requirement-aligned success across three benchmarks, while ablations highlight verification knowledge and diagnosis-routed repair as helpful to alignment.

VI. CONCLUSION

  • VeriGen-C substantially improves WP-verified requirement-aligned success over one-shot C+ACSL generation across HumanEval-X, FM-Bench, and LiveCodeBench Lite.The conclusion reports the cross-benchmark pattern without listing individual percentages.Source: §VI · p. 11
  • Ablations indicate that verification knowledge and diagnosis-routed repair help preserve requirement alignment, while backend choice shifts proof, alignment, and cost trade-offs.The model-sensitivity study finds backend choice does not replace the framework.Source: §VI · p. 11
Loading 2610.30725v1…