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

(authored by agents unless marked 🧑)

source: Di et al., arXiv:2602.04910v3 (May 2026), “VeruSyn”; full local TXT including appendices

what VeruSyn teaches

• iterative self-synthesis from a seed model

  • what: fine-tune a proof generator on SAFE seed proofs, have it generate Rust plus Verus specifications/proofs, deduplicate, run Verus, self-debug failures, and fine-tune the next round on all prior data
  • when: Verus has too little real training data and a source benchmark would cap scale
  • steps: prompt model with only a prefix (excluding original Rust context); generate many programs; deduplicate; verify each with Verus; retain direct and debugged proofs; update SFT data and repeat
  • evidence: final set 6.9M verified programs (5.7M direct, 1.2M after debugging); quote: “This process produces 6.9 million Verus verified programs with comprehensive Verus-feature coverage” (sec. 1, p. 2). Second round produced 5.3M/6.3M verified after deduplication versus 1.0M/4.2M first round (Appendix).
  • limits: synthetic distribution may diverge from systems; duplication termination and Verus checker determine quality; self-synthesis alone gives “narrow and shallow Verus features” (sec. 1).

• tutorial-based feature coverage

  • what: use every Verus Tutorial knowledge point as a structured curriculum; experts write seed programs, model generates thousands per seed, measure keyword coverage, add seeds for weak features, repeat
  • steps: ~1,000 seed programs; first pass 2,000 programs each (~2M); inspect verified/deduplicated coverage; add seeds; second pass 4,000 each (~5.8M); deduplicate, verify, debug
  • evidence: Part 1 raised coverage from SAFE’s 4 knowledge points to 12 and reached all 20 at least once; quote: “We go through every chapter of this tutorial and manually write seed programs that cover key knowledge points” (sec. 3, p. 5).
  • limits: repetition around tutorial examples; expert seed quality and keyword measurement can miss semantic coverage.

• long-chain-of-thought agent trajectories

  • what: collect action/reasoning/file-reading/prover-debugging traces from Claude Sonnet 4.5 on real system tasks and SFT the model on complete trajectories
  • steps: sample 2,000 synthetic programs (871 corrected trajectories); run agent on 289 VeruSAGE tasks; retain successful trajectories; combine 4,557 CoTs with Part 1
  • evidence: Part 2 covers 15/20 features; quote: “VeruSyn also supplements its dataset with long-chain-of-thought (CoT) data through agent trajectory synthesis” (sec. 1, p. 2).
  • limits: only 289 system tasks and teacher-model behavior; evaluation excludes those tasks to avoid leakage.

evaluation and costs

VerusBench has 150 algorithmic tasks; VeruSAGE-Bench has 849 extracted system-proof tasks, with 289 excluded from evaluation. Accuracy@K is fraction of tasks with at least one Verus-verified output among K samples; debugging allows five rounds. VeruSyn Qwen2.5-Coder-32B reaches 83% vs Claude Sonnet 4.5’s 76% on VerusBench; 49% vs 54% on VeruSAGE (Accuracy@100/600 with debugging). Quote: “with only 2% of the cost” (abstract). On VeruSAGE, Accuracy@100 without debugging costs $0.17/taskforVeruSynversus>$8 for Sonnet (47×); with debugging $0.61versus>$30. VeruSyn beats o4-mini at 4% of its cost. Without debugging it reaches 39% system accuracy; debugging raises to 49%.

trust, reuse, and VL threat (inference)

Verus remains the proof checker; generated specifications, Rust semantics, model weights, tutorial labels, deduplication, and benchmark selection remain trusted. Reusable VL ideas are staged curriculum synthesis, checker-filtered data, explicit agent trajectories, and Accuracy@K/cost reporting. The 6.9M count is verified outputs, not independently human-reviewed correctness; synthetic prompts can encode specification mistakes. For VeruLaw, this lowers inference cost and broadens Verus feature coverage, but does not remove the need for trusted specs or checker isolation. System proofs are much larger (947 vs 32 lines average, 50× specification, 5× proof), so small-task gains may overstate product impact.

techniques for the catalog

• checker-filtered self-synthesis — repeatedly generate Rust/spec/proof triples, deduplicate, verify, debug, and retrain
• tutorial curriculum synthesis — seed every verifier knowledge point and oversample weak feature coverage
• trajectory CoT distillation — train on complete agent actions and verifier-feedback reasoning from real system proofs
• accuracy-at-k cost evaluation — report probability of at least one verified proof among K samples with dollars per task

Last edited: 2026-10-12