cs.SEMar 18, 2026
SaveCan LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought
Organizations: University of Virginia.
Abstract
As Large Language Models (LLMs) increasingly assist secure software development, their ability to meet the rigorous demands of Rust program verification remains unclear. Existing evaluations treat Rust verification as a black box, assessing models only by binary pass or fail outcomes for proof hints. This obscures whether models truly understand the logical deductions required for verifying nontrivial Rust code. To bridge this gap, we introduce VCoT-Lift, a framework that lifts low-level solver reasoning into high-level, human-readable verification steps. By exposing solver-level reasoning as an explicit Verification Chain-of-Thought, VCoT-Lift provides a concrete ground truth for fine-grained evaluation. Leveraging VCoT-Lift, we introduce VCoT-Bench, a comprehensive benchmark of 1,988 VCoT completion tasks for rigorously evaluating LLMs' understanding of the entire verification process. VCoT-Bench measures performance along three orthogonal dimensions: robustness to varying degrees of missing proofs, competence across different proof types, and sensitivity to the proof locations. Evaluation of ten state-of-the-art models reveals severe fragility, indicating that current LLMs fall well short of the reasoning capabilities exhibited by automated theorem provers.
Figures & tables
Figure 1: (a) The program is about replacing the last element of the first vector ( first ) with all elements of the second ( second ). Executable Rust code , specifications , and proof hints are highlighted. The specifications define the precondition ( requires ) and postcondition ( ensures ), and verification relies on three parts of proof hints: two blocks of loop invariants and one assertion. (b) Shows the Z3 proof of the running example with high-level , medium-level , and low-level proofs highlighted. The high-level rule unit-resolution (line 491) establishes the property , while medium-level rules such as monotonicity and rewrite (line 622) prove index bounds. Low-level rules encode trivial reasoning, e.g., refl (lines 653–654), which simply asserts x775 .
Figure 2: Overview of VCoT-Lift.
Figure 3: The intermediate VCoT for the running example’s second while loop across stages of VCoT-Lift. \raisebox{-0.9pt}{1}⃝ Shows the Verus program with original proof hints and transformed proofs ; after three transformer–checker loops, several assertions and a lemma establishing a key property s.subrange(0, s.len()) == s are introduced. \raisebox{-0.9pt}{2}⃝ Shows the pruned proofs . \raisebox{-0.9pt}{3}⃝ Shows the repaired proofs , fixing a syntactic error.
Figure 4: Conceptual visualization of: \raisebox{-0.9pt}{1}⃝ Aggregated Z3 proof segments for the running example, where mp and lemma segments are grouped and passed to the corresponding checkers; \raisebox{-0.9pt}{2}⃝ the mapping mechanism, where the modus ponens checker identifies a Z3 proof without a corresponding Verus-level proof and marks the transformation incomplete.
Figure 5: Comparison of Total Proof Lines per Program Between VCoT-Bench-Org and Verus-Bench
Figure 6: Composition of VCoT-Bench.
Figure 7: Overall accuracy across proof-removal ratios.
| Results for overall accuracy | ||||||
|---|---|---|---|---|---|---|
| Model Name | VCoT-Bench-Type | VCoT-Bench-Loc | ||||
| Invariant | Assertion | Lemma | Front | Middle | End | |
| GPT-5.2 | 54.42 | 34.25 | 55.48 | 58.27 | 41.15 | 65.58 |
| GPT-5 mini | 23.47 | 32.88 | 36.30 | 49.04 | 36.92 | 60.00 |
| gpt-oss | 17.69 | 21.58 | 26.20 | 19.81 | 9.81 | 28.65 |
| Claude Sonnet 4.5 | 68.71 | 39.55 | 51.54 | 69.04 | 46.35 | 65.96 |
Table 1: Overall accuracy across proof types and proof locations. The highest and second-highest accuracies are highlighted.
Figure 8: The complete VCoT exposed by VCoT-Lift for the running Verus example with specifications , including original proof hints and the additional proof steps . The VCoT is composed of five primary reasoning phases.
| Level | Rule | Description |
|---|---|---|
| High | lemma | Discharge a hypothesis; if a contradiction is derived from an assumption , the rule concludes . |
| th-lemma | Introduce a theory-specific tautology or conflict clause generated by the solver to justify an inference that is valid within that theory’s specific axioms. | |
| mp | Given a proof of and a proof that implies (or ), this rule concludes . | |
| mp | Given a proof of and a proof that is equivalent to ( ), this rule concludes . | |
| unit-resolution | Performs a resolution step between a multi-literal clause and one or more unit clauses. | |
| quant-intro | Given an equivalence between two terms , concludes that . |
Table 2: Z3 Proof Rule Hierarchy.
| Vendor | Model Name | Checkpoint | Type | Cost |
| OpenAI | GPT-5.2 ( OpenAI, 2025b ) | gpt-5.2-2025-12-11 | API | $630.64 |
| GPT-5 mini ( OpenAI, 2025a ) | gpt-5-mini-2025-08-07 | API | $86.75 | |
| gpt-oss 20b ( OpenAI, 2025c ) | gpt-oss-20b | GPU | – | |
| Anthropic | Claude Sonnet 4.5 ( Anthropic, 2025b ) | claude-sonnet-4-5-20250929 | API | $960.99 |
| Claude Haiku 4.5 ( Anthropic, 2025a ) | claude-haiku-4-5-20251001 | API | $300.32 | |
| Gemini 3.1 Pro ( Google, 2026 ) | gemini-3.1-pro-preview | API | $683.32 |
Table 3: Detailed configurations and evaluation costs for the evaluated LLMs
Appendix figures & tables8 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 9: Comparison of # Assertion and # Lemma Function per program between VCoT-Bench-Org and Verus-Bench.
Figure 10: Impact of semantic block removal on (a) Syntactic Accuracy, and (b) Semantic Accuracy.
| Results for VCoT-Bench-Type | ||||||
|---|---|---|---|---|---|---|
| Model Name | Invariant | Assertion | Lemma | |||
| SynAcc | SemAcc | SynAcc | SemAcc | SynAcc | SemAcc | |
| GPT-5.2 | 59.18 | 62.59 | 13.70 | 56.16 | 61.64 | 59.59 |
| GPT-5 mini | 12.24 | 39.46 | 2.74 | 63.01 | 23.97 | 54.79 |
| gpt-oss | 0.00 | 35.37 | 4.79 | 39.73 | 34.25 | 30.82 |
| Claude Sonnet 4.5 | 97.96 | 59.18 | 53.42 | 39.73 | 90.41 | 39.73 |
Table 4: Syntactic and Semantic Accuracy across Proof Types. The highest and second-highest scores are highlighted.
| Results for VCoT-Bench-Loc | ||||||
|---|---|---|---|---|---|---|
| Model Name | Front | Middle | End | |||
| SynAcc | SemAcc | SynAcc | SemAcc | SynAcc | SemAcc | |
| GPT-5.2 | 63.85 | 63.85 | 35.38 | 54.62 | 66.15 | 73.85 |
| GPT-5 mini | 34.62 | 67.69 | 23.08 | 56.92 | 41.54 | 83.08 |
| gpt-oss | 10.00 | 30.77 | 6.92 | 15.38 | 22.31 | 38.46 |
| Claude Sonnet 4.5 | 93.08 | 62.31 | 63.08 | 46.92 | 80.77 | 64.62 |
Table 5: Syntactic and Semantic Accuracy across Proof Locations. The highest and second-highest scores are highlighted.
| Accuracy of All Judges | ||||||||
|---|---|---|---|---|---|---|---|---|
| Evaluated Models | OpenAI | Claude | Gemini | DeepSeek | ||||
| 5 mini | 5.2 | Sonnet 4.5 | Haiku 4.5 | 3 Pro | 3 Flash | R1 | V3.2 | |
| GPT-5.2 | 94% | 78% | 72% | 54% | 94% | 86% | 78% | 75% |
| GPT-5 mini | 86% | 71% | 89% | 74% | 86% | 88% | 80% | 79% |
| gpt-oss 20b | 92% | 92% | 94% | 91% | 96% | 97% | 94% | 90% |
| Claude Haiku 4.5 | 92% | 77% | 86% | 80% | 91% | 92% | 83% | 86% |
Table 6: Accuracy of eight judge models across outputs from the ten evaluated models.
| Self-Evaluation Bias | |||
|---|---|---|---|
| Judge Model | FPR (Own) | FPR (Other) | Self-Bias |
| GPT-5 mini | 6.7% | 7.5% | 0.8% |
| GPT-5.2 | 0.0% | 0.0% | 0.0% |
| Claude Sonnet 4.5 | 18.0% | 8.4% | +9.6% |
| Claude Haiku 4.5 | 5.0% | 2.2% | +2.8% |
| Gemini 3.1 Pro | 3.5% | 10.3% | 6.8% |
Table 7: Self-evaluation bias of each judge model. Positive Self-Bias indicates higher false-positive rate on outputs from the same model family.
Figure 11: Overall accuracy under Best-of-10 sampling across varying proof-removal ratios.
| Results for overall accuracy | ||||||
|---|---|---|---|---|---|---|
| Model Name | VCoT-Bench-Type | VCoT-Bench-Loc | ||||
| Invariant | Assertion | Lemma | Front | Middle | End | |
| GPT-5.2 | 57.82 (+3.40) | 45.03 (+10.78) | 60.45 (+4.97) | 62.88 (+4.61) | 48.27 (+7.12) | 70.00 (+4.42) |
| GPT-5 mini | 31.63 (+8.16) | 43.21 (+10.33) | 43.66 (+7.36) | 54.04 (+5.00) | 43.08 (+6.16) | 62.88 (+2.88) |
| gpt-oss | 21.49 (+3.80) | 28.93 (+7.35) | 31.10 (+4.90) | 25.42 (+5.61) | 18.58 (+8.77) | 35.08 (+6.43) |
| Claude Sonnet 4.5 | 71.26 (+2.55) | 46.92 (+7.37) | 55.31 (+3.77) | 72.69 (+3.65) | 49.62 (+3.27) | 68.46 (+2.50) |
Table 8: Overall accuracy under Best-of-10 sampling across proof types and proof locations. The highest and second-highest accuracies are highlighted. Improvements over greedy decoding are shown in parentheses.