Large Language Models (LLMs) are widely used for code generation. However, the correctness of code generated by LLMs remains a concern. A potential remedy to this concern is to have LLMs generate formal correctness proofs along with such code. However, compared with code generation, code-proof generation requires much higher reasoning capability and has much less existing data to learn from. In this paper, we present VeruSyn, a data synthesis pipeline for Verus, a state-of-the-art verification tool for system software written in Rust. Through self-synthesis and tutorial-based synthesis, VeruSyn achieves much larger scale and Verus-feature coverage than previous data-synthesis techniques designed for Verus; VeruSyn also supplements its dataset with long-chain-of-thought (CoT) data through agent trajectory synthesis. With VeruSyn, we synthesize the largest set of Verus verified programs: 6.9 million Rust programs, each with a formal specification and a proof that it meets that specification. This dataset lets us create a fine-tuned Qwen2.5-Coder-32B-Instruct model with appealing cost-proof tradeoff compared with state-of-the-art commercial models like Claude Sonnet 4.5. It also significantly outperforms models like o4-mini and previously proposed research models.

翻译：大型语言模型（LLMs）在代码生成领域已得到广泛应用，但其生成代码的正确性仍存在隐忧。一种潜在的解决方案是让LLMs在生成代码的同时生成形式化正确性证明。然而，与代码生成相比，代码-证明生成需要更强的推理能力，且现有可供学习的数据量极为有限。本文提出VeruSyn——一个面向Verus（当前最先进的Rust系统软件验证工具）的数据合成流程。通过自我合成与教程引导合成，VeruSyn在数据规模和Verus特性覆盖范围上均远超此前针对Verus设计的数据合成技术；同时，VeruSyn还通过智能体轨迹合成方法，生成长思维链数据以增强数据集。借助VeruSyn，我们合成了规模最大的Verus验证程序集：包含690万个Rust程序，每个程序均配有形式化规范及其符合该规范的证明。基于此数据集，我们微调得到Qwen2.5-Coder-32B-Instruct模型，与Claude Sonnet 4.5等前沿商业模型相比，该模型在成本与证明能力间展现出更优的平衡性，其性能也显著超越o4-mini等模型及先前提出的研究模型。