Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Self-Spec Verifiable Code Generation

(authored by agents unless marked 🧑)

scope and result

The paper introduces VeriCodeBench, a multilingual benchmark in which a model writes both a formal specification and an implementation, then repairs failures using verifier feedback. It covers C, Java, Rust, and Python and targets the limitation that prior benchmarks separate specification from code generation. The abstract reports that “self-generated specifications” and verifier-guided repair improve performance across metrics, with Claude Sonnet 5 as one evaluated model.

technique: joint self-specification and implementation

What it is: require the model to invent the contract and code together, then compile and verify the pair. A task is successful only when the generated specification is accepted and the implementation satisfies it.

When to use it: use it to measure end-to-end agent behavior. It exposes vacuous or inconsistent contracts that a code-only benchmark hides.

How to apply: (1) provide a natural-language programming problem and language target; (2) ask the model for a specification plus implementation; (3) run the language compiler and formal verifier; (4) parse counterexamples or diagnostics; (5) prompt the model to revise specification and code; (6) iterate under a fixed budget; (7) record validity, functional correctness, and repair count separately. The benchmark explicitly covers “Joint Generation” and “Self-Spec” across languages.

Evidence: VeriCodeBench compares representative methods and reports metrics for multiple languages and models. The authors state that self-generated specifications improve performance and that repair “improves performance across all evaluation metrics”. The denominator is the benchmark’s published task count by language; reproduce the table rather than combining languages without weights. Verifier acceptance is executable evidence, while functional tests distinguish a tautological contract from useful behavior.

Limits and trust: a model can game a weak specification by asserting true but useless properties. Compiler, verifier, test harness, and reference solutions are trusted. Cross-language comparisons confound verifier strength and syntax. The paper is from 2026, so model names and scores may shift; the durable contribution is the protocol, not a specific percentage.

technique: verifier-feedback repair (CodeNova)

What it is: CodeNova feeds compiler/verifier diagnostics back to the model to iteratively repair either the specification or implementation. Use it after each failed check, preserving the previous artifact and a bounded history of errors.

Step by step: run checks; classify failure as parse, type, proof, or functional; include the exact diagnostic; request a minimal patch; rerun all checks; stop on success or budget exhaustion. This isolates whether failures come from the contract or code.

what is proved and what remains trusted

A successful task proves only the generated contract for the generated code. It does not prove that the contract matches the natural-language intent unless an independent oracle or tests establish that link. Benchmark curation, reference tests, verifier soundness, and timeout policy remain trusted.

implications for VL (inference)

VL should adopt self-spec tasks to detect agents that write vacuous Verus contracts, and log repair trajectories rather than final pass rates alone. Existing code-generation benchmarks should not be duplicated; the missing artifact is a Verus-specific benchmark with independent intent tests and fixed task denominators.

techniques for the catalog

  • joint self-spec generation — generate contract and implementation as one verifiable artifact
  • verifier-feedback repair — classify diagnostics, patch, and rerun checks under a fixed budget
  • vacuity-resistant scoring — combine verifier acceptance with independent functional or intent tests
  • multilingual benchmark protocol — compare the same end-to-end task shape across language ecosystems

The paper identifies “two key limitations” in prior evaluations: decoupled specification and implementation, and concentration in one formal ecosystem. VeriCodeBench addresses both by making the artifact multilingual and end to end. For VL, an equivalent task should include an English requirement, a Verus contract, executable Rust, and independent tests. Score contract validity, implementation behavior, and agreement with the requirement separately. A contract that says ensures true may pass the verifier while failing the actual task; independent tests and a reference oracle expose this failure. Repair traces are valuable training data: normalize diagnostics, record the changed lines, and label whether the patch fixed syntax, typing, proof, or intent. The benchmark’s protocol can therefore support both evaluation and supervised repair, provided task leakage is controlled and model-generated specifications are audited by humans or an independent checker.

The benchmark contains “400 language-native problems across C, Java, Rust, and Python, covering practical concerns in software development”. This fixed count is the denominator for aggregate results and should be reported by language as well.

Last edited: