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

arXiv: https://arxiv.org/abs/2602.04910 · HTML: https://mlsanity.com/paper/2602.04910/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 4 Feb 2026.

## Built on by (most cited first, 3 of 3)

- [Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs](https://mlsanity.com/paper/2607.04631/) (2026)
- [Fine-Tuning Qwen3-27B for C-to-Rust Code Translation: A Three-Stage Curriculum of Pretraining, Debugging-Aware SFT, and Task-Specific SFT](https://mlsanity.com/paper/2608.13681/) (2026)
- [TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents](https://mlsanity.com/paper/2610.14923/) (2026)

## Abstract (arXiv)

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.