VeriGen-C improves verified C code generation with aligned specifications
From Natural Language to Verified C: Verification-Guided Generation with ACSL Specifications
Software Engineering
Summary
Generating computer programs from natural language is useful but often creates code that is hard to prove correct automatically. The authors present a system called VeriGen-C that produces both C code and detailed correctness specifications together, making it easier to verify the software’s behavior. Their approach ensures the code and its specification fit well for verification tools to check, increasing the number of programs that pass formal correctness checks. Tests on several benchmarks show VeriGen-C verifies significantly more solutions than previous methods.
What this means in practice
- •For software developers: Generate verified C code with machine-checkable correctness guarantees from natural language requirements to improve software reliability.
- •For software verification engineers: Use jointly synthesized code and ACSL specifications that align closely to automate and accelerate formal verification workflows.
Authors
Zian Wang, Qin Li, Weisong Sun, Haibin Cai
Abstract
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.