AutoVerus: Automated Proof Generation for Rust Code

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

GPT-4o often tries to create a Verus sequence using !seq[...] or access the first x elements with seq[..x], both of which are invalid for the Verus Seq data type.

“For instance, GPT-4o often tries to create a Verus sequence using !seq[...] or access the first x elements with seq[..x], both of which follow Rust syntax but are invalid for Verus Seq data type.”

May combine two claims.

The AutoVerus framework works with GPT-4o, GPT-4-turbo, and Deepseek-R1, all achieving similar results.

“The AutoVerus framework, including its three-phase proof generation methodology and proof filtering, ranking, merging support, works well with different LLM models: GPT-4o, GPT-4-turbo, and Deepseek-R1 all achieve similar results, with DeepSeek-R1 proving slightly fewer tasks than GPT-4o/turbo, and GPT-4-turbo spending more time in proving the same number of tasks than GPT-4o.”

May combine two claims.

Phase-1 finishes slightly over half of the 150 proof tasks, while Phase-2 refinement and Phase-3 debugging contribute 22 and 37 additional proven tasks respectively.

“As also shown in Table 2, Phase-1 is able to finish slightly over half of the 150 proof tasks, while Phase-2 refinement and Phase-3 debugging also contribute to 22 and 37 additional proven tasks respectively.”

May combine two claims.

With 30 seconds per task, AutoVerus generates correct proof for 81 tasks, while the baseline cannot even finish 40 tasks.

“Furthermore, if we give each task only 30 seconds, AutoVerus can generate correct proof for 81 tasks, while the the baseline cannot even finish 40 tasks.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

For that Diffy task, the other three programs are safe and valid.

“Fortunately, the other three programs are safe and valid.”

Probably not a substantial claim: may not pass S3 (load-bearing).

All remaining 38 Diffy tasks were translated from C to Rust.

“We translated all the remaining 38 tasks from 𝐶 to Rust.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The function-post-condition repair agent in the Fibonacci case study added two asserts describing the transitive relationship fibo(n) <= fibo(m-1) and fibo(m-1) <= fibo(m).

“the agent added the two green-highlighted lines in Figure 7c.Interestingly, the LLM does not simply assert fibo(n) <= fibo(m), the failed post condition.Instead, it added two asserts that describe the transitive relationship of fibo(n) <= fibo(m-1), which matches the post-condition of the proof function right before it on Line 7, and fibo(m-1) <= fibo(m), which is quite nice.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

AutoVerus runs into different situations every time, and the final proof produced by it is not always the same.

“Since this is a difficult task, we have noticed that AutoVerus runs into different situations every time, and the final proof produced by it is not always the same.”

May combine two claims.

The arithmetic-overflow repair agent in the Fibonacci case study added an assert stating the bound 0x8000_0000 for fib[i-1] + fib[i-2], synthesized lemma_fibo_monotonic, and used it to support the bound assertion.

“it figured out the right bound 0𝑥8000_0000 for the expression fib[i-1] + fib[i-2], probably based on the bound expressed in the fibo_fits_i32 spec-function in Figure 7b; 3) it realized that proving the monotonicity of the fibonacci sequence is needed and hence synthesized a new proof function lemma_fibo_monotonic and also used this function to support the bound assertion very nicely on Lines 28-31”

May combine two claims.

The baseline took much longer and many more LLM calls than AutoVerus to achieve its successes.

“Of course, the baseline took much longer and many more LLM calls to achieve this than AutoVerus, which we discuss below.”

Probably not a substantial claim: may not pass S3 (load-bearing). The quote only partly states this claim.

Finally, Verus reports that the whole proof task in the Fibonacci case study was successfully done.

“Finally, Verus reports that the whole proof task was successfully done!”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

In Iteration 3 of the Fibonacci case study, Verus reports that the while-loop is completely verified, but there is a new error: the post-condition fibo(n) <= fibo(m) of lemma_fibo_monotonic is not satisfied at the end of the function.

“Verus now reports that the while-loop in Figure 7a is completely verified, but there is a new error-the post-condition fibo(n) <= fibo(m) of the new function lemma_fibo_monotonic shown in Figure 7c is not satisfied at the end of the function.”

May combine two claims.

The baseline succeeded for only 5 out of 38 Diffy tasks, while AutoVerus's Phase-1 alone generated correct proof for 26 Diffy tasks.

“However, the baseline cannot handle more complicated loop invariants, and hence succeeded for only 5 out of 38 Diffy tasks.In comparison, AutoVerus's Phase-1 alone generated correct proof for 26 Diffy tasks.”

May combine two claims.

AutoVerus proved 122 tasks in its first attempt, 10 more in its second attempt, and 5 more on its third attempt.

“Even though the default setting allows up to three attempts for AutoVerus, AutoVerus was able to prove 122 tasks in its first attempt, with 10 more proved in its second attempt and 5 more on its third attempt.”

May combine two claims.

The baseline needs 458 seconds per task or 59 LLM-calls per task to succeed in 67 tasks; AutoVerus needs 22 seconds per task or 2 LLM-calls per task to generate correct proof for at least 67 tasks.

“In order for the baseline to succeed in 67 tasks, it needs a budget of 458 seconds per task or 59 LLM-call per task; in contrast, 22-second per-task or 2 LLM-call per task is sufficient for AutoVerus to generate correct proof for at least 67 tasks.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The entire process consumed 3 million input and 1.5 million output tokens.

“This entire process consumed 3 million input and 1.5 million output tokens.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

Another program for that Diffy task encountered index out-of-bound errors in the last two loops and is ranked lower (V is 3).

“Another program encountered index out-of-bound errors in the last two loops, and hence is ranked lower (i.e., 𝑉 is 3).”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

The final 23 tasks in Verus-Bench are Misc, a collection of 23 miscellaneous Verus programs from Verus tutorials or libraries, including algorithmic programs and challenging features.

“The final 23 is referred to as Misc.This is a collection of 23 miscellaneous Verus programs that appeared in Verus tutorials or libraries.They include some algorithmic programs, like bubble sort, binary search, fibonacci sequence, and tasks that contain challenging features like nested loops, expressing function post conditions as asserts instead of ensures, etc.”

May combine two claims.

Processing the 137 tasks across three rounds required an average of 8.8 LLM calls per task; approximately half were completed with two calls or fewer, and a small number required more than 40.

“Processing these 137 tasks across three rounds required an average of 8.8 LLM calls per task.While approximately half of the tasks were completed with two calls or fewer, a small number required more than 40.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The total cost for the benchmark suite was approximately $37, including tasks that failed after all three rounds.

“Based on the Azure GPT-4o pricing at the time of our evaluation ($5 per 1M input tokens and $15 per 1M output tokens), the total cost for the benchmark suite was approximately $37, including tasks that failed after all three rounds.”

Probably not a substantial claim: may not pass S3 (load-bearing).

In Iteration 1 of the Fibonacci case study, Verus reports one error for the best-so-far proof: the invariant fib.len() == n on Line 24 is not satisfied before the loop.

“Verus only reports one error for this version: invariant fib.len() == n on Line 24 is not satisfied before the loop.”

May combine two claims.

Of CloverBench's 39 Verus translations, 3 cannot be verified by the latest Verus, 4 have weaker specifications than variants already included, and 21 can be verified without proof annotations; the remaining 11 are added to Verus-Bench.

“Our manual inspection found that 3 of them cannot be verified by the latest version of Verus, 4 have weaker specifications than their variants already included in the dataset, and 21 can be verified without proof annotations.We add all remaining 11 into Verus-Bench.”

May combine two claims.

After the first repair in the Fibonacci case study, Verus reports two new errors: an arithmetic-overflow for fib[i-1] + fib[i-2] on Line 33, and the invariant on Line 21 that states fib[j] == fibo(j) for all j between 0 and i does not hold at the end of the loop.

“After the first repair, Verus now reports two new errors: 1) an arithmetic-overflow for fib[i-1] + fib[i-2] on Line 33; 2) the invariant on Line 21 that states fib[j] == fibo(j) for all 𝑗 between 0 and 𝑖 does not hold at the end of the loop.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

In the highest-ranked program for that Diffy task, three loops and the function post-condition are verified (V score is 4), but two verification errors are reported for the last loop.

“In the highestranked program, three loops and the function post-condition are verified (i.e., 𝑉 score is 4), but two verification errors are reported for the last loop with the loop invariants shown in Figure 5a.”

Classified as probably not a substantial claim.

Each Verus-Bench task is a Rust program annotated with Verus specifications.

“we need a suite of proof tasks, with each task being a Rust program annotated with Verus specifications.”

May combine two claims.

Among MBPP-DFY-153's 153 problems, 67 require no proof annotations to verify, 8 are too difficult to translate due to unsupported features, and the remaining 78 are included in Verus-Bench.

“Among these 153, 67 of them require no proof annotations to verify; 8 are too difficult to translate due to code features not well supported by Rust/Verus like floating points and string; the remaining 78 are all translated and included in Verus-Bench.”

May combine two claims.

The first time the assertion-failure repair agent is called in the Fibonacci case study, no good repair is produced; at the second time, it produces a repair adding two asserts and an if m > 1 condition.

“In fact, the first time this repair agent is called upon, no good repair is produced.At the second time, the repair agent comes up with the repair shown in Figure 7d: it added two assert statements to help the SMT solver reason why fibo(m-1) cannot be larger than fibo(m); and it also added the if m > 1 condition to avoid negative indexing, as explained by its own comment.”

May combine two claims.

Unnecessary loop invariants are far more prevalent in AutoVerus proofs; on Diffy, AutoVerus generated an average of 22.2 loop invariants per task, 9.6 unnecessary, while human proofs contained 12.6 total invariants, with only 2.0 unnecessary.

“For example, on the Diffy benchmark, AutoVerus generated an average of 22.2 loop invariants per task, 9.6 of which were unnecessary.In contrast, human proofs for the same tasks contained 12.6 total invariants, with only 2.0 being unnecessary.”

May combine two claims.

On the 30-problem sampled dataset, the default setting (GPT-4o, temperature 1.0) proves 26 tasks, the most among all settings; the baseline repeatedly invoking GPT-4o proves 14 tasks.

“Our default setting (with GPT-4o, temperature 1.0) proves 26 tasks, the most among all settings (shown in Table 5).Note, the baseline scheme of repeatedly invoking GPT-4o can only prove 14 tasks.”

May combine two claims.

Proofs generated by AutoVerus and humans contain a similar number of useful loop invariants; AutoVerus used slightly fewer useful loop invariants on Misc and MBPP tasks, while the trend is reversed on Diffy and Clover tasks.

“As we can see in the blue bars of Figure 12, proofs generated by AutoVerus and those by humans contain a similar number of useful loop invariants.AutoVerus used slightly fewer useful loop invariants on Misc and MBPP tasks, while the trend is reversed on Diffy and Clover tasks.”

The quote only partly states this claim.

Lack of full knowledge of the vstd library caused AutoVerus to fail 5 tasks involving complicated usage of Verus data structures.

“In total, this led to the failure in 5 tasks.”

May combine two claims.

GPT-3.5-turbo with AutoVerus outperforms the baseline of repeatedly invoking GPT-4o, proving 18 tasks.

“Furthermore, benefiting from the AutoVerus design, GPT-3.5-turbooutperforms the baseline of repeatedly invoking GPT-4o, proving 18 tasks.”

May combine two claims.

During the run producing Table 2, LLMs generated 2,637 proof candidates, of which 326 (12.4%) are unsafe; they were filtered out by Lynette.

“During the run of producing the results in Table 2, LLMs generated 2,637 proof candidates, of which as many as 326 (12.4%) are unsafe.Fortunately, they are filtered out by our Lynette tool.”

May combine two claims.

The number of tasks that can be proved drops if any one of the three examples used by AutoVerus's Phase-1 agent is removed; the third example is most influential.

“As shown in Table 4, the number of tasks that can be proved drops if we remove any one of the three examples used by AutoVerus's Phase-1 agent.The third example stands out as particularly influential, resulting in the most reduction in proved tasks when removed.”

May combine two claims.

Under the alternative design combining all five agents in Phase-1 and Phase-2 into one agent, 7 tasks that originally can be proved now cannot, including 3 tasks that originally can be proved with just Phase-1.

“Under this alternative design, 7 tasks that originally can be proved now cannot.This includes 3 tasks that originally can be proved with just Phase-1.”

May combine two claims.

For 14 tasks, although none of the direct output of the Phase-1 agent is correct, merging some of them immediately provides correct proof.

“For 14 tasks, although none of the direct output of the Phase-1 agent is correct, merging some of them immediately provides correct proof just like the example in Figure 5.”

May combine two claims.

AutoVerus makes the most repair-agent invocations with GPT-3.5, probably because the raw output of GPT-3.5 has the worst quality among all models; it needs the fewest repair-agent invocations with GPT-4o.

“Of course, the exact number of invocations are very different across different LLMs: AutoVerus has to make the most repair-agent invocations with GPT-3.5, probably because the raw output of GPT-3.5 has the worst quality among all models; on the other hand, AutoVerus needs the fewest repair-agent invocations with GPT-4o.”

The quote only partly states this claim.

The only concerns for data leakage are three tasks in the Misc part of Verus-Bench: fibonacci, tail_triangle, and lemma_len_intersect, which are created based on examples in the online Verus Tutorial.

“The only concerns are three tasks in the Misc part of Verus-Bench,”

• cites [47]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

May combine two claims.

GPT-4-turbo delivers competitive performance compared to GPT-4o, with both proving 26 out of 30 tasks; GPT-3.5-turbo allows AutoVerus to prove 18 tasks.

“While trying three different GPT models, we observe that GPT-4-turbo delivers competitive performance compared to our default setting with GPT-4o, with both models power AutoVerus to prove 26 out of the 30 tasks.In contrast, GPT-3.5-turboonly allows AutoVerus to prove 18 tasks.”

May combine two claims.

The Inference Dataset includes all 78 tasks correctly proved by AutoVerus using Phase-1 alone; the Refinement Dataset includes all 22 tasks requiring both Phase-1 and Phase-2.

“The Inference Dataset includes all the 78 tasks that can be correctly proved by AutoVerus using Phase-1 alone; the Refinement Dataset includes all the 22 tasks that require both Phase-1 and Phase-2 to be proved by AutoVerus.”

May combine two claims.

AutoVerus invokes a similar set of repair agents with different LLMs: the assertion failure repair agent is most frequently used for all models except GPT-4-Turbo; the popularity of arithmetic under/overflow, two types of invariant failures, and post-condition failures are similar; the two types of pre-condition failures are rarely encountered.

“Generally speaking, AutoVerus invokes a similar set of repair agents with different LLMs: the repair agent for assertion failures is most frequently used for all models except for GPT-4-Turbo; the popularity of repair agents for arithmetic under/overflow errors, two types of invariant failures, and post-condition failures are similar; the two types of pre-condition failures are rarely encountered”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

AutoVerus's proof and the Verus Tutorial's proof both prove the monotonicity of the Fibonacci sequence, but they divide the proof into different sets of cases and conduct the inductive proof differently.

“although both functions prove the monotonicity of the Fibonacci sequence, they divide the proof into different sets of cases and also conduct the inductive proof differently.”

• AssumptionThe authors state this as an assumption: AutoVerus assumes that the specification (i.e., function pre-conditions and post-conditions) is already given.

Probably not a substantial claim: may not pass S3 (load-bearing).

The fifth output is almost never the top-ranked candidate based on Verus, which happens in about 3% of model invocations.

“Interestingly, the fifth output is almost never the top-ranked candidate based on Verus, which happens to about 3% of the model invocation.”

May combine two claims.

43 out of 78 MBPP tasks and 11 out of 23 Misc tasks cannot be proved using loop invariants alone.

“for example, 43 out of 78 MBPP tasks and 11 out of 23 Misc tasks cannot be proved using loop invariants alone.”

Probably not a substantial claim: may not pass S4 (based).

AutoVerus has achieved good results on Verus-Bench.

“AutoVerus has achieved good results on Verus-Bench, and provides a starting point for future research.”

• AssumptionThe authors state this as an assumption: AutoVerus assumes that the specification (i.e., function pre-conditions and post-conditions) is already given.

Probably not a substantial claim: may not pass S3 (load-bearing).

Proof tasks that do not require any proof annotations are not included in Verus-Bench.

“This type of tasks is not included in Verus-Bench.”

Classified as probably not a substantial claim. May combine two claims.

Phase 1 of AutoVerus focuses on loop invariants because asserts and proof functions/blocks are typically added during proof debugging.

“Since asserts and proof functions/blocks are typically added during the proof debugging to provide extra hints to SMT solver, at this first phase of proof generation, AutoVerus focuses on loop invariants.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based).

The debugging phase is arguably the most important phase of AutoVerus because any mistake or limitation of the first two phases can be rescued there.

“This debugging phase is arguably the most important phase of AutoVerus: any mistake or limitation of the first two phases can be rescued here.”

Probably not a substantial claim: may not pass S4 (based).

LLMs easily stumble at subtle syntax extensions made by Verus upon Rust.

“However, this also produces challenges, as LLMs easily stumble at those subtle syntax extensions made by Verus upon Rust.”

Probably not a substantial claim: may not pass S3 (load-bearing).

There is no subrange spec function for the Rust Vec type.

“For example, there is no subrange spec function for Rust Vec type.”

Classified as probably not a substantial claim.

In the Refinement phase, AutoVerus runs a series of agents, each looking for a common mistake or omission in loop invariants and conducting refinement accordingly.

“(2) Refinement phase: AutoVerus runs a series of agents, each looking for a common mistake or a common omission in loop invariants and conducting refinement accordingly;”

Probably not a substantial claim: may not pass S3 (load-bearing). The quote only partly states this claim.

AutoVerus conducts proof generation in three phases: Generation, Refinement, and Debugging.

“Putting these together, AutoVerus conducts its proof generation for input Rust codefoot_3 in three phases, as shown in Figure 2: (1) Generation phase: AutoVerus uses an LLM agent to generate preliminary loop invariants;”

Classified as probably not a substantial claim.

In the Debugging phase, AutoVerus goes through rounds of debugging guided by Verus to produce the correct proof, fixing loop invariants and adding proof annotations such as assert statements and lemma functions.

“(3) Debugging phase: Guided by Verus, AutoVerus goes through rounds of debugging to produce the correct proof, not only fixing loop invariants but also adding proof annotations like assert statements and lemma functions.”

Probably not a substantial claim: may not pass S3 (load-bearing).

Throughout the three phases, proof filtering, ranking, and merging are conducted using Verus and Lynette, an AST-level code analysis tool built upon the Verus parser.

“Throughout these three phases, proof filtering, ranking, and merging are conducted using Verus and Lynette, an AST-level code analysis tool that we build for AutoVerus upon Verus parser.”

Classified as probably not a substantial claim.

In the Generation phase, AutoVerus uses an LLM agent to generate preliminary loop invariants.

“(1) Generation phase: AutoVerus uses an LLM agent to generate preliminary loop invariants;”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based). May combine two claims.

Verus does not require LLMs to learn a new language because LLMs should be familiar with Rust already.

“Unlike many verifiers, Verus does not require LLMs to learn a new language -LLMs should be familiar with Rust already.”

May combine two claims.

AutoVerus combines formal methods and static analysis to filter out invalid candidates, rank proof candidates based on Verus' feedback, and stitch proof snippets together.

“To effectively navigate through this huge search space, we combine formal methods and static analysis to quickly filter out invalid candidates, to rank proof candidates based on Verus' feedback, and to stitch proof snippets together in the hope of creating a perfect proof out of a collection of imperfect ones.”

May combine two claims.

Verus uses its abstract int type by default in specification functions and often requires type casting, which is difficult for LLMs like GPT.

“Verus uses its abstract int type by default in specification functions and hence often requires type casting, such as the 'i as int' on Line 28, 33-36 in Figure 1.This type of casting is difficult for LLMs like GPT that are used to Rust syntax.”

Classified as probably not a substantial claim.

Verus leverages the Rust type system to avoid the complexity of reasoning about memory safety and aliasing, largely reducing the amount of needed proof annotation.

“Verus also leverages the Rust type system to avoid the complexity of reasoning memory-safety and aliasing, largely reducing the amount of needed proof annotation.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims. The quote only partly states this claim.

Phase 3 targets the eight most common types of verification errors, with one repair agent per type, an extra repair agent for assertion errors, and a generic default repair agent.

“Specifically, AutoVerus targets the eight most common types of verification errors, including function pre-condition errors, vector-index out-of-bound errors (a common sub-type of function pre-condition errors), function post-condition errors, loop-invariant unsatisfied at the beginning of a loop errors, loop-invariant unsatisfied at the end of a loop errors, assertion errors, arithmetic under/ov”

Probably not a substantial claim: may not pass S4 (based).

Verus' emphasis on verification speed sometimes comes at the cost of extra proof annotations that may not be needed by other SMT-based verifiers (e.g., Dafny).

“Verus' emphasis on verification speed, a property that is critical for Verus to work for large system code, sometimes comes at the cost of extra proof annotations that may not be needed by other SMT-based verifiers (e.g., Dafny), which creates extra challenges for GenAI.”

May combine two claims.

Verus directly works on Rust code, and Verus specifications and proof annotations are written with Rust syntax and inlined in the Rust code as ghost code.

“Verus directly works on Rust code; Verus specifications and proof annotations are also written with Rust syntax and are inlined in the Rust code under proof in the form of ghost code.”

Probably not a substantial claim: may not pass S3 (load-bearing). The quote only partly states this claim.

Phase 2 consists of four refinement agents: Constant-Propagation, Array-Length, Quantifier, and Conditional-Loop-Invariant.

“The refinement phase consists of a series of LLM agents, each aiming one common mistake in the writing of loop invariants in Verus:”

• Also stated in: § 4.2.1 Refinement-Agent Design. · plain

  “Constant-Propagation agent checks if the function pre-condition includes properties about a read-only parameter, and adds these properties as invariants to every loop in the function.”

Classified as probably not a substantial claim.

Misuse of Rust APIs in Verus annotation is very common for inexperienced users and LLMs.

“As another example, since Rust executable functions cannot be called in ghost code, misuse of Rust APIs in Verus annotation is very common for inexperienced users and LLMs.”

Probably not a substantial claim: may not pass S4 (based). May combine two claims.

Verus proof annotations, although written in Rust syntax, have usage very different from regular Rust executable code and require expertise in verification to master.

“Furthermore, although Verus proof annotations (short as proof) are written in Rust syntax, their usage is very different from regular Rust executable code and require expertise in verification to master.”

Probably not a substantial claim: may not pass S3 (load-bearing).

AutoVerus keeps running debugging iterations until a correctly proved program is found or a pre-configured threshold is reached (10 iterations by default).

“AutoVerus keeps running these iterations until a correctly proved program is found or a pre-configured threshold is reached (10 iterations by default).”

Classified as probably not a substantial claim.

AutoVerus configures all its agents with a high-temperature, multi-output setting so that a wide range of diverse and creative proofs can be generated.

“To handle inevitable and yet unexpected challenges in writing a proof, AutoVerus configures all its agents with a high-temperature, multi-output setting so that a wide range of diverse and creative proofs can be generated for AutoVerus to pick from.”

Classified as probably not a substantial claim.

AutoVerus uses an ordered list of Verus error types: type errors are top priority, followed by bound-related errors, then invariant-not-satisfied-before-loop errors, then remaining errors.

“The top one is type error, because they have to be fixed before Verus can compile the program and conduct verification attempt.The next two are bound-related errors, including the index-bound-error and arithmetic-overflow/underflow errors.”

• Also stated in: § 4.3.2 Repair-Agent Composition and Output Post-Processing. · plain

  “After that, invariant-not-satisfiedbefore-loop errors get selected, as they are often easier to fix than other types of errors.Beyond that, all remaining errors are repaired one by one based on where they show up in the report of Verus.”

Probably not a substantial claim: may not pass S3 (load-bearing).

Diffy contains 69 programs written in C designed to evaluate array and loop related verification.

“Diffy contains 69 programs written in C that were designed to evaluate array and loop related verification.”

• cites [6]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

AutoVerus filters out unsafe candidates through static analysis.

“AutoVerus first filters out the candidates that are unsafe, like the one in Figure 4, through static analysis.”

Classified as probably not a substantial claim. May combine two claims.

The baseline has the same temperature setting and 5-output per LLM-call as AutoVerus.

“Again, keep in mind that the baseline has the same temperature setting and 5-output per LLM-call as AutoVerus.”

Classified as probably not a substantial claim. May combine two claims.

In Phase 3, AutoVerus collects all verification errors in the best-so-far program, picks one error to fix next, and prompts a repair agent that suits that error.

“In each iteration, AutoVerus collects all the verification errors E in 𝑃 𝐵 from Verus (Line 5), picks one error 𝐸 from E to fix next (Line 6), and prompts a repair agent that suits 𝐸 (Line 7).”

Classified as probably not a substantial claim. May combine two claims.

Lynette checks whether an LLM output P is safe regarding the input Rust program and its specification P_o by comparing the pure Rust AST after erasing ghost code, comparing pre- and post-conditions, and searching for debugging ghost functions such as admit() or assume().

“To check whether a LLM output 𝑃 is safe regarding the input Rust program and its specification 𝑃 𝑜 , Lynette checks if 𝑃 and 𝑃 𝑜 can be compiled to the same executable by comparing the pure Rust AST of the files after erasing the ghost code; Lynette compares the pre-and post-condition of 𝑃 and 𝑃 𝑜 so the LLM cannot tweak them to change the goal of the verification; Lynette also searches for debug”

Classified as probably not a substantial claim.

When comparing with the baseline, they show the number of verified tasks under the same time and LLM-call budget to be fair.

“When comparing with the baseline, we will show the number of verified tasks under the same time and LLM-call budget to be fair.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

The Houdini algorithm has been used for GenAI-for-C and is applied here for Verus.

“This algorithm has been used for GenAI-for-C [23] and we apply it here for Verus.”

• cites [23]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

There is no overlap between the examples used by AutoVerus agents and Verus-Bench.

“Notably, there is no overlap between the examples used by AutoVerus agents and Verus-Bench.”

May combine two claims.

Most Diffy tasks contain multiple loops and require good loop-invariant synthesis; 31 tasks require reasoning about non-linear equations.

“Most tasks in this suite contain multiple loops and hence require good loop-invariant synthesis.31 tasks here require reasoning about non-linear equations (e.g., knowing that (𝑖 + 1) 3 == 𝑖 3 + 3 * 𝑖 2 + 3 * 𝑖 + 1), which is not the focus of Verus system verification.”

• cites [6]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

The four refinement agents are designed based on common mistakes that the authors themselves typically commit when writing loop invariants.

“These four agents are designed based on common mistakes that we ourselves typically commit when we write loop invariants.”

May combine two claims.

Lynette is AST-aware and ensures that deletion of unprovable proof annotations honors ghost expression boundaries and produces a syntactically correct result.

“Since Lynette is AST-aware, it makes sure that the deletion honors the boundary of ghost expression, and guarantees to produce a syntactically correct result.”

The quote only partly states this claim.

The baseline is given an unfair advantage of cheating: answers to four complicated tasks from Verus-Bench are put as examples in its prompt.

“Finally, we give this baseline an unfair advantage of”

Probably not a substantial claim: may not pass S3 (load-bearing).

The baseline's prompt is essentially a summary of all prompts used in AutoVerus agents.

“To make this baseline competitive, we designed its prompt to essentially be a summary of all the prompts used in AutoVerus agents.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

The baseline uses the same LLM-temperature setting as AutoVerus (1.0) and is configured to generate 5 outputs per invocation, same as the Phase-1 agent in AutoVerus.

“It uses the same LLM-temperature setting as AutoVerus (1.0), and is configured to generate 5 outputs in each invocation, same as the Phase-1 agent in AutoVerus.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

Lynette uses the pure Rust AST as an anchor to merge ghost code from two proof candidates P1 and P2, with the minimum merging unit being a ghost expression.

“Lynette first erases all of the ghost code in the program to obtain the pure Rust AST, which is the same for 𝑃 1 and 𝑃 2 , and uses it as the anchor to merge the ghost code in 𝑃 1 and 𝑃 2 .The minimum merging unit is a ghost expression, i.e., a Verus assertion, a proof block, or an invariant.”

Classified as probably not a substantial claim. May combine two claims.

The baseline uses the same LLM-temperature and 5-output per invocation setting as AutoVerus, and has a more sophisticated prompt and examples than any AutoVerus agent.

“Note that, this baseline scheme uses the same LLM-temperature and 5-output per invocation setting as AutoVerus, and has more sophisticated prompt and examples than any AutoVerus agent.”

Probably not a substantial claim: may not pass S4 (based).

With the basic proof-repair knowledge embedded in AutoVerus agents and robust post-processing, AutoVerus can reliably figure out a correct proof after a number of attempts.

“Fortunately, with the basic proof-repair knowledge embedded in AutoVerus agents and the robust post-processing, AutoVerus can reliably figure out a correct proof after a number of attempts.”

Classified as probably not a substantial claim.

Since Verus can automatically tell whether a proof is correct, there is no manual effort involved even if they invoke LLM or execute the AutoVerus workflow multiple times.

“Keep in mind that since Verus can automatically tell whether a proof is correct, there is no manual effort involved even if we invoke LLM or execute the AutoVerus workflow for multiple times.”

• AssumptionRests on an assumption: Verus can automatically tell whether a proof is correct.

Classified as probably not a substantial claim. May combine two claims.

AutoVerus considers a program with higher V as better, with lower E as the tie-breaker.

“For any two programs that contain the same executable Rust code, AutoVerus considers the one with higher 𝑉 score as the better one (i.e., more functions proved), with the tie-breaker being having a lower 𝐸 score (i.e., fewer verification errors).”

Classified as probably not a substantial claim.

AutoVerus ranks remaining LLM-generated Verus programs based on a score tuple {V, E}, where V is the number of functions successfully verified by Verus and E is the number of verification errors reported by Verus.

“AutoVerus then ranks remaining LLM-generated Verus programs based on a score tuple {𝑉 , 𝐸} (Line 4 in Algorithm 1), with 𝑉 being the number of functionsfoot_4 successfully verified by Verus, and 𝐸 being the number of verification errors reported by Verus.”

May combine two claims.

Verus-Bench excludes trivial proof tasks that can be proved by Verus without any proof annotations; 88 proof tasks from source benchmark suites were rejected for this reason.

“Second, we make sure not to include any trivial proof tasks (i.e., tasks that can be proved by Verus without any proof annotations).In fact, 88 proof tasks from our source benchmark suites are rejected for this reason!”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

Due to the randomness of LLMs, the number of correctly verified tasks may change over runs; by default, they report the number after running AutoVerus three times.

“Due to the randomness of LLMs, the number of correctly verified tasks may change over runs.By default, we report the number of correctly verified tasks after running AutoVerus (the whole three phases) for three times; the same applies for various variants of AutoVerus.”

May combine two claims.

CloverBench includes 60 example programs written and verified in Dafny, and its authors provide the Verus translation for 39 of them.

“This suite includes 60 example programs, as might be found in CS textbooks, written and verified in Dafny.The authors of CloverBench also provide the Verus translation for 39 of them.”

• cites [42]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

In Phase 2, each agent generates one proof candidate, so no merging or ranking is needed.

“The post-processing here is simpler than that of Phase-1: each agent only generates one, instead of five, proof candidates, and hence there is no merging or ranking needed.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

Verbosity from unnecessary loop invariants can harm code and proof readability, but the negative impact is limited because an automated process can effectively remove them.

“While this verbosity can harm code and proof readability, the negative impact is limited, as an automated process can effectively remove these unnecessary annotations.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

Verus-Bench is still just a collection of 150 tasks; it cannot represent many real-world proof tasks in large system code and cannot guarantee to represent all small-scale proof tasks.

“However, it is still just a collection of 150 tasks.It cannot represent many real-world proof tasks in large system code; it also cannot guarantee to represent all small-scale proof tasks.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The challenge of writing formal proofs has sparked interest in using LLMs to automate formal proof synthesis.

“This challenge has sparked interest in using LLMs to automate formal proof synthesis [28].”

• cites [28]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• AssumptionRests on an assumption: Formal proofs offer mathematical guarantees of correctness against program specifications, yet writing these proofs remains a labor-intensive, expertise-driven process.

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

The authors who participated in the design of AutoVerus are already familiar with some tasks in the Diffy benchmark and the Misc set.

“However, the authors who participated in the design of AutoVerus are already familiar with some of the tasks in the Diffy benchmark and in the Misc set.”

May combine two claims.

For the 137 successfully proved tasks, the quality of AutoVerus proof is good and in line with human-written proof.

“For the 137 tasks that AutoVerus successfully proved, at a high level, the quality of AutoVerus proof is good and in line with human-written proof -after all, passing the Verus verification is a high bar for quality.”

May combine two claims.

The design of AutoVerus is generally applicable for different LLM models and can effectively help boost the performance of LLMs.

“Overall, this result shows that the design of AutoVerus is generally applicable for different LLM models, and can effectively help boost the performance of LLMs.”

May combine two claims. The quote only partly states this claim.

The impact of potential data leakage is minimal because Verus proofs for all 38 Diffy tasks and all 78 MBPP tasks were not publicly available throughout the research project, and the 11 CloverBench examples were released after the earlier GPT-4o models used.

“First, the (un-)availability of online Verus resources.Among the four sources of Verus-Bench, Verus proofs for all 38 Diffy tasks and all 78 MBPP tasks were not publicly available throughout this research project.The 11 examples from CloverBench were released in the late spring of 2024, while we utilized earlier GPT-4o models (with 2024-02-15 and 2024-05-13 versions), predating the widespread”

May combine two claims.

AutoVerus can work with different types of models, and code-proof remains a challenging task even for the new generation of reasoning models.

“It shows that AutoVerus can work with different types of models.It also shows that code-proof remains a challenging task even for the new generation of reasoning models.”

May combine two claims.

Only 8 out of 657 (1.2%) repair iterations required the default repair agent, showing that the 9 error-specific repair agents offer good coverage of the most common verification errors.

“Note that, only 8 out of 657 (1.2%) repair iterations required the default repair agent.This shows that our 9 error-specific repair agents offer good coverage of the most common verification errors.”

May combine two claims.

Unnecessary loop invariants exist even in human-written proofs because it is challenging to identify the minimal set of evidence required by the verifier; for AutoVerus, the issue is exacerbated because LLM agents sometimes add identical loop invariants across multiple proof attempts.

“These unnecessary loop invariants exist even in human-written proofs, as it is challenging to identify the minimal set of evidence required by the verifier to finish a proof.For AutoVerus, this issue is exacerbated because LLM agents sometimes add identical loop invariants across multiple proof attempts.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The evaluation does not yet cover some of the newest Rust features supported by Verus, such as iterators.

“Finally, our evaluation does not yet cover some of the newest Rust features supported by Verus, such as iterators.”

May combine two claims.

LeanDojo, LEGO-Prover, and Baldur only work for interactive theorem provers and are primarily designed for maths rather than programs.

“However, they only work for interactive theorem provers and are primarily designed for maths rather than programs.”

• cites [55]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites [48]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites [16]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Classified as probably not a substantial claim.

A higher temperature setting is beneficial in fostering LLM creativity and exploring a wider range of potential solutions, as long as human experts and discipline are also applied.

“This aligns with our design intuition that a higher temperature setting is beneficial in fostering LLM's creativity and exploring a wider range of potential solutions, as long as human experts and discipline are also applied.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

LLMs have been revolutionizing various software engineering tasks.

“LLMs have been revolutionizing various software engineering tasks [10,46,50,52,53], especially for code generation [2,7], but the reliability of the generated code remains uncertain [29].”

• cites [10]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites [46]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites [50]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites [52]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites [53]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

Recent efforts like LeanDojo, LEGO-Prover, and Baldur have used LLMs and leverage the vast existing data of interactive theorem provers to create RAG databases or fine-tune models.

“Recent efforts like LeanDojo [55], LEGO-Prover [48], and Baldur [16] have used LLMs, and they all leverage the vast existing data of interactive theorem provers to create RAG databases or fine-tune models.”

• cites [55]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites [48]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites [16]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Classified as probably not a substantial claim. May combine two claims.

The authors tried not to tune AutoVerus based on features of specific proof tasks in Verus-Bench, and the team setting up the majority of Verus-Bench did not participate in the design of AutoVerus.

“We have tried our best not to tune AutoVerus based on features of specific proof tasks in our Verus-Bench, and have our team that sets up the majority of the Verus-Bench not participating in the design of AutoVerus.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The reliability of code generated by LLMs remains uncertain.

“but the reliability of the generated code remains uncertain [29].”

• cites [29]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

Verus integrates Rust's borrow checker into its verification process, enforcing linearity and borrowing in specifications and proofs.

“Verus distinguishes itself further by integrating Rust's borrow checker into its verification process, enforcing linearity and borrowing in specifications and proofs.”

• cites [43]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites [56]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

There is inherent randomness in AutoVerus and the evaluation given the probabilistic nature of LLMs.

“There is an inherent randomness in AutoVerus and our evaluation given the probabilistic nature of LLM.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

Existing Verus online resources are too few for LLMs to remember or understand.

“Based on these results, we suspect that existing Verus online resources are too few for LLMs to remember or understand.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

Verus's design simplifies reasoning about pointers and concurrency, making Verus particularly suited for systems verification.

“This design simplifies reasoning about pointers and concurrency, making Verus particularly suited for systems verification.[43,56].”

• cites [43]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites [56]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

AutoVerus and Loopy both leverage the Houdini algorithm.

“AutoVerus shares the similarity with Loopy as both leveraging Houdini algorithm.”

• cites [23]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

May combine two claims.

Loopy only focuses on loop invariants that do not involve quantifiers, arrays, etc., while AutoVerus does not have these constraints for loop-invariant synthesis.

“Loopy only focuses on loop invariants that do not involve quantifiers, arrays, etc., while AutoVerus does not have these constraints for loop-invariant synthesis.”

• cites [23]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

26.9% of the proof tasks in DafnyBench do not require any proof annotations.

“Note, 26.9% of the proof tasks in DafnyBench do not require any proof annotations.”

• cites [30]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

Most of the resulting Dafny programs from natural language description workflows contain easy or no proof annotations.

“Given the difficulty of generating the whole program based on natural language, most of the resulting Dafny programs contain easy or no proof annotations, as discussed in § 6.1.”

• cites [33]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites [42]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.