PaperlayerView exact revision on arXiv

Source-linked AI summary

Self-Spec Verifiable Code Generation

Jiaru Qian, Yihong Dong, Yongmin Li, Hao Zhu, Bin Gu, Ge Li

arXiv:2609.39568v1cs.SEcs.AI

TL;DR

Existing evaluations often separate specification and code generation or focus on mathematical tasks, leaving end-to-end capability in developer-facing settings less covered. VeriCodeBench evaluates a self-spec pipeline across four languages, while CodeNova combines constraint-guided specification and verifier-guided repair. The findings identify specification quality as a bottleneck and report that CodeNova improves aggregate joint success.

  • Problem

    Existing evaluations often separate specification from code generation under oracle specifications and focus on proof-oriented mathematical tasks, leaving end-to-end and developer-facing settings less covered.

    Source: §1 · p. 2

  • Method

    VeriCodeBench evaluates self-generated specifications and code across four native language tracks, while CodeNova combines constraint-guided specification with verifier-guided candidate repair.

    Source: §1 · p. 2

  • Results

    CodeNova improves aggregate joint success, while specification quality remains a bottleneck for end-to-end success.

    Source: §5 · p. 10

  • Takeaways & Limitations

    The findings motivate advancing faithful requirement formalization alongside implementation and proof generation.

    Source: §5 · p. 10

    Even with verifier-guided repair, CodeNova using self-generated specifications remains 12.4 percentage points below the oracle setting in aggregate validity.

    Source: §4.3 · p. 9

Abstract

from arXiv · show

Large language models (LLMs) may generate unreliable code on corner cases missed by testing, while formal verification can provide machine-checkable guarantees. Recently, researchers have proposed several benchmarks to evaluate the capabilities of LLMs in generating formally verifiable code, where LLMs need to formulate formal specifications, generate the corresponding code, and verify its correctness. However, existing benchmarks have two key limitations: (I) They primarily evaluate specification and code generation stage-wise, with code generation typically conditioned on an oracle specification. This setup overlooks whether strong stage-wise performance translates into end-to-end success. (II)They mainly focus on a single proof-oriented language and mathematically structured tasks, offering limited coverage of tasks common in software development. In this paper, we introduce VeriCodeBench, a benchmark for self-spec verifiable code generation, where the LLM relies solely on its own generated specification and code throughout the entire process. VeriCodeBench contains 400 language-native problems across C, Java, Rust, and Python, covering practical concerns in software development. We evaluate specification coverage, code validity, and joint problem-level success. We further introduce CodeNova to enhance the capabilities of LLMs in self-spec verifiable code generation. CodeNova makes requirements explicit through constraint-guided specification and uses verifier feedback to guide targeted implementation repairs. Experimental results reveal that self-generated specifications remain a major bottleneck, while providing more sophisticated specifications may not necessarily lead to higher verification success rates. CodeNova substantially improves performance across all evaluation metrics, enabling Claude Sonnet 5 to achieve the strongest results under the self-spec protocol.

1 INTRODUCTION

The paper argues that stage-wise evaluations and narrow formal-language task distributions leave key gaps in assessing verifiable code generation. It introduces a multilingual self-spec benchmark and CodeNova, an approach combining requirement formalization with verifier-guided repair.

1 INTRODUCTION

  • Stage-wise benchmarks do not establish end-to-end capability because generated specifications can change downstream implementation difficulty and proof obligations.A more complete specification may reduce verification success, so the model-generated specification must be carried through the pipeline.Source: §1 · p. 2
  • Existing benchmarks also offer limited exposure to software-development abstractions and failure modes, including pointer validity in C and object mutation and exceptions in Java.Many focus on a single formal ecosystem, proof-oriented languages, and mathematically structured tasks.Source: §1 · p. 2
  • VERICODEBENCH evaluates 400 language-native problems across C, Java, Rust, and Python using specification coverage, validity against the same specification, and joint problem-level success.Its tracks use native verification ecosystems and preserve language-specific syntax, semantics, and proof obligations.Source: §1 · p. 2
  • CodeNova extracts behavioral and safety constraints, formalizes them as specifications, generates code conditioned on them, and uses verifier feedback for focused repairs.It checks specification coverage and repairs unsatisfied proof obligations with the native verifier.Source: §1 · pp. 2–3
  • The paper defines self-spec verifiable code generation as preserving the generated specification through code generation, repair, and verification.This setup evaluates the pipeline using the model's own artifacts rather than an oracle specification.Source: §1 · p. 3

2 RELATED WORK

Related benchmarks and systems address pieces of formal reasoning and verification, but often separate stages or focus on mathematical tasks. The section positions VeriCodeBench and CodeNova as covering the full pipeline in developer-facing language settings.

2.1 BENCHMARKS FOR FORMAL REASONING AND VERIFICATION

  • Mathematical benchmarks such as MiniF2F and ProofNet assess formal reasoning but do not center on executable programs with state and memory obligations.MiniF2F covers competition-level mathematics across formal systems; ProofNet pairs undergraduate problems with informal proofs and Lean statements.Source: §2.1 · p. 3
  • FormalBench, AlgoVeri, CLEVER, and VERINA cover specification inference or verifiable code-generation stages, but primarily use curated formal tasks rather than broad software-development scenarios.VeriCodeBench instead uses a self-spec setting and 400 language-native tasks across C, Java, Rust, and Python.Source: §2.1 · p. 3

2.2 LLM-ASSISTED FORMAL VERIFICATION

  • Prior LLM systems explore specification generation, synthesis, proof generation, and verifier-guided repair, but most focus on individual pipeline stages.CodeNova combines requirement formalization, code generation, and verifier-guided repair in one workflow.Source: §2.2 · p. 3
  • Figure 1 depicts VeriCodeBench jointly measuring requirement coverage and code verification, alongside CodeNova's constraint-guided specification and verifier-guided repair.Both are presented within the self-spec pipeline.Source: Figure 1 · p. 4

3 SELF-SPEC VERIFIABLE CODE GENERATION

The section frames self-spec generation as a coupled specification-and-implementation task, then presents VeriCodeBench’s evaluation design and CodeNova’s generation pipeline.

3.1 PROBLEM FORMULATION

  • The task is a coupled pipeline: a generated specification is assessed for semantic adequacy and constrains downstream implementation generation.Source: §3.1 · p. 4

3.2 VERICODEBENCH

  • VERICODEBENCH operationalizes the task with 400 problems across four language-native tracks and measures specification adequacy, code validity, and joint success.Joint success requires full target coverage and verifier acceptance on the same problem.Source: §3.2 · pp. 4–5, §3.2.2 · p. 5

3.2.1 SELF-SPEC EVALUATION

  • The primary self-spec protocol requires using the model’s generated specification through code generation, repair, and verification; stage-wise evaluation is secondary.Source: §3.2.1 · p. 5

3.2.2 TWO INDEPENDENT CORRECTNESS CONDITION

  • Coverage compares generated specifications with curated targets using deterministic entailment checks; joint success also requires verifier acceptance on that problem.CEF reverses entailment for preconditions to avoid crediting unnecessarily restrictive domains.Source: §3.2.2 · p. 5

3.2.3 FOUR LANGUAGE TRACKS

3.3 CODENOVA

  • CODENOVA combines Constraint-Guided Specification with Verifier-Guided Candidate Repair to generate verified code under a self-generated specification.Source: §3.3 · p. 6

3.3.1 CONSTRAINT-GUIDED SPECIFICATION

  • CGS extracts atomic behavioral and safety constraints, translates them into a specification, reviews omissions, and refines until alignment or its review budget ends.Source: §3.3.1 · p. 7

3.3.2 VERIFIER-GUIDED CANDIDATE REPAIR

  • VGCR converts verifier diagnostics into repair subgoals and checks up to K complete-program candidates per round, returning the first accepted candidate or continuing repair.Source: §3.3.2 · p. 7

4 EXPERIMENTS

The experiments evaluate end-to-end self-spec generation and examine how specification source affects code validity. CODENOVA achieves the highest aggregate joint success among the tested configurations, while oracle-spec comparisons expose the difficulty of self-spec generation.

4.1 EXPERIMENTAL SETUP

  • The evaluation tests four LLMs on 400 problems, using each model for specification, code generation, and subsequent review or repair.Implementations are checked with the native toolchain for each language; failures include syntax or type errors, unproved obligations, verifier errors, and timeouts.Source: §4.1 · pp. 7–8, §4 · p. 7

4.2 END-TO-END SELF-SPEC PERFORMANCE

  • Under Direct, validity averages 71.0% across 16 model–language settings, while joint success is 44.1%; Claude-Sonnet-5 averages 60.3% joint success.The gap shows that verifier acceptance alone does not ensure complete requirement coverage.Source: §4.2 · p. 8
  • CGS raises mean requirement coverage from 0.7162 to 0.7761 and average joint success from 44.1% to 45.6%, though code validity declines in several settings.For Kimi-K2.7-Code on Rust, coverage rises from 0.6965 to 0.7562 while valid implementations drop from 91 to 60.Source: §4.2 · p. 8
  • 49.1% aggregate joint success is CODENOVA’s best result among four configurations; Claude-Sonnet-5 reaches 65.5% across tracks.Combining VGCR with CGS raises validity from 65.6% to 75.7% and joint success from 45.6% to 49.1%.Source: §4.2 · p. 8, Table 3 · p. 8

4.3 ERROR PROPAGATION AND ORACLE-SPEC DIAGNOSTIC

  • Oracle specifications improve code validity in nearly every comparison, but the 12.4-percentage-point aggregate-validity gap is not a direct measure of specification errors.Replacing a self-generated specification changes both the information available and the verification obligations; coverage and verifier acceptance capture different failure modes.Source: §4.3 · pp. 9–10, Table 4 · p. 9

5 CONCLUSION

The paper introduces VERICODEBENCH for evaluating self-spec verifiable code generation across four languages and presents CODENOVA as an approach that improves aggregate joint success. Its findings identify specification quality as a bottleneck and show that repair remains limited by inadequate specifications.

5 CONCLUSION

  • VERICODEBENCH contains 400 self-spec problems across C, Java, Rust, and Python, jointly assessing requirement coverage and native verifier acceptance.The benchmark exposes failures that verification under a generated specification alone can miss.Source: §5 · p. 10
  • CODENOVA combines constraint-guided specification with verifier-guided candidate repair to improve aggregate joint success.The remaining failures highlight the limits of repair when specifications are inadequate.Source: §5 · p. 10
  • The evaluation finds that specification quality affects downstream verification and remains a bottleneck for end-to-end success.The conclusion motivates advancing faithful requirement formalization alongside implementation and proof generation.Source: §5 · p. 10

A.1 DATASET CONSTRUCTION AND QUALITY CONTROL

The benchmark is built from language-native tasks with curated behavioral targets and verified references, then evaluated under a protocol that preserves the dependency between generated specifications and code. Its artifacts and coverage procedure support auditable, reproducible assessment.

A.1 DATASET CONSTRUCTION AND QUALITY CONTROL

  • Each task supplies a natural-language requirement, fixed language-level signature, and any minimal public type context, while target clauses and reference code remain hidden.The fixed signature removes irrelevant interface search while leaving behavioral formalization to the model.Source: §A.1 · p. 12
  • Curators manually define atomic behavioral obligations and use reference specifications to resolve verification-relevant details, making target clauses explicit and auditable.The target set includes proof-oriented conditions only when they belong to the intended specification.Source: §A.1 · p. 12
  • Every task has a manually constructed implementation and full native specification checked with the track’s verifier, establishing realizability under the fixed interface.Reference implementations are not used as candidate answers in model evaluation.Source: §A.1 · p. 12

A.2 DESIGN PRINCIPLES

  • The self-spec protocol freezes the generated specification through code generation and verifier-guided repair, preserving the dependency between specification and implementation.This prevents silently weakening the specification to obtain an easier proof and captures error propagation across the pipeline.Source: §A.2 · pp. 12–13
  • The four tracks use language-native problems and verification idioms, so cross-language differences reflect complete task–toolchain combinations rather than parallel translations.The tracks cover concerns such as C pointer validity, Java object frames, Rust ownership-aware mutation, and Python permission-based reasoning.Source: §A.2 · p. 13

A.3 CONSTRAINT ENTAILMENT DETAILS

  • Coverage and verifier acceptance are recorded separately and combined at problem level, with fixed target denominators and oracle-spec or stage-wise controls.Constraint entailment checks compatible generated clauses against each target through language-specific canonicalization and SMT-based entailment queries.Source: §A.2 · p. 13, §A.3 · p. 13

A.4 BENCHMARK ARTIFACTS

  • The release includes requirements, target obligations, reference specifications and implementations, plus run evidence linking generated artifacts to verifier outcomes and coverage reports.Stored artifacts and diagnostics make failures traceable to specification generation, code generation, preservation, or verification.Source: §A.4 · pp. 13–14

B IMPLEMENTATION DETAILS OF CODENOVA

CODENOVA represents requirements as atomic constraints, translates them into language-native specifications, and iteratively reviews them before implementation generation. It then uses verifier diagnostics to plan and schedule implementation and proof-annotation repairs.

B.1 CONSTRAINT REPRESENTATION AND SPECIFICATION REFINEMENT

  • Atomic constraints separate admissible inputs, return behavior, state changes, and invariants, with language-specific fields for frames, exceptions, mutation, and permissions.The generated constraint set can remain incomplete and is distinct from the curated target set used for coverage scoring.Source: §B.1 · p. 14
  • Specification translation preserves pre/post-state distinctions and adds language-specific guidance, while optional loop invariants and termination measures remain separate from function requirements.Review uses alignment judgments and refinement hints until alignment is reported or the configured budget is reached; budget exhaustion does not establish alignment.Source: §B.1 · p. 14

B.2 REPAIR PLANNING AND CANDIDATE SCHEDULING

  • Verifier-derived repair plans organize failures into subgoals with diagnostic evidence and proposed implementation or annotation changes; these are LLM interpretations, not proved lemmas.A failed or timed-out proof attempt is not treated as a concrete counterexample.Source: §B.2 · p. 14
  • Repair schedules integrate all subgoal hints before prioritizing individual issues, verifies complete candidates, and returns the first accepted candidate or retains the last submitted one.Candidate checks preserve interactions among proof obligations; selection relies on verifier acceptance rather than an LLM score or assumed monotonic progress.Source: §B.2 · pp. 14–15

B.3 CONTROLLED COMPONENT EVALUATION

The controlled evaluation isolates specification-generation and repair effects by pairing runs that reuse the same specification and initial code.

B.3 CONTROLLED COMPONENT EVALUATION

  • Repair comparisons reuse each run’s exact specification and initial code without resampling, isolating repair gains from specification-generation effects.Coverage is identical within each with-repair/without-repair pair.Source: §B.3 · p. 15
  • Direct makes one specification and implementation attempt before a single verification, while full CODENOVA combines specification guidance with repair.CGS retains Direct’s single code attempt; VGCR adds repair under Direct’s saved specification.Source: §B.3 · p. 15
  • The evaluation records extracted constraints, self-check findings, repair plans, candidate focuses, and verifier outcomes for analysis.Source: §B.3 · p. 15

C PASS@k ANALYSIS

The pass@k analysis finds verifier-guided repair generally beneficial, while constraint-guided specifications have conditional effects and higher sampling budgets can reveal remaining headroom. Case studies show that explicit specifications can improve behavioral coverage but can also make verification harder.

C PASS@k ANALYSIS

  • CGS effects vary by track and sampling budget: richer specifications can lower success or raise the attainable level by making intended behavior easier to recover.The passage attributes possible declines to additional proof obligations or a less usable proof interface.Source: C PASS@k ANALYSIS · p. 15
  • VGCR curves generally dominate Direct or approach the same ceiling sooner, and combined CODENOVA recovers cases where CGS alone is harmful while retaining its gains.The passage describes verifier feedback as a way to turn additional samples into targeted repairs.Source: C PASS@k ANALYSIS · p. 15
  • CODENOVA often retains headroom through pass@5, but curve flattening indicates sampling may not remove persistent specification bottlenecks or unrealizable obligations.Language-specific verifier semantics and specification idioms also shape initial success and saturation.Source: C PASS@k ANALYSIS · p. 15

D CASE STUDY

  • The case study selects Claude-Sonnet-5 artifacts to illustrate how constraint extraction and verification-guided repair affect joint success components.Source: D CASE STUDY · p. 15

D.1 CGS CAN REPAIR MISSING BEHAVIORAL COVERAGE

  • Across the reported examples, CGS reaches final coverage of 6/6, 3/3, and 2/2; generated code remains valid, and the decomposition retains verifier acceptance.Source: §D.1 · p. 16

D.2 CGS MAY ALSO MAKE AN ALREADY-VALID PROGRAM HARDER TO PROVE

  • A richer CGS specification can preserve full target coverage yet make an already-valid implementation fail verification through added proof obligations.The examples include a timed-out C frame goal, an unproved Java loop invariant, and a Python disjunctive postcondition failure.Source: §D.2 · pp. 16–17

D.3 VGCR COMPENSATES HARDER SPECIFICATIONS

VGCR repairs implementation-level failures while keeping the CGS specification and its coverage fixed.

D.3 VGCR COMPENSATES HARDER SPECIFICATIONS

  • VGCR turns several CGS-only failures into joint successes by changing implementation details without weakening or changing the specification.Examples include replacing an existential witness with a concrete index, adding exception guards, restoring a required C include, and correcting Rust reference mutability.Source: §D.3 · p. 17

D.4 CODE GENERATION PERFORMANCE IS SENSITIVE TO RECEIVED SPECIFICATION

Specification choice affects downstream code and proof difficulty in both directions: self-generated interfaces can hinder verification, while oracle contracts can impose additional obligations. The paper also describes prompt records for the shared pipeline and its four native language tracks.

D.4 CODE GENERATION PERFORMANCE IS SENSITIVE TO RECEIVED SPECIFICATION

  • Self-generated proof interfaces can prevent verification even when oracle-conditioned artifacts verify, while oracle contracts can also impose obligations that make code generation harder.Examples include a missing loop-frame and arithmetic-range interface, a Verus mutable-reference contract form, and oracle requirements for safe multiplication or modified locals.Source: §D.4 · pp. 17–18
  • Equal validity totals can conceal specification-adequacy gaps: oracle contracts recover four failures but make four previously valid cases fail, while joint success exposes missing coverage.The passage reports an unchanged validity total of 91 and a 34-point joint-success gap for the example comparison.Source: §D.4 · p. 18, Table 5 · p. 18

D.5 TAKEAWAY

  • Across the artifacts, CGS can improve semantic completeness while lowering validity; VGCR targets implementation and proof failures under a frozen contract.The passage distinguishes verifier acceptance from specification adequacy, which joint success evaluates together.Source: §D.5 · p. 18

E PROMPT RECORDS

  • The prompt appendix records the released pipeline’s stages, schemas, runtime fields, frozen-specification boundary, and shared stage order across four native verifier tracks.CGS covers constraint extraction, translation, and self-check/refinement; VGCR covers repair analysis and focused candidates.Source: E PROMPT RECORDS · p. 18

E.1 C / ACSL

  • The C/ACSL prompts separate structured constraint extraction, contract translation, and requirement-alignment checks, with loop annotations kept in code hints.Source: §E.1 · p. 19

E.2 JAVA / JML

  • The Java/JML prompts explicitly cover exceptional behavior and narrow mutation frames, and the self-check rejects renamed fields or widened frames.Source: §E.2 · pp. 19–20

E.3 RUST / VERUS

  • The Rust/Verus prompts include panic freedom and mutation frames, use old/final state for mutable references, and check for dropped return or frame constraints.Source: §E.3 · p. 20

E.4 PYTHON / NAGINI

  • The Python/Nagini prompts cover permissions, exception freedom, and invariants, while self-check preserves mutation facts, None cases, and exception freedom.Source: §E.4 · p. 21
Loading 2609.39568v1…