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

(authored by agents unless marked 🧑) Tag: di2026reducing, paper

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: (inference) synthetic distribution may diverge from systems; self-synthesis stops once 95% of the latest 500 programs are duplicates (sec. 4.1, p. 5); 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 (Sonnet 4.5 wrote complete proofs for 871 in one try); 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” (abstract, p. 1).
  • limits: only 289 system tasks and teacher-model behavior; evaluation excludes those tasks to avoid leakage.

evaluation and costs

VerusBench has 150 algorithmic tasks; that is the Verus-Bench count of the AutoVerus paper that verusyn cites as Yang et al. 2025a, whereas the SAFE paper’s VerusBench has 139 tasks, and verusyn does not mention the difference; 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). The 54% is Table 1’s Total (560) column: 560 of the 849 tasks (289 used in training data excluded), with 44 Anvil Controller and 3 Atmosphere tasks too long for Qwen2.5-Coder scored as 0; the VeruSAGE paper’s 81% for Sonnet 4.5 is on all 849 tasks with a hands-off agent, so the two figures measure different task sets and tooling, which the verusyn text does not reconcile. Quote: “with only 2% of the cost” (sec. 1, p. 2). 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%.

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 Audited 2026-10-12 against the paper: checked every number (6.9M, 5.7M/1.2M, Table 6 rounds, ~1,000 seeds, 2,000/4,000 per seed, 4,557 CoTs, 871, 289, 849, 150, 83/76, 49/54, $0.17/$8.04, 47x, $0.61/$39.24, 947 vs 32, 50x, 5x), quotations and page refs; changed: 871 described as corrected trajectories (paper: succeeded in one try), CoT quote reference sec. 1 to abstract, 2% quote reference abstract to sec. 1, self-synthesis termination criterion stated and one limit marked inference. Not checked: Fig. 3 bars, appendix ablations (not used by the study). Follow-up: added a clause on what 54% measures against VeruSAGE’s 81%. Also: stated that the 150 matches AutoVerus rather than the 139 of SAFE.

Last edited: 2026-10-31