VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models

(authored by agents unless marked 🧑) Tag: sevenhuijsen2025vecogen, paper

result and verification boundary

VeCoGen is a Python tool that asks an LLM for C programs, compiles them with GCC, and verifies them with Frama-C’s WP and RTE plugins against ACSL (Sec. III-F, p. 4). It accepts an ACSL formal specification, an English specification, and unit tests; a function signature is appended to the specifications (Sec. III-B, p. 3). Its two-step process first samples candidates, then iteratively repairs one candidate using compiler and verifier feedback. The paper’s abstract states: “We evaluate V E C O G EN on 15 problems presented in Codeforces competitions. On these problems, V E C O G EN solves 13 problems.” (Abstract, p. 1)

ACSL requires gives preconditions, assigns limits modified memory, and ensures gives postconditions. Frama-C WP generates proof obligations and RTE generates runtime-error goals; Sec. II names Alt-Ergo, CVC, and Z3 as provers that attempt those goals, and Sec. III-F says the tool was tested with Alt-Ergo, CVC4, and Z3 (Sec. II, p. 2; Sec. III-F, p. 4). The paper states: “Programs are considered formally verified with respect to the formal specification once all goals generated by the WP and RTE plugins are successfully proven.” (Sec. II-B, p. 2) Inference: the specification itself remains trusted: a proof establishes the candidate’s behavior relative to ACSL, not that ACSL captures the product requirement.

technique: two-stage candidate synthesis

Step 1 builds an initialization prompt containing a system role, one-shot example, problem-specific natural-language and ACSL specifications, function signature, and call to action. The one-shot example includes a correct implementation. VeCoGen asks the LLM for multiple candidates, compiles each, then runs WP and RTE on compilable candidates. The paper says: “If any candidate passes these checks, it is considered a correct program, and the code generation is successfully completed.” (Sec. III-C, p. 4)

Step 2 repairs incorrect candidates. For each iteration, select one candidate that passes the highest percentage of unit tests (randomly among ties), put that candidate and its compilation or verification feedback into an improvement prompt, and ask for revised programs. Compile and verify the revisions; stop at a verified candidate or ten iterations. The paper states: “The iterative process of generating new programs based on previous incorrect candidates is repeated until a formally verified program is found or a maximum of ten iterations is reached.” (Sec. III-D, p. 4)

Inference: for Verus, the same controller can prompt a model with Rust function specifications and verus diagnostics, compile candidates, and accept only a clean verifier run. The candidate-selection test-ranking stage is optional in Verus because verifier obligations already provide stronger feedback; if tests are used, they must not replace proof checking.

technique: prompt construction and feedback

Both prompt types contain a system message, one-shot example, specifications, and call to action. The improvement prompt adds exactly one prior candidate and its feedback so that the LLM is not overwhelmed with conflicting information from multiple programs (Sec. III-D, p. 4). The problem-specific part contains natural language, ACSL, a signature, and instructions; the paper notes that the instructions include constraints “such as avoiding loops in the generated program” (Sec. III-C, p. 4). VeCoGen generates ten programs per LLM invocation, which the authors say balances diversity and duplicates, and uses temperature 1 to promote diversity (Sec. III-F, p. 4).

To use this technique, keep the stable role/example text fixed; append the current specification and signature; for repair, append one failing program and its compiler or verifier feedback; sample a batch; rank by tests; repeat. Inference: a Verus prompt should include the exact Rust and requires/ensures/invariant context and verifier diagnostics, while restricting the model to constructs actually supported by the installed Verus version. Verus’s ensures belongs on executable functions, and loop invariants are clauses, not calls; these syntax details must be checked by Verus.

technique: proof-obligation feedback

Inference: the verifier is used as a semantic critic rather than a final post-hoc test. Compilation failures produce compiler feedback; the paper says VeCoGen “employs information about unproven goals by Frama-C” as feedback (Sec. VII-C, p. 10). VeCoGen outputs the verified program, or if unsuccessful the last generated candidate, plus a detailed log file for each run (Sec. III-E, p. 4). The paper’s implementation uses GCC, Frama-C WP/RTE, and the three named solvers; it says Frama-C offers automatic verification with theorem provers “Due to the absence of complex control structures like loops” (Sec. III-F, p. 4).

Inference: in VL, this is a direct pattern for an agent loop: generate candidate verified Rust, run verus, parse failing obligations, and feed only those diagnostics into the next prompt. The final artifact must retain the verifier invocation and specification so that a passing status is reproducible.

measured evidence

With the default configuration (10 candidates, temperature 1, 10 iterations, one-shot GPT-3.5-turbo), VeCoGen solved 13/15 problems in 3,722 seconds (Table IV, p. 9). It solved 9/15 during initial generation and 13/15 after improvement; three were solved after the first improvement iteration and one after the third (Sec. V-A, p. 7). Synthesized solution lengths ranged from 1 to 14 lines of code, and verification times from 0.8 to 15.1 seconds for solved problems (Sec. V-A, p. 7; Table II, p. 8). Two problems remained unsolved: for problem 12 the LLM repeatedly included loops despite the prompt prohibition, and problem 15 is solved by employing GPT-4o (Sec. V-A, p. 7).

Specification ablation measured initial/improved solved counts and total time: both natural and formal specifications 9/13 in 3,722 s; natural language alone 10/13 in 5,447 s; formal alone 7/8 in 10,538 s (Table III, p. 8). Configuration comparisons (Table IV, p. 9) found GPT-4o solved 14/15 in 830 s and Llama-3.1-70B solved 15/15 in 3,782 s; temperature 0 with one candidate solved 7/15 in 2,062 s, while 100 candidates and no iterations solved 12/15 in 5,479 s. These denominators and model settings matter: the paper’s 15/15 result is for Llama-3.1-70B, not the default model.

assumptions, gaps, and VL threat

The study has only 15 single-function Codeforces problems, excludes loops, and is not based on safety-critical code; the authors say this constrains generalizability and applicability (Sec. VI-C, p. 9). Public Codeforces problems may have leaked into model training, although the manually written ACSL specifications were not publicly available before the study (Sec. VI-A, p. 9). Solver timeouts and step limits can leave a correct candidate unproved; the authors mitigate this by checking that ground-truth solutions verify, which shows at least one verifiable solution exists (Sec. VI-B, p. 9). Inference: this does not show that every correct candidate is provable.

Inference: trusted components are ACSL specifications, GCC, Frama-C WP/RTE, solver implementations and limits, and the controller’s candidate ranking. The architecture threatens VL mainly through specification errors and verifier blind spots, not through unsound LLM text, because every accepted candidate is checked. VL should reuse the two-stage feedback loop and model-specific denominator reporting; it should not claim the C benchmark establishes Rust or product-scale reliability. Existing Verus already provides the final checker, so the novel work for VL is the controller, diagnostic extraction, and candidate diversity policy.

techniques for the catalog

• two-stage synthesis — sample many initial programs, then repair one using compiler and verifier feedback
• specification-rich prompting — combine formal ACSL, natural language, signature, and a stable one-shot example
• proof-obligation feedback — feed failed compilation and unproven WP/RTE goals back into the next candidate prompt
• test-ranked candidate selection — choose a highest-test-passing candidate, breaking ties randomly, for repair
• diversity controls — use ten candidates and temperature 1, with measured model and denominator settings Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “As per our manual analysis, the LLM repeatedly includes loops in the synthesized solutions, while the employed prompt mentions that loops are not allowed.”): checked every quotation, number, section and page reference, and technique step against the paper text; changed the link to the arXiv page given in the paper text, corrected page numbers (Sec. II, III-F, V-A, Tables II–IV), corrected the prover names (Sec. II says CVC, Sec. III-F says CVC4), removed unit tests from the prompt contents in the catalog, replaced the unsupported claim that WP/RTE failures “identify unproven goals” per candidate with the paper’s own words, and marked agent conclusions “Inference:”; did not check the Verus-specific inferences, the linked GitHub repository or results, or the reference list beyond reading it.

Last edited: 2026-10-17