Technical Summary: Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set

1. Problem Statement

The correctness of code generated by Large Language Models (LLMs) remains a significant challenge, particularly for security- and reliability-critical system software. While LLMs have demonstrated strong code generation capabilities, they frequently produce syntactically correct code that violates safety, security, or functional properties. A potential remedy is to require LLMs to generate formal correctness proofs alongside the code.

However, generating formal proofs for system software (specifically using Verus, a state-of-the-art verification tool for Rust) requires significantly higher reasoning capabilities than standard code generation. Furthermore, the field suffers from severe data scarcity. Existing verified Rust systems are few, and the available datasets (e.g., SAFE, AlphaVerus) are limited in scale and diversity. Prior work has shown that only expensive, large-scale commercial models (e.g., Claude Sonnet 4.5) possess the capability to generate such proofs effectively, while smaller or cheaper models fail. The core problem addressed by this paper is: How can we effectively generate code proofs at a low cost by synthesizing high-quality, high-volume training data for smaller LLMs?

2. Methodology: The VeruSyn Pipeline

The authors propose VeruSyn, a data synthesis pipeline designed to create the largest set of Verus-verified programs to date. The pipeline addresses three specific limitations of prior synthesis efforts: limited scale, narrow feature coverage, and low reasoning complexity. VeruSyn integrates three distinct synthesis approaches in an iterative, coordinated manner:

2.1 Scaling the Number of Programs (Self-Synthesis)

Unlike prior methods that rely on translating existing benchmark suites (which bounds the dataset size by the source), VeruSyn employs a self-synthesis strategy.

• Process: An LLM is fine-tuned to directly generate both Rust programs and their corresponding Verus specifications and proofs from scratch, without relying on pre-existing source programs.
• Iteration: The process begins with a base model fine-tuned on the SAFE dataset. This model generates initial programs. As synthesis proceeds, the model is iteratively fine-tuned on the newly generated, verified, and debugged data to improve its generation capabilities.
• Termination: Synthesis stops when the ratio of duplicate programs in a batch reaches 95%, ensuring diversity.

2.2 Scaling Feature Coverage (Tutorial-Based Synthesis)

To overcome the bias of prior datasets toward simple loop invariants, VeruSyn uses the Verus Tutorial as a structured knowledge source.

• Process: Experts manually create "seed programs" that cover key knowledge points from every chapter of the Verus tutorial.
• Synthesis: The proof-generation model is prompted to generate thousands of new programs for each seed, explicitly guided by the corresponding tutorial chapter.
• Goal: This ensures systematic coverage of diverse Verus features (e.g., quantifiers, non-linear arithmetic, bit vectors) that are often missing in algorithmic benchmarks but essential for real-world system verification.

2.3 Scaling Reasoning Complexity (Agent Trajectory Synthesis)

To handle complex, real-world system proofs that require long chains of reasoning, VeruSyn incorporates Chain-of-Thought (CoT) data derived from agent trajectories.

• Process: A state-of-the-art coding agent (powered by Claude Sonnet 4.5) is tasked with writing proofs for a small set of real-world system verification problems (from the VeruSAGE-Bench).
• Data Collection: The complete log of the agent's reasoning, actions (reading files, invoking Verus, analyzing errors, editing proofs), and final successful trajectory is collected.
• Integration: These trajectories are converted into training data, providing the model with examples of how to debug and reason through complex verification errors over multiple steps.

2.4 Anti-Cheating and Filtering

A critical component of the pipeline is a rigorous filtering process to prevent "cheating" (e.g., modifying specifications to make proofs trivially true, adding infinite loops to skip verification, or using assume statements).

• Mechanisms: The pipeline uses tree-sitter parsers to check specification compatibility, detects forbidden keywords (like assume), and enforces decreases clauses for termination.
• Debugging: Unverified programs are fed back to the model with error reports for debugging; only successfully verified pairs are retained.

3. Key Contributions

• Dataset Scale: The synthesis of 6.9 million Verus-verified Rust programs, each with a formal specification and a proof. This is the largest dataset of its kind.
• Feature Diversity: The dataset covers 12 to 15 distinct Verus knowledge points (out of 20 key points), significantly outperforming prior datasets (SAFE and AlphaVerus) which covered only 4–5 points meaningfully.
• CoT Integration: The inclusion of 4,557 long CoT instances derived from agent trajectories on real-world system tasks.
• Model Performance: A fine-tuned Qwen2.5-Coder-32B-Instruct model that achieves competitive proof synthesis capabilities at a fraction of the cost of commercial models.

4. Evaluation Results

The authors evaluated the VeruSyn-fine-tuned model on two benchmarks: VerusBench (150 algorithmic tasks) and VeruSAGE-Bench (849 tasks extracted from real-world Rust systems, with 289 excluded to prevent data leakage).

4.1 Accuracy

• System Proofs (VeruSAGE-Bench): Without debugging, the VeruSyn model achieved a 39% success rate (Accuracy@100), significantly outperforming the raw Qwen model (10%), SAFE-fine-tuned models (6%), AlphaVerus-fine-tuned models (11%), and the commercial o4-mini (15%).
• With Debugging: After 5 rounds of debugging, the VeruSyn model reached 49% accuracy, compared to 54% for the expensive Claude Sonnet 4.5.
• Algorithmic Proofs (VerusBench): The model achieved 75% accuracy (w/o debug), slightly outperforming Claude Sonnet 4.5 (72%).

4.2 Cost Efficiency

The paper highlights a dramatic reduction in cost:

• Per-Task Cost: The VeruSyn model costs approximately $0.17 per task (without debugging) and $0.61 (with debugging).
• Comparison: This is roughly 47x cheaper than Claude Sonnet 4.5 ($8.04 without debugging) and significantly cheaper than o4-mini ($3.39).
• Trade-off: The VeruSyn model with 5 rounds of debugging ($0.61) achieves higher accuracy (49%) than Claude Sonnet 4.5 without debugging (46%), representing a 13x cost reduction for superior performance.

4.3 Ablation Studies

• Data Components: Removing either the self-synthesis/tutorial data (Part 1) or the CoT data (Part 2) significantly degraded performance on real-world system tasks. Part 1 was crucial for algorithmic tasks, while Part 2 was essential for complex system proofs.
• Teacher Model: Using a stronger teacher model (Claude Sonnet 4.5) for CoT generation resulted in significantly better downstream performance (39% vs. 15% when using o4-mini as the teacher).

5. Significance and Claims

The paper claims that VeruSyn demonstrates that high-quality, large-scale synthetic data can bridge the gap between small, cost-effective open-source models and expensive commercial models in the domain of formal verification.

• Cost-Proof Tradeoff: The work establishes a new benchmark for cost-efficiency, showing that a 32B parameter model fine-tuned on synthesized data can outperform or match 4.5x larger commercial models at a fraction of the inference cost.
• Scalability: The methodology proves that self-synthesis and tutorial-guided synthesis can scale beyond the limitations of existing benchmark suites, creating an "unbounded" supply of training data for formal verification tools.
• Generalization: The results suggest that the synthesized data effectively teaches models not just syntax, but the complex reasoning patterns required for verifying real-world system software, a capability previously thought to be exclusive to the largest models.

The authors conclude that their training dataset is available on HuggingFace, aiming to lower the barrier to entry for formal verification in system software development.