Self-Spec Verifiable Code Generation

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

cs.SESep 30, 2026

Self-Spec Verifiable Code Generation

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

Organizations: School of Computer Science, Peking University · Beijing Key Laboratory of Trustworthy Code Large Language Models · Key Laboratory of High Confidence Software Technologies, Peking University, Ministry of Education · aiXcoder · Shanghai Jiao Tong University · Beijing Institute of Control Engineering

Abstract

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.

Figures & tables

Method / Benchmark	Joint Generation	Self-Spec	Multilingual	Language	Size
nl2spec ( Cosler et al., 2023 )	$\times$	$\times$	$\times$	LTL	36
AutoSpec ( Wen et al., 2024 )	$\times$	$\times$	$\times$	C	251
SpecGen ( Ma et al., 2025 )	$\times$	$\times$	$\times$	Java	385
ClassInvGen ( Sun et al., 2025 )	$\times$	$\times$	$\times$	C++	9
PropertyGPT ( Liu et al., 2024 )	$\times$	$\times$	$\times$	Solidity	23
SLD-Spec ( Chen et al., 2025 )	$\times$	$\times$	$\times$	C	62

Table 1: Comparison with representative methods and benchmarks. Joint Generation indicates that a method or benchmark covers both specification and code generation. Self-Spec means that LLM relies solely on its own generated specification rather than an oracle throughout the entire process.

Figure 1: Overview of VeriCodeBench and CodeNova . Left: VeriCodeBench evaluates the self-spec pipeline by jointly measuring whether the generated specification covers the requirement and whether the generated code verifies against that same specification, across 400 language-native problems. Right: CodeNova combines Constraint-Guided Specification with Verifier-Guided Candidate Repair to generate verified code under a self-generated specification.

Language	Specification	Verifier	Size	Native coverage
C	ACSL	Frama-C/WP	100	Pointers and aliasing, arrays and slices, loops, byte/string buffers, structs, frame conditions, and bounded C arithmetic
Java	JML	OpenJML ESC	100	Arrays, scalar and Boolean APIs, strings, nullability, object invariants, object/field frames, mutation, and exceptional behavior
Rust	Verus	Verus	100	Scalar arithmetic, Option / Result , vectors and slices, ownership and borrowing, unique mutation, bounds, and panic freedom
Python	Nagini specifications	Nagini	100	Typed scalar functions, Optional / None , lists and dictionaries, predicate permissions, mutation, and exception freedom

Table 2: The four language-native tracks in VeriCodeBench . Each track contains 100 problems.

Base LLM	Method	C (100)			Java (100)			Rust (100)			Python (100)
Base LLM	Method	Joint	Req. cov.	Valid	Joint	Req. cov.	Valid	Joint	Req. cov.	Valid	Joint	Req. cov.	Valid
DeepSeek V3.2	Direct	8	0.3247	34	30	0.7113	76	33	0.5522	44	46	0.8267	68
	+VGCR	11	0.3247	60	31	0.7113	82	45	0.5522	68	46	0.8267	71
	+CGS	12	0.5215	30	36	0.7810	56	30	0.5572	49	51	0.8593	65
	CodeNova	17	0.5215	54	38	0.7810	66	35	0.5572	58	52	0.8593	68
Kimi-K2.7-Code	Direct	16	0.5856	68	56	0.8250	77	57	0.6965	91	76	0.9327	86

Table 3: Results on VeriCodeBench , with 100 problems per language. Joint denotes joint-success counts; Req. cov. represents mean requirement coverage; Valid means code-valid counts. Direct and VGCR share the same generated specifications, as do CGS and CodeNova . Joint success requires both complete requirement coverage and verifier acceptance on the same problem. Bold values denote the best result. Second best results are underlined .

Base LLM	Method	C (100)		Java (100)		Rust (100)		Python (100)
Base LLM	Method	Self	Oracle	Self	Oracle	Self	Oracle	Self	Oracle
DeepSeek V3.2	Direct	34	$69_{\color[rgb]{0,0.65,0.31}\uparrow 25}$	76	$94_{\color[rgb]{0,0.65,0.31}\uparrow 18}$	44	$70_{\color[rgb]{0,0.65,0.31}\uparrow 26}$	68	$90_{\color[rgb]{0,0.65,0.31}\uparrow 22}$
DeepSeek V3.2	CodeNova	54	$69_{\color[rgb]{0,0.65,0.31}\uparrow 15}$	66	$99_{\color[rgb]{0,0.65,0.31}\uparrow 33}$	58	$91_{\color[rgb]{0,0.65,0.31}\uparrow 33}$	68	$93_{\color[rgb]{0,0.65,0.31}\uparrow 25}$
Kimi-K2.7-Code	Direct	68	$70_{\color[rgb]{0,0.65,0.31}\uparrow 2}$	77	$96_{\color[rgb]{0,0.65,0.31}\uparrow 19}$	91	$91_{\color[rgb]{0.98,0.44,0.26}-}$	86	$92_{\color[rgb]{0,0.65,0.31}\uparrow 6}$
Kimi-K2.7-Code	CodeNova	86	$89_{\color[rgb]{0,0.65,0.31}\uparrow 3}$	79	$100_{\color[rgb]{0,0.65,0.31}\uparrow 21}$	60	$93_{\color[rgb]{0,0.65,0.31}\uparrow 33}$	82	$95_{\color[rgb]{0,0.65,0.31}\uparrow 13}$
Qwen3.6-plus	Direct	50	$86_{\color[rgb]{0,0.65,0.31}\uparrow 36}$	83	$93_{\color[rgb]{0,0.65,0.31}\uparrow 10}$	56	$74_{\color[rgb]{0,0.65,0.31}\uparrow 18}$	65	$90_{\color[rgb]{0,0.65,0.31}\uparrow 25}$

Table 4: Code validity with self-generated versus oracle specifications. Self uses the Direct or CGS specification from Table 3 ; Oracle supplies a curated function specification. Both settings require the model to generate code and implementation-level proof annotations.

Figure 2: Pass@ $k$ joint-success curves across the four language tracks. The panels use language-specific y-axis ranges to improve visual resolution. Detailed analysis are provided in Appendix C .

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

Specification source	Validity	Coverage	Joint success
Self	91	0.697	57
Oracle	91	1.000	91

Appendix

Table 5: Kimi-K2.7-Code Direct results on Rust. Oracle contracts have full target coverage by construction, whereas equal validity under Self does not imply adequate generated specifications.

Explore similar work

VeriScale: Adversarial Test-Suite Scaling for Verifiable Code Generation
May 21, 2026Yifan Bai, Xiaoyang Liu, Zihao Mou +7Code Generation Large Language Model Benchmarks
School of Mathematical Sciences, Shanghai Jiao Tong University · School of Science and Engineering, The Chinese University of Hong Kong, Shenzhen · School of Mathematics, Jilin University +5
VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation
May 8, 2026Zichen Xie, Mrigank Pawagi, Yuxin Liu +5Code Generation Raw Judge Outputs
University of Virginia · 2Indian Institute of Science · 3Rice University +1
Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization
May 26, 2026Anmol Agarwal, Natalie Neamtu, Pranjal Aggarwal +6Autoformalization Raw Judge Outputs
CMU · Amazon · Work performed while at Amazon.

May 21, 2026, cs.LGJ/K move · Enter open · S save

VeriScale: Adversarial Test-Suite Scaling for Verifiable Code Generation

Yifan Bai, Xiaoyang Liu, Zihao Mou, Guihong Wang+6

School of Mathematical Sciences, Shanghai Jiao Tong University · School of Science and Engineering, The Chinese University of Hong Kong, Shenzhen · School of Mathematics, Jilin University+5

Code Generation Large Language Model Benchmarks Adversarial Evaluation

Open paper AskPDF arXiv

As large language models (LLMs) are increasingly deployed for software engineering, constructing high-quality benchmarks is crucial for evaluating not just the functional correctness, but also the formal verifiability of generated code. However, existing benchmarks are limited by the quantity and quality of positive and negative test cases, leading to an overestimation of model capabilities in generating specifications and implementations. To address this, we propose VeriScale, a novel framework driven by the adversarial implementations. It consists of two stages: test-suite expansion to construct diverse and challenging test cases, and test-suite reduction to distill them into compact yet discriminative suites. While VeriScale is general, we instantiate it on Verina to construct VerinaPlus, which expands the original test suites by over 83

\times

, and VerinaLite, a lightweight 14

\times

variant. Our experiments across eight state-of-the-art LLMs demonstrate that VerinaPlus exposes substantial model weaknesses hidden by the original benchmark, evidenced by sharp score drops on both SpecGen and CodeGen tasks, whereas VerinaLite maintains this discriminative power at a fraction of the evaluation cost. The enhanced benchmarks and source code are publicly available at https://github.com/XiaoyangLiu-sjtu/VeriScale.

Abstract

Explore similar work

VeriScale: Adversarial Test-Suite Scaling for Verifiable Code Generation

VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation

Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization