Automated Proof Generation for Rust Code via Self-Evolution

## Abstract

Abstract Ensuring correctness is crucial for code generation.
Formal verification offers a definitive assurance of correctness, but
demands substantial human effort in proof construction and hence raises a pressing need for automation. The primary obstacle lies in the severe lack of data — there is much less proof than code for LLMs to train upon.
In this paper, we introduce SAFE, a novel framework that overcomes the lack of human-written proof to enable automated proof generation of Rust code. SAFE establishes a self-evolving cycle where data synthesis and fine-tuning collaborate to enhance the model capability, leveraging the definitive power of a symbolic verifier in telling correct proof from incorrect ones. SAFE also re-purposes the large number of synthesized incorrect proofs to train
the self-debugging capability of the fine-tuned models, empowering them to fix incorrect proofs based on the
verifier’s feedback.
SAFE demonstrates superior efficiency and precision compared to GPT-4o.
Through tens of thousands of synthesized proofs and the self-debugging mechanism, we improve the capability of open-source models,
initially unacquainted with formal verification, to automatically write proof for Rust code.
This advancement leads to a significant improvement in performance, achieving a 70.50% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o’s performance of 24.46%.

## 1 Introduction

Large Language Models (LLMs) have recently exhibited impressive capabilities in code generation
(Roziere et al., ; Guo et al., ; Lozhkov et al., ; Google, ).
However, the correctness of generated code cannot be guaranteed. To tackle this issue, prior research (Chen et al., ; Zhang et al., ; Huang et al., ) has explored assessing generated code by
test cases, which sometimes are
also generated by LLMs. Although helpful, testing cannot cover all possible program inputs; they can reveal the presence of bugs but cannot prove their absence (Dahl et al., ).
In contrast, formal verification employs a symbolic prover to mathematically prove that a program satisfies the desired properties under all possible inputs, without running the program. Unfortunately, to use formal verification, one needs to first formally express the desired properties, often in a special proof-oriented language,
and then craft formal proofs, which takes substantial formal verification
expertise
(Zhang et al., ).
Therefore, to advance trustable code generation, automated formal verification, particularly automated proof generation, is in a pressing need.

Two main approaches of proof automation have been explored.
The first (Misu et al., ; Sun et al., ; Pei et al., ; Liu et al., ; Chakraborty et al., ; Kamath et al., ; Chakraborty et al., ; Yao et al., ; Yang et al., ) relies
on well crafted prompt or in-context learning on LLMs.
To compensate for the unfamiliarity of LLMs towards formal proof,
this approach often requires intensive prompt engineering that hard codes proof-writing tips, many
LLM invocations, and/or support from static
program analysis,
resulting in a limited generalization ability.
The second approach (Polu et al., ; First et al., ; Azerbayev et al., ; Yang et al., )
fine-tunes open-source LLMs.
This approach has shown to be effective for
Lean (Avigad, ) (for mathematical proving) and F^∗ (Swamy & Hrit, )
(a special proof-oriented language), where tens of thousands of human-written Lean and F^∗ proofs exist.
However,
how to apply this data-oriented approach to many other verification tools or proof languages that have much less exiting proof remains as an
open question.

In this paper, we tackle this open
question in automating proof generation for Verus (Lattuada et al., ),
the state-of-the-art verification tool for code written in Rust.
Verus is a perfect target for us, since (1) it is one of the
rare verification tools that can directly prove the correctness
of code written in a popular language (Rust),
which is increasingly widely used in production as a safer and better alternative to C/C++ (ONCD, ; Rivera et al., );
and (2) due to
its short history, there are fewer than 500 Rust files currently
verified by Verus on GitHub, too few for fine-tuning.

The challenge of lacking data for Verus proof generation shows up
at several levels.
First, lack of suitable programs to quickly generate proof for. Not all Rust features are supported by Verus yet. Furthermore, large Rust
projects typically require code refactoring to get verified
(Zhou et al., ; Sun et al., ), and yet small Rust programs may not have meaningful
properties to prove (e.g.,
a hello-world function).
Second, lack of Verus specifications. Before proving any Rust function,
Verus needs a formal specification that describes the expected behavior of the function,
such as the pre-condition (Line 7–9) and post-condition
(Line 10–13) shown in Listing 1. Not surprisingly,
these specifications do not
exist except for in those existing verified Rust files on Github. Third, lack of Verus proofs.
It took many months to write a couple of thousand
lines of Verus proofs
even for experts (Zhou et al., ; Sun et al., ). It took
more than ten years’ effort to accumulate those fine-tuning
training data for Lean (Yang et al., ) and F-Star (Chakraborty et al., ).

In this paper, we propose the Self-evolving Automated prooF gEneration (SAFE) framework that overcomes the challenge
of multi-level data scarcity.
First, to quickly obtain a large number of proof-friendly Rust programs, we leverage
GPT-4o to “translate” tens of thousands of small Python and Rust programs in popular code-synthesis
datasets to Rust programs written in Verus-supported Rust features.
Any program that cannot be compiled by Verus compiler is dropped.

Second, to obtain formal specifications for these tens of thousands of Rust
programs, SAFE uses a procedure of
self-evolving specification generation. This procedure is bootstrapped by GPT-4o that is prompted to generate Verus-style
specifications based on each Rust function and its associated
natural language doc-string. In every following round,
those specifications generated in previous rounds
are used to train a new fine-tuned open-source LLM that produces
more specifications in generally higher quality for the next
round of finetuning. Keys to the success of this step include
(1) using a quantitative metric (Lahiri, ) to differentiate high-quality
specifications from low-quality ones, and only use the former
for finetuning; and (2) the observation that we only need
reasonably well, instead of perfect,
specifications to enable proof generation in the next step.

Next, to obtain tens of thousands of verified Rust programs,
SAFE similarly uses a self-evolving procedure. Proof is
much harder to synthesize than specifications. Even with careful prompt
engineering,
GPT-4o only managed to synthesize correct proof for
$<20\%$ of programs in the dataset with specifications synthesized
above, after a month
of non-stop invocation. Fortunately, this is sufficient to
bootstrap SAFE.
Through rounds of self-evolving, the quantity and quality of synthesized proof keeps increasing, while the fine-tuned open-source model’s capability of proof synthesis keeps getting augmented. These models also generate proof much
faster than GPT-4o.
The keys to the success here include (1) the ability of Verus in authoritatively and quickly
telling correct proof from incorrect ones, which allows SAFE
to sift through the huge amount of low-quality data in early rounds without any human labeling, and (2) the
reasonable quality of SAFE-synthesized specifications that allow
SAFE to largely
avoid trivial proofs, which have little usage in fine-tuning.

Finally, SAFE re-purposes the huge number of incorrect proofs generated in the previous step to
add self-debugging capability
into its models.
In each round, whenever a correct proof $P_{\checkmark}$ is synthesized after several attempts, the triplet of an earlier incorrect proof $P_{X}$, the verification error reported by Verus on $P_{X}$, and $P_{\checkmark}$, becomes a training data point, which fine-tunes the model’s capability in
debugging and repairing proof— a great side effect of having incapable models early on.

In our experiments, SAFE leverages DeepSeekCoder (Guo et al., ) as the generator, successfully synthesizing 19,017 formal specifications and 9,706 verified Rust functions, from a dataset comprising 45,395 Rust functions sourced from the MBPP (Austin et al., ) training split and the CodeNet (Puri et al., ) training dataset.
Note that, the initial Rust dataset contains zero lines of formal specification or proof.
Our evaluation on a human-curated Verus benchmark with human-written specification, VerusBench, and a synthetic benchmark, CodeNet-Test demonstrate that SAFE empowers DeepSeekCoder, which is initially unacquainted with Verus, to achieve 43.17% and 43.83% accuracy on the two benchmarks by direct generation, far surpassing GPT-4o’s performance of 11.51% and 0.28%.
Furthermore, the model’s accuracy reaches 79.14% in VerusBench and 48.43% in CodeNet-Test once its self-debugging feature is used.

We believe a
key to SAFE’s self-evolving framework lies in its automated measuring and filtering mechanisms for every step of data synthesis — Verus compiler for the first step, the quantitative specification-quality metric for the second step, and Verus verification for the last two steps.
These mechanisms allow high-quality training data to gradually get accumulated without human labelling.
We believe this SAFE approach can be extended and adapted to enhance any LLMs and other formal languages that face data scarcity issues, offering a promising solution for proof automation.
Finally, we will open source our code and benchmarks.

## 2 Background and Related Work

Figure: Listing 1: An Example Verus Program (Binary Search).

### 2.1 Verus verification tool

To formally prove whether a Rust function is guaranteed to satisfy its specification, Verus (Lattuada et al., ) statically analyzes the Rust code, the specification, and the proof annotations, and forms queries for the underlying SMT-solver (e.g., Z3 (De Moura & Bjørner, )) to formally solve. By leveraging the type system in Rust and allowing both specification and proof annotations to write in Rust syntax, Verus has become the state-of-the-art verification tool for Rust, one of the most popular programming languages (JE & CT, ; Fulton et al., ), and has been used to successfully verify large Rust systems (Sun et al., ; Zhou et al., ).
Unfortunately, since Verus has been developed for only about three years, there are less than 500 Verus verified Rust files on Github so far. Meanwhile, although Verus specifications and proof are written mostly in Rust, they are still difficult to generate for both human beings (Sun et al., ; Zhou et al., ) and LLMs.

Listing 1 shows a Rust function that implements binary search.
At
high level, the function specification (Line 7–13) states that the post-condition, expressed in a ensures code block, is
guaranteed to hold as long as the pre-condition,
in a requires block, is true. For this function,
its pre-condition (Lines 7-9) states that the input array is ordered in an ascending manner and that the input value to be searched k must exist in the array (forall and exists are Verus quantifiers). The post-condition requires that the return value $r$ should be a valid index pointing to the input value k.

For simple programs/specifications, Verus can accomplish the formal verification without any extra annotations (we refer to these cases as trivial proof). Unfortunately, for functions and specifications that involve loops,
collections, and quantifiers, Verus often needs users to provide
proof annotations. The loop invariants specified on Line 18–21 are one type of proof
annotations. They specify what properties are true right before
and right after every loop iteration. Verus will prove the
correctness of each loop invariant and then use proved loop
invariants to help prove the function specification. If any loop invariant
is incorrect or if needed invariants are missing, the proof will fail.
For more complicated tasks, other types of proof annotations
like assert and lemma functions may be needed.

### 2.2 Prior work in proof-benchmark building and self-evolving framework

There was much effort recently in building verification dataset of existing human written proofs (Loughridge et al., ; Zhang et al., ; Chakraborty et al., ). Unfortunately, since writing formal proof takes expertise beyond normal coding,
this dataset building approach is difficult to scale.
Recent work has explored augmenting the Dafny-proof dataset using proofs synthesized by GPT-4 through few-shot learning and human-written proof examples (Misu et al., ; Sun et al., ).
However, due to the limited proof-generation power of GPT-4, the number of proofs in these dataset are fewer than 200, with many being trivial proofs.

Self-evolving style of learning has been explored before in other context.
While (Gulcehre et al., ) propose a reinforced self-training framework in the machine translation task,
(Polu et al., ) leverages the expert iteration strategy for mathematical theorem proving with Lean.
Our work applies the idea of self-evolving to a very different task, synthesizing correctness proof for
Rust code, with different challenges: unlike previous work,
Verus does not have a large collection of existing data for bootstrapping; there is much less a concern of generating
“specification” in mathematical theorem proving; furthermore, unlike interactive theorem provers that decompose a
proof problem into small steps through tactics (e.g., Lean), Verus uses SMT-solver with hints from proof
annotations to prove the whole function
correctness as a whole and hence presents completely different challenges to proof synthesis.

## 3 Approach

As illustrated in Figure 1, SAFE involves two self-evolving (Tao et al., ; Gulcehre et al., ) procedures.
The first procedure synthesizes specifications that are used as inputs to the second procedure, while
the second procedure produces the end-result of SAFE — a fine-tuned LLM that can automatically
synthesize proof for Rust code.

In Algorithm 1, we show the two procedures of our self-evolving framework.
In both procedures, we use GPT-4o to generate the round-0 0 data $spec/proof\textit{-}data_{0}$.
In each round $r$, we use data collected and filtered from rounds 0 to $r-1$ to fine-tune $model_{r}$ based on its preceding $model_{r-1}$. At the end of each round, $model_{r}$ is used to generate the round-$r$ data, which is then graded and filtered. High-quality data is preserved for the next round. Low-quality specifications are discarded; incorrect proofs are re-purposed to become self-debugging training data for the next round.
This iterative approach substantially improves the volume and quality of the synthesized data.

In the following, we present more details for each step of SAFE.

Figure: Figure 1: The SAFE Framework
Refer to caption: x1.png

Figure: Algorithm 1 Self-Evolving

### 3.1 Step 1: Generating Verus-compatible Code

This step ensures the compatibility of our input Rust programs with Verus, which does not support all Rust features.
For instance, some Rust expressions and standard library functionalities like for, Iterators, HashMap,
and others are not supported or only partially supported by Verus.
Thus, it is necessary to adapt normal Rust code to Verus-compatible one before adding specifications.

To address this compatibility issue, we employ GPT-4o as a code translator, effectively substituting Verus-incompatible
Rust code snippets with Verus-compatible alternatives, such as converting an iterator-based implemenation into a while-loop
based implementation.
Specifically, we prompt GPT-4o with all the unsupported features sourced from Verus official documentation. All the converted codes that can pass the grammar check of Verus compiler are collected for next steps.
This step is performed only once in our self-evolving framework.

### 3.2 Step 2: Self-evolving Specification Synthesis

In this step, LLMs are tasked with generating preconditions and postconditions for a Rust function based on the function’s implementation and
docstring.
Different from prior work in spec-generation (Flanagan & Leino, ; Ma et al., ), SAFE
needs synthesized specification as input for its self-evolving proof-synthesis framework, which raises unique requirements on its spec-evaluation criteria (i.e., which specification to keep or discard) and the mechanism to evaluate the criteria.

In terms of criteria, generally speaking, a perfect specification $S$ should be correct (i.e., any correct implementation should be accepted by $S$)
and complete (i.e., any incorrect code implementation should be rejected by $S$). For example, the spec in the
left column below is correct but incomplete for the binary search function, as an incorrect implementation that
always returns 0 would be accepted by this spec;
the spec in the right column below is incorrect, as
a correct implementation may fail this spec when the input array has multiple elements matching the search key.
In SAFE, getting perfect specification is not the goal.
SAFE should discard incorrect specifications, which can never be proved no matter what proof
annotations are used and hence will waste
training cycles in the next step.
However, SAFE is fine with incomplete specifications, as the usage of spec in SAFE is to stimulate
proof synthesis not to judge code correctness. In fact, SAFE needs incomplete specifications,
as complete specifications are likely too challenging to prove at the early stage of the proof-synthesis model’s
evolution.
Of course, specifications that are too incomplete should be discarded, because trivial specifications can be proved
without any proof annotations and hence offer no usage for proof-synthesis training (e.g., 0 <= r for the binary search function).

In terms of the mechanism to evaluate the above criteria, much previous work relies on running many test cases, formal
verifying the consistency between spec and code, or user inspection. None of these mechanisms suit SAFE: relying on user inspection or
running the program through many test cases would
severely slow down the self-evolving framework; formal verification also does not work when we do not have a capable model to
automatically synthesize proof.

With all these constraints in mind, SAFE chooses to leverage a recently proposed technique (Lahiri, )
to symbolically and quantitatively measure the Correctness and Completeness of specification. Specifically, we
use Verus to symbolically evaluate what percentage of test cases $\mathbf{T}$ provided by the original dataset can pass a given specification $S$
(i.e., the Correctness score),
and what percentage of test cases $\mathbf{T^{\prime}}$ mutated from $\mathbf{T}$ can be rejected by $S$
(i.e., the Completeness score).
Since Verus can symbolically conduct this evaluation without checking code implementation, this process can be done very quickly;
since this technique offers quantitative scores, we can set a threshold that fits the
unique need of SAFE. Specifically, we keep all the specifications that have higher than 80% of Correctness score and
higher than 60% of Completeness score.
This way, SAFE can obtain many imperfect but useful specifications for its proof synthesis.
We do not set the Correctness threshold to be 100%, because we also use GPT to generate some test cases when few test cases are provided by the dataset, and we cannot guarantee perfect correctness of these test cases.

We keep up to three synthesized specifications for each function, which not only enriches the
spec-training dataset but also increases the chance of synthesizing valid proof later.
Our self-evolving process for specification stops when there is no significant increase in total number of
accepted function–spec pairs, at which time all these pairs move on to become the input for the next step.

### 3.3 Step 3: Self-evolving Proof Synthesis

Now that we have tens of thousands of function-specification pairs, we can start the self-evolving procedure of proof synthesis.
Comparing with spec-synthesis, deciding whether to accept or reject a synthesized item
is much more straightforward — only proof that Verus can use to verify the Rust function satisfies its specification is
accepted; if any verification errors are raised, the proof is discarded(^1^11If a Rust function is in fact buggy or a synthesized specification is incorrect, no proof will be accepted.).
However, since proof synthesis is much more difficult than specification synthesis, we need to pay special attention to
bootstrap the self-evolving procedure and to keep it moving forward.

For bootstrapping, we realized that a simple prompt to GPT-4o, like “You are an expert in Verus. Your mission is to
write
proof annotations for the following function”, would not work. It is very difficult for GPT-4o to
synthesize all the needed loop invariants without any incorrect ones in
between. More complicated proof annotations like proof blocks and lemma functions are even more out of reach.
Therefore,
we write a detailed prompt for GPT-4o, explaining the principles and tricks of writing Verus proof.
Designing these prompts took three Verus experts about 40 working hours.
By doing so, we finally manage to make GPT-4o synthesize proof annotations that allow Verus to prove
more than one thousand Rust functions at the cost of one whole month of non-stop GPT-4o invocation. Fortunately, this is sufficient for bootstrap. For the remainder of the self-evolving procedure, GPT-4o is not used any more.
Instead, we use an open-source LLM much smaller than GPT-4o to efficiently synthesize data and improve its capability in a self-evolving manner as in Algorithm 1.

To keep the self-evolving procedure moving forward, we have observed that it is important to allow the model to “debug” an
imperfect proof.
In many cases, the proof annotations generated by the model only contain small errors or miss one line of annotation, without
the capability of self-debugging, the model would start from scratch and fail to synthesize a perfect proof even after many
attempts.
Fortunately, we do not need to worry about lack of training data here:
“Thanks to” the incapability of LLMs in proof generation, a huge number of incorrect proofs are generated, which can be
re-purposed to fine-tune the proof generator on self-debugging tasks.
Specifically, for every Verus program $p$ (together with its specification) for which a perfect proof $P_{\checkmark}$ is
eventually synthesized in a round,
we denote those incorrect proofs generated before $P_{\checkmark}$ as $[P_{1},\dots,P_{n}]$.
For every incorrect proof $P_{X}\in[P_{1},\dots,P_{n}]$ , a triplet {$P_{X}$, Error${}_{P_{X}}$, $p_{\checkmark}$}
is added to our self-debugging dataset, where Error${}_{P_{X}}$ represents the verification errors Verus reported about
$P_{X}$.
Just in case too many similar incorrect proofs are generated,
we sample at most 10 incorrect proofs from $[P_{1},\dots,P_{n}]$ that have the same verification error to keep the
diversity of the training dataset.
Note that, in SAFE, we put the self-debugging dataset and proof dataset together to
fine-tune our model, which will be empowered to both generate proof from scratch and
repair an existing proof based on verification error messages for a Rust function and its specification.

## 4 Experiments

### 4.1 Experimental Setup

#### 4.1.1 Dataset

As an early exploration of automated formal verification, in this paper, we focus solely on the Rust code of algorithm types at the function level, as our source of data.
We employ the MBPP dataset (Austin et al., ) (only training split for data synthesis) and the CodeNet dataset (Puri et al., ) as our data sources. These two datasets contain small programs written in different programming languages, each of which is an intended
solution to a coding problem described in natural language and is associated with three test cases on average.
We translate the Python programs in MBPP and extract the Rust programs in CodeNet.
In total, we collect 45,395 Rust single-function programs.
Of these, 21,398 have been successfully transformed into Rust code that is compatible with Verus by SAFE.
We conduct the specification synthesis first, after two rounds of self-evolution, we obtain 19,017 high-quality specifications.
Then we run three rounds of self-evolving proof synthesis, ending with 9,706 verified programs, and 10,486 self-debugging data pairs.
To the best of our knowledge, this represents the most extensive synthetic dataset created for Verus code to date.

#### 4.1.2 Benchmark and Metrics

We assess the model’s proficiency in generating proofs in two benchmarks, the human-written benchmark VerusBench and the synthetic benchmark CodeNet-Test.

VerusBench is a human-written benchmark dataset with human-written Rust code and corresponding Verus specifications.
It contains 139 code files in total.
23 of them are algorithmic programs from Verus tutorials.
38 of them come from the dataset of SV-COMP-2021 (Beyer, ) (in short, SV) – a contest focused on program verification for C and Java languages; we utilize 38 Verus-translated tasks provided by (Yao et al., ).
The remaining 78 tasks come from MBPP-DFY-153 (Misu et al., ), a Dafny version of the MBPP test set.
We have translated 78 of them that are compatible with Verus.

CodeNet-Test is an expansive benchmark, 10x larger than VerusBench, crafted by LLM and encompassing 1,435 diverse tasks.
Given the substantial human effort required to write Verus code and specifications, it’s impractical to create a large test suite by human.
To comprehensively measure the model capability of generating proofs, we split a subset of CodeNet for testing,
ensuring it was not utilized in our data synthesis process. We leverage our specification generator to craft specifications for this subset and apply the same scoring mechanism to preserve reasonably well specifications.

We measure the capability of proof generation by Accuracy@K.
Specifically, we use our model to sample K proofs during proof generation, and for each incorrect sample, we sample K proofs generated during self-debugging, resulting in K * K debugged proofs.
For Accuracy@1, we use greedy decoding, which only generate 1 output, and for Accuracy@10, we sample 10 outputs with a temperature of 0.7.
Then, for each task in our benchmarks, Accuracy@K equals one if at least one proofs/debugged proofs is verified by Verus.

### 4.2 Evaluation Results

#### 4.2.1 Main Results

In Table 1, we compare the accuracy of SAFE with our baseline approaches.
Due to the inherent complexity of this task, there is no pre-existing fine-tuned model to serve as a baseline. We employ GPT-4o, DeepSeekCoder-33B-Instruct model (Guo et al., ) and Llama3.1-8B-Instruct model (Dubey et al., ) with basic prompts same as what we use for the fine-tuned models as our baselines. To offer some advantages
to the baselines,
we also feed four examples for in-context learning in these baselines, which we do not use for
SAFE fine-tuned
models.

We can see that SAFE achieves substantially higher accuracy compared to baseline approaches in both datasets and metrics.
In VerusBench benchmark, SAFE achieves an Accuracy@1 of 52.52% and an Accuracy@10 of 70.50% while the best of our baselines is 11.51% in Accuracy@1 and 24.46% in Accuracy@10.
We also measure the Accuracy@100 of SAFE to show the potential upper limit of our method.
DeepSeekCoder achieves the best performance of 79.14%.
With the long and carefully designed prompt, which was used to bootstrap SAFE proof synthesis, GPT-4o
is reasonably effective for VerusBench.
For the CodeNet-Test benchmark, we find the performance of baselines and prompt-based GPT-4o, denoted as
SAFE^0, drops significantly — by more than 10$X$ comparing with VerusBench, while SAFE doesn’t suffer as much.
It is important to note that CodeNet-Test is significantly larger and exhibits a distinct data distribution compared to VerusBench, the former is derived from competitive programming, whereas the latter encompasses common algorithms.
The results indict the prompt-based method has limited generalizability in automated proof generation, while SAFE no longer needs complicated prompts during inference.
We further report paired t-test (Hsu & Lachenbruch, ) results for Table 1 in Table 5 in Appendix.
As a result, by leveraging our self-evolving framework, SAFE can substantially improve the capability of open-source model, initially unacquainted with formal verification, and effectively generate proofs for Verus programs.

**Table 1: Accuracy of SAFE and baselines. SAFE^0 is GPT-4o with a long prompt that is used to bootstrap SAFE; SAFE is LLaMa3.1 or DeepSeekCoder with three rounds of finetuning and a simple prompt; SAFE+ allows a round of self-debugging beyond SAFE’s proof generation.**
| Benchmark | Accuracy | GPT-4o | LLaMa3.1 | DeepSeekCoder |  |  |  |  |  |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| Raw | SAFE^0 | Raw | SAFE | SAFE+ | Raw | SAFE | SAFE+ |  |  |
| VerusBench | @1 | 11.51 | 25.90 | 3.60 | 46.04 | 52.52 | 9.35 | 43.17 | 49.64 |
| @10 | 24.46 | 41.01 | 11.51 | 53.96 | 64.03 | 17.27 | 53.96 | 70.50 |  |
| @100 | - | - | - | 55.40 | 67.63 | - | 59.71 | 79.14 |  |
| CodeNet-Test | @1 | 0.28 | 2.86 | 0.00 | 44.32 | 48.50 | 0.21 | 43.83 | 48.43 |

**Table 2: Accuracy of SAFE models produced by each round (measured on VerusBench)**
| Self-<br>Evolving | Metric | Proof Generation | Self-Debugging |  |  |  |  |  |  |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| SV | MBPP | Tutorial | Total | SV | MBPP | Tutorial | Total |  |  |
| GPT-4o | Accuracy@1 | 39.47 | 19.23 | 26.09 | 25.90 | - | - | - | - |
| Accuracy@10 | 60.53 | 33.33 | 34.78 | 41.01 | - | - | - | - |  |
| Round 1 | Accuracy@1 | 55.26 | 29.49 | 4.35 | 32.37 | 57.89 | 30.77 | 4.35 | 33.81 |
| Accuracy@10 | 81.58 | 30.77 | 13.04 | 41.73 | 81.58 | 30.77 | 13.04 | 41.73 |  |
| Round 2 | Accuracy@1 | 73.68 | 29.49 | 34.78 | 42.45 | 84.21 | 38.46 | 39.13 | 51.08 |
| Accuracy@10 | 89.47 | 30.77 | 47.83 | 49.64 | 92.10 | 56.41 | 52.17 | 65.47 |  |
| Round 3 | Accuracy@1 | 78.95 | 30.77 | 26.09 | 43.17 | 81.58 | 41.03 | 26.09 | 49.64 |
| Accuracy@10 | 92.11 | 35.90 | 52.17 | 53.96 | 97.37 | 58.97 | 65.22 | 70.50 |  |

#### 4.2.2 Benefits from Self-Evolving

In Table 2, we use the performance on VerusBench to show how our self-evolving framework improves the capability of models. In this set of experiments, we
use DeepSeekCoder-33B-Instruct for data synthesis and fine-tuning; Round 1, 2, 3 represent three models
fine tuned from DeepSeekCoder-33B-Instruct.
Table 2 illustrates that for every subset of VerusBench,
the best Accuracy@1 and Accuracy@10 scores are achieved at the last two rounds of model evolution, which indicts the effectiveness of self-evolution.
Besides, the round 1 model with a simple prompt already outperforms GPT-4o with a much more
sophisticated prompt for all but the “Tutorial” subset.
Round 3 model outperforms Round 2 model in terms of Accuracy@10 for all subsets of tasks, with or without self-debugging.
Meanwhile, the improvement from Round 2 to Round 3 is much smaller than the improvement from GPT-4o to Round 1, and from Round 1 to Round 2, which justifies our decision of stopping the self-evolution after three rounds.
We further report paired t-test results for Table 2 in Table 6 in Appendix.

Finally, the Round 3 model greatly outperforms GPT-4o for all three sub-sets of VerusBench, even though GPT-4o uses a much more sophisticated
prompt: GPT-4o was most effective for the SV subset with a
39.47% Accuracy@1, while Round 3 model improves that metric to 78.95% (81.58% with self-debugging); GPT-4o was
the least effective for the MBPP subset with a 19.23% Accuracy@1, which is improved by Round 3 model to 30.77%
(41.03% with self-debugging).
This trend bolds well for SAFE to work with different datasets and different bootstrapping methods in the
future.

#### 4.2.3 Improvement of Self-debugging

Table 1 demonstrates that SAFE+, which allows LLMs to do self-debugging, substantially improves the accuracy compared to direct generation, indicting the effectiveness of the self-debugging mechanism.
In Table 2, self-debugging mechanism shows consistent improvements in all the three components of VerusBench.
As we show in Listing 2 of the Appendix, Verus provides error messages for any incorrect proof about which
proof annotation, which part of the specification, or which implicit proof target
(e.g., no overflow for every arithmetic expression) cannot be
verified, which can
help repair the proof for experienced human users and well trained models.

Decoding Strategies for Self-Debugging.
From Table 1, we can see the enhancements of self-debugging become more significant with the increase in the number of sampled outputs.
To further evaluate how decoding strategies affect the performance of self-debugging in VerusBench, we conduct four settings by combining greedy and sampling decoding during the generation and debugging phases, and run two more self-debugging rounds with greedy decoding.
Figure 2 shows that more rounds of self-debugging hardly improve the accuracy, with the improvement less than 1%.
Besides, sampling decoding strategy is more useful for generation phase rather than for the self-debugging process. Notably, the “sampling+greedy” (generate multiple proofs and for each incorrect proof generate one debugged proof) strategy outperforms the “greedy+sampling” (generate one proof and generate multiple debugged proofs) setting.

Figure: (a) LLaMa
Refer to caption: x2.png

#### 4.2.4 Impact of Specification Quality

As mentioned in Section 3.2, we only keep specifications with high Correctness scores
and reasonably high Completeness scores.
To investigate the impact of this design decision, we zoom into the last round of proof-synthesis model
fine-tuning to see how the quality of proof-synthesis model can be affected by the quality of specification dataset.
Specifically, the current Round-3 SAFE model is obtained by fine-tuning the Round-2 SAFE model using
correct proof synthesized by the bootstrapping model, the Round-1 model, and the Round-2 model based on the specifications $S$
selected by
SAFE, denoted as
$\mathbf{P_{0}[\mathbf{S}]}\cup\mathbf{P_{1}[\mathbf{S}]}\cup\mathbf{P_{2}[
\mathbf{S}]}$ ($\mathbf{P}_{i}[\mathbf{S}]$ denotes
all the correct proofs synthesized in round $i$ based on specification set $S$). In our two alternative settings, we go back to the set of
all specifications synthesized during the spec-synthesis self-evolving procedure and randomly sample a set of specifications
$S*$ that have the same size as $S$; naturally $S*$ contains many low-quality specifications that do not pass our Correctness and Completeness
threshold. In our alternative setting of ‘Round 2 w/ mix-quality’, we obtain a model by fine-tuning the Round-2 SAFE model using
$\mathbf{P_{0}[\mathbf{S}]}\cup\mathbf{P_{1}[\mathbf{S}]}\cup\mathbf{P_{2}[
\mathbf{S*}]}$; in our alternative setting of ‘low-quality spec-input’,
we obtain a model by fine-tuning the original DeepSeekCoder using $\mathbf{P_{2}[\mathbf{S*}]}$ alone.

From the results in Table 2, we can see that high-quality specifications contribute substantially to the end-to-end effectiveness of SAFE.
If the model is trained without any high quality data (‘low-quality spec-input’), the accuracy drops for all three subsets of VerusBench and
even drops to 0% Accuracy@1 and 5.26% Accuracy@10 for SV. Probably because more debugging data is created in this setting, the
self-debugging feature helps more for this setting, but the overall accuracy still lags way behind the default SAFE Round-3 model.
When low quality data is mixed with high quality ones, the performance still drops as shown in the
‘Mixed-Quality’ row in the table.
In Appendix, we further report paired t-test results for Table 3 in Table 7, and provide an example Rust program (Listing 14) whose low quality specification led to an extremely simple proof — this simple proof probably offered no benefit for proof-synthesis fine-tuning.
In conclusion, specification selection matters to the fine-tuning and the evolution of proof-synthesis models.

**Table 3: Accuracy drop of proof synthesis w/ training-specification quality drop (on VerusBench)**
| Model | Metric | Proof Generation | Self-Debugging |  |  |  |  |  |  |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| SV | MBPP | Tutorial | Total | SV | MBPP | Tutorial | Total |  |  |
| SAFE | Accuracy@1 | 78.95 | 30.77 | 26.09 | 43.17 | 81.58 | 41.03 | 26.09 | 49.64 |
| Round 3 | Accuracy@10 | 92.11 | 35.90 | 52.17 | 53.96 | 97.37 | 58.97 | 65.22 | 70.50 |
| DSCoder | Accuracy@1 | 0.00 | 29.49 | 4.35 | 17.27 | 0.00 | 43.59 | 21.74 | 28.06 |
| fine-tuned | $\Delta(-\mbox{ Round 3})$ | (-78.95) | (-1.28) | (-21.74) | (-25.9) | (-81.58) | (+2.56) | (-4.35) | (-21.58) |
| w/ low-quality | Accuracy@10 | 5.26 | 32.05 | 21.74 | 23.02 | 15.79 | 50.00 | 47.83 | 40.29 |
| spec-input | $\Delta(-\mbox{ Round 3})$ | (-86.84) | (-3.85) | (-30.43) | (-30.94) | (-81.58) | (-8.97) | (-17.39) | (-30.22) |
| Round 2 | Accuracy@1 | 36.84 | 30.77 | 17.39 | 30.22 | 42.11 | 43.59 | 21.74 | 39.57 |
| Model | $\Delta(-\mbox{ Round 3})$ | (-42.11) | (-0.00) | (-8.7) | (-12.95) | (-39.47) | (+2.56) | (-4.35) | (-10.07) |
| fine-tuned | Accuracy@10 | 65.79 | 32.05 | 30.43 | 41.01 | 71.05 | 51.28 | 52.17 | 56.83 |
| w/ mix-quality | $\Delta(-\mbox{ Round 3})$ | (-26.32) | (-3.85) | (-21.74) | (-12.95) | (-26.32) | (-7.69) | (-13.04) | (-13.67) |

## 5 Conclusion

In this paper, we propose SAFE, a novel self-evolving framework to advance automated proof generation for Rust.
SAFE alleviates the severe data lack challenge by coupling data synthesis and model fine-tuning in a self-evolving manner, demonstrating superior efficiency and precision compared to relying solely on GPT-4o.
Through ten of thousands of synthesized proofs and the self-debugging mechanism, we improve the capability of open-source models, initially unacquainted with formal verification, to automatically write proof for Rust code.
Our evaluation shows that SAFE leads to a significant improvement over GPT-4o,
more than doubling the accuracy of GPT-4o for a human-curated benchmark set and an
even bigger advantage on a large LLM-crafted benchmark set.

## Appendix A Verus Examples

Figure: Listing 2: An imperfect proof of binary search with its error message recieved from Verus.

Figure: Listing 3: The proof code of fibonacci.

Imperfect proof example. An imperfect proof annotation of binary search is shown in Listing 2. Compared with the correct version in Listing 1, this imperfect proof lacks a crucial loop invariant in Line 20.
According to the error messages following the code, we can see, a postcondition cannot be proved without this loop invariant.
Furthermore, the absence of this invariant causes Verus failing to prove the absence of arithmetic underflow/overflows.
Specifically, this loop invariant states that value k exists in v[i1 .. i2]. Without this loop invariant,
Verus cannot reason about the comparison between v[ix] and k on line 24, and hence cannot reason about how
the values of i1 and i2 would change in this loop. This then leads to Verus’ failure in reasoning about the
bound of i2 - i1 on line 23 (and hence the arithmetic underflow/overflow error), and the final value of i1 on line 30
(and hence the postcondition not satisfied error).

More complicated proof annotations.
Listing 3 shows much more complicated proof annotations for a Rust function that computes
the fibonacci sequence.
The proof for this code includes not only loop invariants which were introduced in Listing 1,
but also a proof function (Line 16–29 in the listing), a proof block (Line 53–55),
and assert statements (Line 27) that are used to provide
hints to the underlying theorem prover. This example comes from the Verus paper (Lattuada et al., ), with more detailed explanation
available in that paper.

## Appendix B Prompts

Figure: Listing 4: SAFE’s prompt for proof generation.

Figure: Listing 5: SAFE’s prompt for self-debugging.

Figure: Listing 6: GPT-4o’s prompt for proof generation.

## Appendix C Implementation Details

### C.1 Specification Filtering

Listing 7 shows an example of how we leverage test cases and Verus’ symbolic reasoning
capability to quickly score and filter specifications.
For each function with a synthesized specification (i.e., Line 6–8 in Listing 7, in order to know whether
this specification is consistent with a test case $t$, we do the following: 1)
we replace the function body with Verus’ assume statements. Each assume
tells Verus about the value of one input or output variable (these values come from the test case $t$);
2) when an input/output variable is a container, several assert statements are inserted to make sure
the underlying theorem prover can correctly reason about the value of every element in the container; 3) Verus is invoked
to prove this function. If the specification is consistent with this test case, verus verification would succeed; otherwise,
verus verification would fail.

As mentioned in the paper, to evaluate the completeness of a specification, we mutate existing test cases to see if
incorrect test cases can be rejected by a specification.
In this example, we mutate the output in the ground truth by adding a new value $15$ into $result$ vector.
In this case, Verus will report that the post-condition on Line 7 fails because $15$ does not exist in vector $a$.
If a synthesized specification does not contain something like Line 7, this mutated test case will likely point out the
incomppleteness of that specification.

In our experiments, we take 5 ground truth test cases and 20 mutated wrong test cases on average for scoring. We filter out all the specifications that have a score lower than 0.8 in correctness or 0.6 in incompleteness. To avoid too many specifications preserved for single program, we allow at most three specifications to be preserved for a single function.

Figure: Listing 7: An example used for scoring and filtering based on test cases.

### C.2 Statistics of Synthesized Data

As explained earlier in the paper, we obtained 45,495 Rust single-function programs from MBPP training set and CodeNet dataset.
After translating them into Verus-compatiable Rust programs, we have 21,398 programs left for specification synthesis.
The statistics of all synthesized data in different round of our self-evolution process in shown in Table 4.
Note that, at the very beginning, we put aside a random subset of CodeNet Rust programs aside to use for the evaluation of
SAFE. Those programs do not participate in the fine-tuning and are not included in the numbers shown in Table 4.

In round 0, we employ GPT-4o to synthesize specification, retaining only the verified Rust functions along with their specifications.
This process was time-consuming, taking an entire month to synthesize 3,673 verified programs.
Even with our designed prompts, GPT-4o needs to sample 20–30 times for a single program on average.
We then use the synthesized specifications to bootstrap the self-evolving specification synthesis process, which is conducted over two rounds. In each round, we leverage the fine-tuned model to generate specifications for all 21k Verus programs and select the high quality ones for further fine-tuning. At the end, we use the selected 19,017 specifications as inputs for the proof synthesis procedure.
The numbers of verified programs and debugging fine-tuning triplets are also shown in Table 4.
As we can see, as many as 9,706 verified programs and 10,486 debugging data are produced after Round-2 model and are used to
fine-tune the Round-3 model, the final proof-synthesis model.

**Table 4: Statistics of synthesized data**
|  | Verus programs | All specs | Selected specs | Verified programs | Debugging data |
| --- | --- | --- | --- | --- | --- |
| Seed | 21,398 | - | - | - | - |
| Round-0 | - | - | 3,673 | 3,673 | 0 |
| Round-1 | - | 102,549 | 16,530 | 8,368 | 9,910 |
| Round-2 | - | 117,759 | 19,017 | 9,706 | 10,486 |

### C.3 Training Hyperparameters

Bootstrapped by 3,673 verified programs synthesized by GPT-4o, we employ the DeepSeekCoder model (Guo et al., ) as the generator in the self-evolution procedure. We run the self-evolving specification generation and auto-proving process multiple rounds. For specification generation, we run two rounds. Proof generation is three. At each round of fine-tuning, we combine the verified programs and self-debugging data pairs together as training data, and train DeepSeekCoder 5 epochs, using a batch size of 128 and a learning rate of $1\times 10^{-5}$.

## Appendix D Additional Experiments

### D.1 Statistics of VerusBench

Figure 3 illustrates the token number distributions of specifications and proofs in VerusBench.
For preconditions, in Figure 3, we show that SV’s average token number is substantially larger than that of MBPP and Tutorial.
In contrast, SV’s average token number is substantially smaller than the rest two as shown in Figure 3.
Such statistics can, to some extent, reflect the difficulty of three components in VerusBench, i.e., SV is relatively easiler than the rest two.
When comparing the human-written proof annotations for MBPP and Tutorial programs in VerusBench, Figure 3 shows that the average token number of proof annotations in MBPP is larger than that of Tutorial, although there are some outliers.

Figure: (a) The token number’s distribution of preconditions
Refer to caption: x4.png

### D.2 Results of Statistical Significance Testing

SAFE Compared to Raw Models.
Table 5 shows the p-values between SAFE under various settings and its base models.
We highlight p-values that are larger than 0.05 in italics.
From this table, we can observe that the p-values of all fine-tuned models (LLaMa and DeepSeekCoder) are less than 5E-7, indicating the significant improvement of SAFE.

**Table 5: The p-values of SAFE’s accuracy compared to raw models, non-significant data ($p>0.05$) points are pointed out in Italics**
| Benchmark | Accuracy | GPT-4o | LLaMa3.1-8B-Instruct | DeepSeekCoder-33B-Instruct |  |  |
| --- | --- | --- | --- | --- | --- | --- |
| SAFE | SAFE | SAFE+ | SAFE | SAFE+ |  |  |
| VerusBench | Accuracy@1 | 2.01E-03 | 4.68E-11 | 3.88E-14 | 2.34E-09 | 6.33E-13 |
| Accuracy@10 | 4.69E-03 | 5.39E-07 | 5.23E-12 | 5.39E-07 | 1.53E-15 |  |
| Accuracy@100 | - | 8.67E-31 | 9.25E-45 | 2.45E-34 | 5.15E-64 |  |
| CodeNet Test | Accuracy@1 | 0.08 | 2.26E-122 | 1.07E-24 | 1.54E-142 | 1.51E-215 |

Comparison between Various Rounds of Self-Evolving.
Table 6 shows the p-values of SAFE’s accuracy between various rounds of self-evolving.
We highlight p-values that are larger than 0.05 in italics.
When compared to round 1, round 2 and round 3 show significant improvement in Accuracy, especially after self-debugging.
Additionally, we also show that there is insignificant improvement between round 2 and round 3 except the accuracy in Tutorial after self-debugging.
Thus, three rounds of self-evolution is sufficient for our approach.

**Table 6: The p-values of SAFE’s accuracy between various rounds of self-evolving, non-significant data ($p>0.05$) points are pointed out in Italics**
| Paired T-Test<br>Rounds | Metric | Proof Generation | Self-Debugging |  |  |  |  |  |  |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| SV | MBPP | Tutorial | Total | SV | MBPP | Tutorial | Total |  |  |
| Round 1 & 2 | Accuracy@1 | 1.09E-03 | 1.00 | 4.40E-11 | 0.06 | 6.66E-07 | 0.17 | 2.74E-13 | 2.30E-03 |
| Accuracy@10 | 0.06 | 1.00 | 9.14E-11 | 0.15 | 7.97E-03 | 1.00E-05 | 5.24E-13 | 3.60E-05 |  |
| Round 1 & 3 | Accuracy@1 | 2.19E-05 | 0.79 | 3.04E-07 | 0.06 | 1.36E-05 | 0.06 | 3.04E-07 | 4.98E-03 |
| Accuracy@10 | 7.97E-03 | 0.37 | 5.24E-13 | 4.12E-02 | 1.67E-05 | 1.70E-06 | 1.17E-21 | 9.11E-07 |  |
| Round 2 & 3 | Accuracy@1 | 0.33 | 0.79 | 0.12 | 1.00 | 0.53 | 0.63 | 2.10E-02 | 0.81 |
| Accuracy@10 | 0.41 | 0.37 | 0.47 | 0.55 | 0.06 | 0.72 | 2.86E-02 | 0.44 |  |

Comparison between SAFE’s Accuracy with Low/High Quality Specifications.
Table 7 shows the p-values of SAFE’s accuracy between round 3 and low quality ones.
We highlight p-values that are larger than 0.05 in italics.
We show that in most scenarios (except Accuracy@1 in round 2 + low quality specifications), low quality specifications might leads to a significant decrease in terms of SAFE’s end-to-end effectiveness.

**Table 7: The p-values of SAFE’s accuracy with low quality specifications, compared to round 3 with high quality ones, non-significant data ($p>0.05$) points are pointed out in Italics**
| Data Source | Metric | Proof Generation | Self-Debugging |  |  |  |  |  |  |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| SV | MBPP | Tutorial | Total | SV | MBPP | Tutorial | Total |  |  |
| DSCoder fine-tuned<br>w/ low-quality spec-input | Accuracy@1 | 5.15E-64 | 0.79 | 3.04E-07 | 3.22E-06 | 3.62E-71 | 0.72 | 0.40 | 1.98E-04 |
| Accuracy@10 | 4.04E-87 | 0.53 | 9.39E-08 | 5.38E-08 | 8.66E-71 | 0.15 | 3.26E-03 | 4.79E-07 |  |
| Round 2 Model fine-<br>tuned w/ mix-quality | Accuracy@1 | 1.94E-13 | 1.00 | 8.07E-02 | 2.45E-02 | 1.71E-12 | 0.72 | 0.40 | 0.07 |
| Accuracy@10 | 2.78E-08 | 0.53 | 2.27E-04 | 3.05E-02 | 5.34E-10 | 0.23 | 2.86E-2 | 2.51E-02 |  |

### D.3 Case Studies

#### D.3.1 SAFE’s Advantages Compared to GPT-4o

To demonstrate the effectiveness of SAFE, we show an example proof generated by GPT-4o without our prompts and SAFE in Listing 8 and Listing 9, respectively.

In Listing 8, GPT-4o introduces four loop invariants, specifying that (1) the index variable i does not exceed the length of input array xlen; (2) the length of the input array remains during the loop; (3) the values of the first i elements are equal to their original values plus 4; (4) the values of the rest elements are equal to their original values.
However, GPT-4o neglects to include proofs to address the potential arithmetic underflow/overflow, thus leading to the errors reported in Lines 30-64.

In contrast, SAFE addresses this error and successfully generates a correct proof for this program.
Listing 9 shows a correct proof generated by SAFE (DeepSeekCoder).
Compared to GPT-4o’s proof, it adds another loop invariant in Line 19 pointing out that the original values of the input array are less than or equal to 0x7FFFFFFB, thus addressing the arithmetic underflow/overflow error.
SAFE’s effectiveness mainly credits to our self-evolution framework.

Figure: Listing 8: An incorrect proof of $myfun2$ generated by GPT-4o.

Figure: Listing 9: The correct proof of $myfun2$ generated by SAFE.

#### D.3.2 The Effectiveness of Our Self-Debugging Mechanism

Figure: Listing 10: An incorrect proof of $is_sorted$ generated by SAFE before self-debugging.

Figure: Listing 11: The correct proof of $is_sorted$ fixed by SAFE after self-debugging.

In Listing 10 and Listing 11, we demonstrate the effectiveness of our self-debugging mechanism during proof synthesis with another example.
This example program checks whether a given array is sorted by checking whether there exists a pair of adjacent elements where arr[index] > arr[index + 1].

Listing 10 shows the initial proof generated by SAFE, which includes loop invariants: (1) the index does not exceed the length of the given array; (2) all elements before the current index satisfy the ‘‘sorted’’ property.
However, during each iteration of this loop, this program checks the current element against the next one and terminates the loop when index equals arr.len() - 2.
As a result, the loop invariants fail to account for the last element, leading to the error described in Lines 29-41.

SAFE successfully fixes this error via self-debugging.
The error message clearly indicates that the loop invariant forall |i: int, j: int| 0 <= i < j < index cannot be
verified.
Using this feedback from Verus, SAFE modifies the boundary condition in that loop invariant, i.e., the ranges of the variable i and j in that invariant. The adjusted invariant forall |i: int, j: int| 0 <= i < j < index + 1
allows Verus to successfully finish the proof.

#### D.3.3 Limitations

We reported that SAFE failed to generate correct proof for 20.86% of the programs in VerusBench, even after sampling 100 proofs and 100 debugged proofs for each incorrect proof (i.e., Accuracy@100).
In Listing 12 and Listing 13, we analyze an example where SAFE fails to generate a correct proof.
This program removes odd numbers from a given array by scanning the input array arr and appending the even numbers to a new array, even_list.

Listing 12 shows that SAFE successfully generates the main structure of the proof, verifying that the elements in even_list correspond to the even elements in the first index elements of arr.
However, Verus reports errors indicating that the loop invariants are not satisfied both before and after the loop (Lines 34-44 in Listing 12).
Even under the Accuracy@100 setting, where 100 * 100 debugged proofs are generated, SAFE encounters similar errors, and fails to generate a correct proof.

The root cause of this error is that proving this program needs to add assert statements and leverage the reveal
feature of Verus (Doc, ).
We suspect the reveal feature was never synthesized in any finetuning dataset, so the final SAFE model
also lacks sufficient domain knowledge to prove this program.
This limitation can be substantially mitigated by incorporating a larger and more diverse training set during the initial round of self-evolution.

Figure: Listing 12: An incorrect proof of $remove$_$odds$ before and after self-debugging.

Figure: Listing 13: The ground truth proof of $remove_odds$.

#### D.3.4 An Example Proof with a Low-Quality Specification

In Section 4.2.4, we demonstrate that the quality of specifications contribute substantially to the end-to-end effectiveness of SAFE.
Listing 14 presents an example proof with a low-quality specification.
This program computes the greatest common divisor of two integer number using the Euclidean Algorithm.
However, this specification merely requires that the result be greater than zero, ‘‘result > 0’’, without ensuring that the result should be divisors of both inputs a and b.

Programs with such low-quality specifications might lead to extremely simple proofs, which are very different from proofs in more
realistic tasks.
For example, the proof annotations synthesized in Lines 16-17 simply copy the function pre-condition — a > 0 and b >= 0.
For more realistic tasks, proofs can rarely get done this way. Consequently, putting many proofs with this quality
(i.e., all resulted from low-quality specifications) into the fine-tuning dataset does not help model’s evolution.

Figure: Listing 14: An example proof of $gcd$ with a low quality specification.

## Peer Reviews

confidence: 4
contribution: 3
initial_rating: 6
presentation: 2
questions: Please address the points raised in the “Weakness” section.
soundness: 3
strengths: This paper studies automating proof generation in formal program verification with LLMs, an important direction with great potential for practical applications. The focus is on Rust, a relatively new language that is gaining widespread adoption. Although synthetic data generation for fine-tuning LLMs is not a completely novel idea, the paper introduces a few interesting techniques for the domain of proof generation for Rust. I particularly like the metric for filtering high-quality specifications. The evaluation is thorough, demonstrating the benefits of SAFE over baselines and the effectiveness of its individual components.
summary: This paper proposes SAFE, a data generation and fine-tuning procedure for improving LLMs in generating proofs for the correctness of Rust code. SAFE consists of three stages: (i) verus-compatible code generation, (ii) self-evolving specification synthesis, and (iii) self-evolving proof synthesis. During stage (ii), SAFE leverages a symbolic and quantitative measure based on the correctness and completeness of the specification. For stage (iii), SAFE fine-tunes both proof generation and repair models. The experiments demonstrate the advantages of SAFE: it significantly improves the performance, compared to both the base model and GPT-4o.
weaknesses: The paper only focuses on small programs in the style of MBPP and CodeNet. Although I understand this is partly due to the limitation of the Verus tool, I do believe that the paper should present some case studies or discussion on how to scale the approach to real-world software projects.

Apart from proof generation, a major part of formal verification is writing the specifications. The paper covers mechanisms to fine-tune a “good” specification generation. It would strengthen the paper if more evaluation can be done on the specification generation task and how it can be combined with proof generation to automate end-to-end verification.

The paper lacks a study on the choice of the correctness and completeness thresholds for the specification metric.

The paper writing can be improved. Below are some issues I found or some recommendations:
- The text in Section 3 is sometimes ad-hoc and contains low-level details (e.g., choice of parameters). I would be helpful to revise the text to be more formal and move the details to later sections.
- Line 289: The paper says “much previous work relies on running many test cases” without providing any references.
- Line 519: Table 2 should be Table 3
- Table 3: The split of model names to multiple lines is confusing. I thought one line of text corresponds to one single baseline. The $\Delta$ rows look redundant as well.

---

confidence: 4
contribution: 3
initial_rating: 6
presentation: 3
questions: 1. A clarifying question about the self-evolving data: The data collected through GPT-4o (round 0) is used to fine-tuned the first specification/proof generation model. What's the data input used to let the generation model generate data for then next round? 
* Are these data the same programs as those used in the generating round 0 data? If this is the case, would the training data in each round kind of repetitive and lack of diversity?
* Or does author use some strategies to leave some unique programs for each round, so that the fine-tuning data for each round contains different programs?
2. Self-debugging is quite effective and improves the accuracy, how does the model obtain the ability of self-debugging? does the fine-tuning procedure contains self-debugging training data?
3. Why are the baseline models prompted with 4 examples instead of more examples?
soundness: 3
strengths: 1. This paper proposes a novel approach that use self-evolving to iteratively improve LLM's ability of generating Rust specification and proofs. The fact that this approach does not rely on larger LLM such as GPT-4o in the following iterations (except the first round) makes it more generalizable and scalable.
2. The proposed approach shows great effectiveness, with three round of self-evolving, the fine-tuned LLM shows about 40% higher accuracy@1 compared to the prompting approach.
3. Comprehensive analysis and experiments, showing that each round of 1, 2 and 3 brings some improvement to the fine-tuned LLM (although the round 2 model is better than the round 3 model under some settings), and showing that high-quality specifications important to improve the model's accuracy during self-evolving.
summary: This paper introduces SAFE, an innovative framework designed to address the challenges of automated proof generation for Rust code, SAFE overcomes the significant data scarcity issue ( i.e., there is far less proof data than code data for training language models) by using a self-evolving approach to synthesize specification/proof data and fine-tune models iteratively. SAFE operates through a feedback loop where synthesized proofs are continuously verified by a symbolic verifier, distinguishing correct from incorrect proofs. Incorrect proofs are used to train the model's self-debugging ability, while the correct proofs are used to improve the model for the next round. The design of the approach is smart and uses the insight that (1) using a quantitative metric to select high-quality specifications for fine-tuning; (2) we only need reasonably well, instead of perfect specifications to fine-tune in the next step; and (3) Verus can quickly tell correct proof from incorrect ones, which enables the collecting and filtering of large amount of data.

SAFE achieves a substantial improvement, attaining a 70.50% accuracy on a benchmark set crafted by human experts, a notable advancement over GPT-4o's performance of 24.46%. SAFE also obtains self-debugging ability using the incorrect proofs collected during the data collection step. Experiments show that each round of self-evolving improves the accuracy of SAFE, and proves the importance of using high-quality training data.
weaknesses: 1. The self-debugging ability is shown to be only effective for the first time, what could be potential approach for improving the self-debugging ability in the following rounds?
2. I am wondering if this self-evolving approach can improve smaller LLMs ability. For instance, if the backbone is DeepSeekCoder-1.3B, how effective is the self-evolving approach?

---

confidence: 4
contribution: 4
initial_rating: 8
presentation: 4
questions: Please provide a short statement or clarification to the points raised above.
soundness: 4
strengths: - The paper is well-written and nicely structured. The figures and tables are well formatted and legible.
- The story is engaging and the tackled topic highly relevant.
- The results are clearly presented and provide interesting insights.
summary: The presented paper proposes a method to bootstrap training data for generating proofs of Rust code using LLMs. The pipeline starts from a small set of curated programs and gradually evolves using the verifier as signal for dataset curation. Finally they evaluate the resulting fine-tuned LLM and show state of the art results on a difficult dataset of low-resource correctness proofs.
weaknesses: - In Table 1 the Accuracy of GPT-4o on VerusBench @100 is unfortunately missing (likely due to high inference cost?). Similarly the result of DeepSeekCoder RAW @100 is missing. If the authors could provide these values, the tables would provide a much more complete picture.
- In Table 2, Round 3 appears to severely degrade performance of the resulting model on the Tutorial dataset. Does this constitute some first signs of overfitting or collapse or could the authors provide some more insight on what is happening here? It might be interesting to provide some basis on deciding where to stop the iterative process.
- There is no discussion of Limitations. While the provided method is clearly powerful some discussion on potential limitations would be highly appreciated.

---

confidence: 4
contribution: 4
initial_rating: 5
presentation: 2
questions: - In table 2 you report a "total" column; I noticed the numbers don't add up if you just take the mean of the other columns, so I presume what you're actually doing is taking the mean over all of the samples in the entire dataset? (I think that's what you want to do, I just want to make sure I understood correctly).
- When constructing training data for the repair task, are you doing any filtering to make sure that the "incorrect program" is actually similar to the "correct program", or could they be completely different?
- What is the difference between SAFE and expert iteration, other than your synthetic data generation for the specifications?
soundness: 2
strengths: I think the core ideas in this paper are very interesting, and that there are several good contributions here:
- Filtering the specifications based on a symbolic, deterministic score computed from the tests seems like the right thing to do, and I appreciate the brief ablation study of the impact of this step (section 4.2.4).
- The experiment in 466-474 provide further evidence for previous findings in the code generation literature about "sampling+greedy" self-debugging outperforming "greedy+sampling" (I recommend that the authors consider explicitly comparing these results to e.g. [1, 2]).
- Perhaps most importantly, verifying Rust code is not only potentially impactful but also (as far as I know) a completely novel task; kudos to the authors for going through the effort to collect all the data.


[1] 
Teaching Large Language Models to Self-Debug
Xinyun Chen, Maxwell Lin, Nathanael Schärli, Denny Zhou.
International Conference on Learning Representations (ICLR), 2024.

[2] 
Is Self-Repair a Silver Bullet for Code Generation?
Theo X. Olausson, Jeevana P. Inala, Chenglong Wang, Jianfeng Gao, Armando Solar-Lezama.
International Conference on Learning Representations (ICLR), 2024.
summary: This paper seeks to finetune a code-generating LLM to generate verification annotations for code.
Specifically, the authors target Verus, which is an SMT-backed automated-theorem-proving-style verifier for Rust code.
The key technical challenge that the authors thus need to overcome is that ths is a very low resource language,
so simple techniques such as finetuning aren't directly applicable; and even API-backed models do so poorly
on this task that naively distilling wouldn't help, either.
Instead, the authors basically bootstrap the finetuning process as follows:
- First, they generate a set of proof *specifications* for some Rust programs using GPT-4o. They then filter out specs which are "low quality", e.g. those which are always true.
- Then, they use these specifications to generate (against using GPT-4, with some expert-crafted task-specific prompts) proof *annotations* for a small subset of these specifications.
- Finally, they bootstrap a finetuning process from these initial annotations, training in each round the open-source model on the correct proofs it generated in the last round.
There's some additional bells and whistles, such as also training on incorrect proofs by framing it as auxiliary repair task, but I believe this summarizes the core idea.

In terms of the experiments, the authors share results both for a small, human-written benchmark and for GPT-transpiled versions of MBPP and SV.
At first glance I was a bit worried about the scale of this data, but given the novelty of the task and the relative lack of Rust datasets in the literature I actually commend the authors on their effort to collect as much data to evaluate on as possible.
weaknesses: There are a few rather major flaws that make me hesitant to recommend the paper for acceptance in its current format.

One is that I find that the paper tries a little bit too hard to sell the novelty of this "SAFE" approach.
Bootstrapping finetuning of LLMs by interleaving it with search has been done before; most people call it "expert iteration" [3] (authors: please correct me if you think there is a *significant* difference between your method and this).
Especially what you call "SAFE_0" feels a bit rich: unless I am mistaken, you are literally just doing synthetic data generation with GPT-4o and filtering the results based on some measure of quality.
Also, on line 359 you say "21,398 [programs] have been successfully transformed [...] by SAFE"; unless I'm mistaken you mean "by GPT-4" here, because at this point you haven't done anything other than asking GPT to first transpile the code to Rust and to then transpile the Rust code into the subset of the language that is supported by Verus.

I would encourage the authors to tone down the language a bit more and focus on the actually novel parts of this paper, which I believe to be: the task target; finetuning on repair tasks to improve generation performance; and the metric used to filter the specification samples.

A more important issue is that I do not think the comparison to the baselines is fair in its current form for the "SAFE+" method.
The authors themselves point out that in this variation (i.e., when you do a round of self-debugging if the initial generation does not succeed), they generate `k * k` repair samples - how can you then compare against pass@1? You have actually drawn `k + k*k` samples from the model, so you should at least compare against a baseline of `pass@(k + k*k)`.
This is an issue that has come up again and again the self-debugging/refinement literature, and I once again encourage the authors to engage with that literature.
You still have good results here - for example, the SAFE+ pass@10 is substantially higher than the SAFE pass@100 on VerusBench - but the way you're currently presenting them overstates their significance.

Finally, the writing could use some more proof reading, especially the abstract and the introduction (but this is a minor complaint).


[3] 
@misc{polu2022formalmathematicsstatementcurriculum,
      title={Formal Mathematics Statement Curriculum Learning}, 
      author={Stanislas Polu and Jesse Michael Han and Kunhao Zheng and Mantas Baksys and Igor Babuschkin and Ilya Sutskever},
      year={2022},
      eprint={2202.01344},
      archivePrefix={arXiv},
      primaryClass={cs.LG},
      url={https://arxiv.org/abs/2202.01344}, 
}

Meta-review: This paper considers learning how to prove the correctness of Rust programs, an important programming language for which there is very little training data, by bootstrapping both specifications and proofs. This problem is more broadly emblematic of the need to produce verified code for low resource languages, potentially even low resource areas of math (though not explored in the paper). The primary strength is that the method is creative, potentially high impact, and has good empirical results. The primary weakness is that it only considers proofs for MBPP-style problems, and required nontrivial manual effort to bootstrap the system (while also relying on automated general-purpose methods). I recommend acceptance because this weakness is understandable given that this would only be the first step in this research program, and because it is both conceptually interesting and practically relevant to machine learning and formal methods.

Decision: Accept (Poster)