Automated Proof Generation for Rust Code via Self-Evolution

1 INTRODUCTION

• SAFE addresses a shortage of Verus proof data: fewer than 500 Rust files were verified with Verus on GitHub, and suitable programs, specifications, and proofs are scarce.The paper describes scarcity at three levels: Verus-compatible programs, formal specifications, and proof annotations.Source: §1 · p. 2
• SAFE uses GPT-4o to translate programs into Verus-supported Rust, dropping any that fail the Verus compiler’s grammar check.The initial programs come from code-synthesis datasets; the conversion is performed once.Source: §1 · p. 2
• SAFE iteratively generates specifications and fine-tunes open-source models, retaining higher-quality specifications while accepting that proof-generation inputs need not be perfect.The framework uses a quantitative specification-quality metric and considers reasonably well-formed specifications sufficient to stimulate proof synthesis.Source: §1 · p. 2
• Verus filters synthesized proofs, and SAFE turns earlier incorrect proofs, verifier errors, and eventual correct proofs into self-debugging training examples.The approach uses evolving proof synthesis to increase the quantity and quality of proofs; its open-source models generate proofs faster than GPT-4o.Source: §1 · p. 2
• With self-debugging, SAFE reached 79.14% accuracy on VerusBench and 48.43% on CodeNet-Test, after direct-generation results of 43.17% and 43.83% versus GPT-4o’s 11.51% and 0.28%.The direct-generation comparisons are respectively for VerusBench and CodeNet-Test.Source: §1 · p. 3

2.1 VERUS VERIFICATION TOOL

• Verus statically analyzes a Rust function, its specification, and proof annotations, then sends queries to an SMT solver to check correctness.Verus uses Rust syntax for specifications and proof annotations, and fewer than 500 Verus-verified Rust files were available on GitHub.Source: §2.1 · p. 3
• For simple programs and specifications, Verus can verify without extra annotations; loops, collections, and quantifiers often require annotations such as loop invariants.Verus checks each invariant and uses proved invariants to help establish the function specification; incorrect or missing invariants cause proof failure.Source: §2.1 · pp. 3–4

2.2 PRIOR WORK IN PROOF-BENCHMARK BUILDING AND SELF-EVOLVING FRAMEWORK

• Prior proof-dataset construction is difficult to scale because proof writing requires expertise; GPT-4-synthesized Dafny datasets contained fewer than 200 proofs, many trivial.Existing human-written proof datasets and GPT-4-augmented datasets are both discussed as prior approaches.Source: §2.2 · p. 4
• SAFE must synthesize its own proof problems because it lacks both large manually written example corpora and a large supply of proof problems.Those problems are Verus-compatible Rust functions paired with specifications.Source: §2.2 · p. 4
• Verus proves a function as a whole with an SMT solver, making proof synthesis difficult to decompose and stepwise search strategies inapplicable.SAFE therefore treats whole-proof debugging as crucial.Source: §2.2 · p. 4
• SAFE accumulates training data through automated measurement and filtering at program translation, specification synthesis, and proof synthesis or debugging.The filters use the Verus compiler, a specification-quality metric, and Verus verification, respectively.Source: §2.2 · p. 4

3 APPROACH

• SAFE runs two self-evolving procedures: specification synthesis supplies inputs to proof synthesis, whose output is a fine-tuned LLM for Rust proof generation.Each round fine-tunes from data collected and filtered in previous rounds; low-quality specifications are discarded and incorrect proofs become self-debugging data.Source: §3 · p. 4

3.1 STEP 1: GENERATING VERUS-COMPATIBLE CODE

• SAFE uses GPT-4o to translate unsupported Rust code into Verus-compatible alternatives, retaining only code that passes the Verus compiler’s grammar check.For example, iterator-based code can be converted to while-loop-based code; this compatibility step occurs once.Source: §3.1 · pp. 4–5

3.2 STEP 2: SELF-EVOLVING SPECIFICATION SYNTHESIS

• SAFE generates specifications from each function and docstring, keeping those with at least 80% Correctness and 60% Completeness scores.The scores use Verus to measure acceptance of original input-output tests and rejection of output-mutated tests; the thresholds admit imperfect but useful specifications.Source: §3.2 · pp. 5–6
• SAFE permits incomplete specifications to stimulate proof synthesis, but discards incorrect specifications and those so incomplete that they yield trivial proofs.Perfect specifications are not required; complete specifications may be too challenging for early proof-synthesis models.Source: §3.2 · pp. 5–6

3.3 STEP 3: SELF-EVOLVING PROOF SYNTHESIS

• Only proofs that Verus accepts are retained; GPT-4o bootstraps proof synthesis, after which a smaller open-source LLM is fine-tuned for proof generation and self-debugging.The detailed bootstrap prompt enabled GPT-4o to synthesize annotations for more than one thousand functions, at the cost of a month of continuous invocations.Source: §3.3 · pp. 6–7
• For each eventually verified proof, SAFE pairs earlier incorrect proofs with Verus errors and the correct proof to train self-debugging.Joint training targets both generating a proof from scratch and repairing one using verifier feedback.Source: §3.3 · p. 7

4.1 DATASET

• After three rounds of proof synthesis, SAFE’s dataset contains 9,706 verified programs and 10,486 self-debugging data pairs from 45,395 collected Rust single-function programs.The VerusBench set has 139 files; CodeNet-Test has 1,435 tasks and is 10× larger than VerusBench.Source: §4.1 · p. 7, §4.2 · p. 7

4.3 EVALUATION RESULTS

• 46.04% Accuracy@1 and 53.96% Accuracy@10 for SAFE on VerusBench, versus GPT-4o’s 11.51% and 24.46%; SAFE+ with DeepSeekCoder reaches 70.50%.The 70.50% result uses 10 initial proofs and 10×10 debugged proofs per task.Source: Table 1 · p. 8, §4.3 · p. 8

4.2 BENCHMARK AND METRICS

• Accuracy@K counts a task as correct when at least one of K generated or debugged proofs verifies; SAFE+ can generate K initial proofs and then K debugged proofs for each failed initial proof.Accuracy@1 uses greedy decoding; Accuracy@10 samples ten outputs at temperature 0.7.Source: §4.2 · p. 8

4.3.1 BENEFITS FROM SELF-EVOLVING

• Across VerusBench subsets, the best Accuracy@1 and Accuracy@10 scores occur in the final two evolution rounds, and Round 3 beats GPT-4o on all three subsets.On SV, Round 3 reaches 78.95% Accuracy@1 (81.58% with self-debugging), versus GPT-4o’s 39.47%; on MBPP, the corresponding values are 30.77% (41.03%) and 19.23%.Source: §4.3.1 · p. 9, Table 2 · p. 9

4.3.2 IMPROVEMENT OF SELF-DEBUGGING

• Self-debugging improves accuracy over direct generation, and sampling multiple initial proofs followed by one debugged proof each outperforms generating one proof followed by multiple debugged proofs.Additional self-debugging rounds add less than 1% accuracy.Source: §4.3.2 · p. 9

4.3.3 IMPACT OF SPECIFICATION QUALITY

• Low-quality specifications reduce accuracy across all three VerusBench subsets, and mixing low-quality data with selected high-quality data also lowers performance.In the Low-Quality setting, SV falls to 0% Accuracy@1 and 5.26% Accuracy@10; the experiment compares these settings with SAFE’s selected specifications.Source: §4.3.3 · pp. 9–10, Table 3 · p. 10

5 CONCLUSION

• SAFE combines self-evolving data synthesis, model fine-tuning, and self-debugging to improve open-source models’ Rust proof generation.The conclusion says the framework uses tens of thousands of synthesized proofs and a self-debugging mechanism.Source: §5 · p. 10
• The conclusion reports that SAFE improves efficiency and precision compared with relying solely on GPT-4o.Source: §5 · p. 10

A VERUS EXAMPLES

• Verus reports zero verified results and two errors for the imperfect binary-search proof.The listing is labeled an imperfect proof and includes a failed postcondition and possible arithmetic underflow/overflow errors.Source: A VERUS EXAMPLES · p. 15

A.1 IMPERFECT PROOF EXAMPLE

• Without a crucial binary-search loop invariant, Verus cannot establish the postcondition or prove the absence of arithmetic underflow and overflow.The missing invariant concerns the existence of the search key within the current interval; without it, Verus cannot reason about how the interval changes.Source: §A.1 · pp. 15–16

A.2 MORE COMPLICATED PROOF ANNOTATIONS

• The Fibonacci example uses loop invariants, a proof function, a proof block, and assertions as hints to the theorem prover.The example is attributed to the Verus paper.Source: §A.1 · p. 16, §A.2 · p. 17

B PROMPTS

• SAFE’s proof-generation prompt asks for proof code, including loop invariants and assertions, so Verus can verify the Rust function against its specifications.Source: B PROMPTS · p. 17
• The self-debugging prompt supplies incorrect Verus code and error messages and asks the model to return corrected, verifiable code.Source: B PROMPTS · p. 17

C.1 SPECIFICATION FILTERING

• A specification that accepts a binary-search implementation always returning 0 is correct but incomplete, while another can reject a correct implementation when duplicate keys occur.Source: §C.1 · p. 17
• Test-case checks assess whether a synthesized specification is consistent by replacing the function body with assumptions for test inputs and outputs, then asking Verus to prove it.For containers, inserted assertions help the theorem prover reason about each element.Source: §C.1 · p. 17
• GPT-4o’s proof-generation prompt instructs it to add loop invariants and proof blocks, with refinements for variables, constants, arrays, quantifier ranges, and first-iteration conditions.It also permits ghost variables and requests proof blocks where needed.Source: §C.1 · p. 18
• Mutating a ground-truth output by adding an absent value tests whether the specification rejects the altered case, exposing possible incompleteness.The example adds 15 to the result vector; Verus reports failure if the postcondition requires that value to exist in the input vector.Source: §C.1 · pp. 18–19
• SAFE scores specifications using five ground-truth and, on average, 20 mutated wrong test cases, retaining scores of at least 0.8 for correctness and 0.6 for incompleteness, with at most three per function.Source: §C.1 · p. 19

C.2 STATISTICS OF SYNTHESIZED DATA

• 21,398 of the 45,495 Rust single-function programs were retained after translation into Verus-compatible Rust for specification synthesis.A random subset of CodeNet programs was held out for evaluation and excluded from the reported synthesized-data counts.Source: §C.2 · p. 19
• 9,706 verified programs and 10,486 debugging examples produced after Round 2 were used to fine-tune the Round-3 proof-synthesis model.Round 0 used GPT-4o to produce 3,673 verified programs over a month, and two later rounds selected 19,017 specifications for proof synthesis.Source: §C.2 · p. 19

C.3 TRAINING HYPERPARAMETERS

• DeepSeekCoder was trained for five epochs per round at batch size 128 and learning rate 1 × 10^-5; specification synthesis ran for two rounds and proof generation for three.The process was bootstrapped with 3,673 GPT-4o-synthesized verified programs.Source: §C.3 · p. 20

D.1 SCALING TO REAL-WORLD LARGE SOFTWARE PROJECTS

• SAFE focuses on small programs because too few large Verus projects exist for fine-tuning, and cross-function dependencies may require support beyond machine learning.Dependencies may cross files or classes; the authors believe models trained on small-program functions could still be useful in larger projects.Source: §D.1 · p. 20

D.2 FINE-GRAINED SELF-DEBUGGING

• More self-debugging rounds hardly improve proof-synthesis accuracy; future training data could map individual edits to the verification errors they fix.Current incorrect-to-correct proof pairs may contain multiple mistakes and corresponding verification errors.Source: §D.2 · p. 20

E.1 STATISTICS OF VERUSBENCH

• For preconditions, SV’s average token count is substantially larger than MBPP’s and Tutorial’s, while for postconditions SV’s is substantially smaller than the other two.The authors say these statistics suggest SV is relatively easier than the other components.Source: §E.1 · p. 20, Figure 3 · p. 21
• Human-written proof annotations average more tokens for MBPP than Tutorial, although Figure 3c includes outliers.Source: §E.1 · p. 20, Figure 3 · p. 21

• Many synthesized specifications are trivially correct but have completeness scores below 0.6, leading to trivial proofs and filtering.These clusters have correctness score 1.0 and fall outside the accepted-score rectangle.Source: §E.2 · p. 21
• A large cluster has completeness 1.0 but correctness 0 because its specifications incorrectly reject all test cases.Verus cannot prove the Rust function satisfies these specifications, regardless of proof annotations, so SAFE filters them out.Source: §E.2 · p. 21
• SAFE keeps specification clusters that overlap the accepted-score range and filters the described incomplete or reject-all cases.Source: §E.2 · p. 21

• All fine-tuned LLaMa and DeepSeekCoder models have p-values below 5E-7 versus their raw models, indicating significant improvement.Source: Table 5 · p. 21, §E.3 · p. 21
• In most scenarios, low-quality specifications may significantly decrease SAFE’s end-to-end effectiveness, except Accuracy@1 in round 2 with low-quality specifications.Source: §E.3 · p. 21
• Round 2 and round 3 significantly improve accuracy over round 1, especially after self-debugging; round 2 to round 3 improvement is insignificant except for Tutorial after self-debugging.The authors conclude that three rounds of self-evolution are sufficient.Source: §E.3 · p. 21, Table 6 · p. 22

E.4 SELF-EVOLUTION WITH SMALL BACKBONE MODELS

• SAFE’s self-evolution improves VerusBench accuracy with a 1.3-billion-parameter backbone.Table 8 reports accuracy across rounds; the supplied text gives no exact values.Source: §E.4 · p. 23, Table 8 · p. 23

F.1 SAFE’S ADVANTAGES COMPARED TO GPT-4O

• SAFE adds an invariant bounding original array values by 0x7FFFFFFB, addressing the arithmetic underflow/overflow missed by GPT-4o.SAFE’s proof for the program is correct, while GPT-4o’s proof omits proofs for potential arithmetic underflow/overflow.Source: §F.1 · p. 23

F.2 THE EFFECTIVENESS OF OUR SELF-DEBUGGING MECHANISM

• Self-debugging fixes a sortedness proof by changing the loop invariant’s index boundary from index to index + 1.Verus’s error identifies an invariant that cannot be verified; the adjusted boundary lets Verus finish the proof.Source: §F.2 · pp. 23–24

F.3 AN INEFFECTIVE EXAMPLE

• SAFE fails on 20.86% of VerusBench programs even after sampling 100 proofs and 100 debugged proofs per incorrect proof.In the remove-odds example, repeated attempts leave loop invariants unsatisfied; proving it requires assert statements and Verus’s reveal feature, which may be absent from the fine-tuning data.Source: §F.3 · p. 25

F.4 AN EXAMPLE PROOF WITH A LOW-QUALITY SPECIFICATION

• The gcd specification requires only result > 0, not that the result divides both inputs.The program computes the greatest common divisor of two integers using the Euclidean Algorithm.Source: §F.4 · p. 25
• With the low-quality specification, synthesized proof annotations simply copy the precondition a > 0 and b >= 0.Source: §F.4 · p. 25
• Because realistic tasks rarely admit proofs that simply copy preconditions, adding many proofs from low-quality specifications does not help model evolution.Source: §F.4 · p. 25