Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought

arXiv:2603.18334 · cs.SE, cs.AI, cs.LG · Submitted 2026-08-17 · Read on arXiv

Listen

Radio episode about this paper

Transcript

Introduction to the show: ident: AI Radio. Generated commentary on the latest Artificial Intelligence papers.

Tom: Next we'll be talking about the paper "Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought".

Jane: The paper was written by Zichen Xie and Wenxi Wang from University of Virginia.

Tom: Stay tuned as we take you through the paper and discuss its implications.

Jane: We also have Lu with us today — senior AI researcher at Tsinghua.

Tom: We also have Meng with us today — lead engineer at a mysterious AI startup.

Jane: We also have Lalam with us today — the in-house Large Language Model.

Tom: Alright, let's get started.

Title: Tom: Welcome back to the show, everyone! Today we're digging into a paper with a title that's a mouthful: "Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought." Jane, I gotta say, just reading that title got me excited.

Jane: It got me excited too, Tom, because it's asking a really fundamental question. We keep hearing that large language models can write code, but can they actually *prove* that code is correct? Not just write something that looks right, but mathematically guarantee it works for every possible input?

Tom: Exactly! And that's where Rust comes in. Rust is this systems programming language that's all about safety and performance. The Linux kernel is adopting it, major tech infrastructure is using it. But even Rust can have logical bugs, right?

Jane: Right, and that's where formal verification enters the picture. There's this tool called Verus that takes Rust code and checks it against formal specifications. It's like having a super-strict math teacher check every step of your homework, not just the final answer.

Tom: So the paper's title is basically asking: when we give LLMs this verification task, are they actually reasoning through the logic like a theorem prover would, or are they just pattern-matching their way to a plausible-looking answer?

Jane: And that's the crux of it. The authors from the University of Virginia, Zichen Xie and Wenxi Wang, they looked at this and said, "You know what? Everyone's been evaluating LLMs on whether they can generate the right proof hints, but they're only looking at pass or fail. Did the program verify or not?"

Tom: Right, it's a black box. You see the output, you see whether it compiled and verified, but you have no idea what the model actually understood. Did it construct a sound deductive chain, or did it just get lucky with syntactic alignment?

Jane: So they came up with this idea of a Verification Chain of Thought, or VCoT. It's like exposing the step-by-step reasoning that the solver does, making it visible and human-readable. And then they built a benchmark around it to test whether LLMs can complete missing pieces of that chain.

Tom: And what they found, Jane, is pretty sobering. We'll get into the details, but spoiler alert: the models are fragile. They lean heavily on context and pattern matching, and when you strip that away, their performance just collapses.

Jane: It's a wake-up call for anyone who thinks LLMs are ready to replace formal verification tools. But it's also a really creative way to open up the black box and actually see what's happening inside. I'm curious how they pulled that off.

Tom: Me too. Let's get into the methodology next, because the way they lifted those low-level solver proofs into something humans can read is genuinely clever.

Summary: Jane: So Tom, before we get into the clever part, let's recap where we are. The paper is "Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought," and the core problem is that verification tools like Z3 produce proofs that are technically correct but practically unreadable.

Tom: Unreadable is an understatement. The paper shows a running example where the Z3 proof is over ten thousand lines long, and more than eighty percent of it is just trivial low-level reasoning. Like, literally proving that a variable equals itself.

Jane: That's the semantic gap. The solver is doing all this fine-grained reasoning, but it's buried under so much noise that you can't see the actual logical structure. So the authors built this framework called VCoT-Lift to lift that low-level reasoning into high-level, human-readable verification steps.

Tom: And how do they do that? They use LLMs themselves, right? That's the twist.

Jane: It is. They use LLMs to transform the Z3 proof into Verus-level proofs. But they don't just ask the model to do it in one shot. They have this four-stage pipeline. First, there's a transformer that synthesizes Verus proofs from the Z3 proofs. Then there's a checker that evaluates completeness, focusing only on the high-level proof rules.

Tom: So it's like a teacher checking whether you covered all the important steps, but ignoring the trivial stuff like "two plus two equals four."

Jane: Exactly. And they have these specialized checker agents for different types of proof rules. Lemma checkers, modus ponens checkers, quantifier checkers. Each one looks at its slice of the Z3 proof and verifies that the transformation captured it.

Tom: And then there's a pruner and a repair stage, right?

Jane: Right. The pruner removes redundant or trivial steps that don't add anything, and the repair stage actually runs the Verus verifier to catch syntax errors and semantic mistakes. So the whole thing is grounded in actually checking whether the transformed proof works.

Tom: That's the soundness guarantee. And the result is this dataset called VCoT-Bench-Org, which has way more proof detail than the original Verus-Bench. Like, six and a half times more proof lines on average.

Jane: And that's what they use to build the benchmark. They dig holes in the proofs at the level of semantic blocks. So you might remove a lemma function, or a set of loop invariants, or a group of assertions, and then ask the LLM to fill in the missing piece.

Tom: So it's not just "write the whole proof from scratch." It's "here's a mostly complete proof, but this chunk is missing. Can you reconstruct it?"

Jane: Precisely. And they organize these tasks along three dimensions. The ratio dimension asks how much of the proof you remove. The type dimension asks whether you're removing invariants, assertions, or lemmas. And the location dimension asks whether the missing piece is at the front, middle, or end of the proof.

Tom: That's a really thorough way to probe what the models actually understand. And the results, Jane, they're not pretty. Let's talk about what they found.

Jane: Let's do it. Because I think the findings tell us something important about where LLMs stand in formal verification.

Improvements: Tom: So Jane, we've set up the benchmark. Now let's talk about what they actually found when they tested ten state-of-the-art models on this thing. And the first finding is that these models are fragile. Like, really fragile.

Jane: Fragile is the right word. When only ten percent of the proof blocks are missing, the best model, Claude Sonnet four point five, gets about seventy-two percent accuracy. But when you remove everything and ask for the full proof from scratch, that same model drops to about seventeen percent.

Tom: And the weakest model, gpt-oss, starts at thirty-three percent and just falls off a cliff. So the models are clearly not reasoning from first principles. They're leaning on the surrounding context, using it like scaffolding.

Jane: That's exactly what the authors argue. The models are doing pattern matching and syntactic alignment, not genuine deductive reasoning. And there's this interesting threshold effect too. Performance drops sharply from ten to forty percent removal, then levels off.

Tom: That forty percent threshold is fascinating. It suggests that once you remove enough of the structural anchors in the proof, the whole logical continuity collapses. The model can't infer the proof logic anymore, so removing more blocks doesn't really matter.

Jane: And then there's the type dimension. Assertions are the hardest for most models. Claude Sonnet four point five gets about sixty-nine percent on loop invariants but only about forty percent on assertions. That makes sense because assertions require precise, state-specific reasoning. One missing condition and the whole thing fails.

Tom: But loop invariants are the most discriminative, right? The gap between the best and worst model on invariants is almost fifty-nine percentage points. That's a huge spread.

Jane: It is. And the location findings are interesting too. Middle blocks are the hardest. Models handle front blocks that set up constraints and end blocks that follow recognizable closing patterns, but the middle requires connective reasoning. You have to propagate invariants, track state evolution, compose multi-step deductions.

Tom: And that's where even the big models stumble. Gemini three drops from about sixty-three percent on front blocks to thirty-six percent on middle blocks. That's a massive drop.

Jane: One more thing I found surprising: the reasoning variants sometimes hurt. Qwen three's thinking mode actually performed worse than its non-thinking mode. And Gemini three Flash outperformed the larger Gemini three on middle blocks.

Tom: That's counterintuitive, right? You'd think more reasoning tokens would help. But the authors suggest that verbose thinking can introduce hallucinated predicates or semantic drift. In formal proofs, where syntactic precision matters, that extra "thinking" can actually be noise.

Jane: So what does this mean practically? I think it means we're a long way from LLMs replacing automated theorem provers. But the benchmark itself is a valuable contribution because it gives us a way to measure progress.

Tom: And that's the optimistic take. The paper isn't just saying "models are bad." It's providing a tool to evaluate them properly, which is the first step toward improving them. Lu and Meng are going to have thoughts on this, I'm sure.

Conclusion: Jane: Well, we've reached the end of our discussion on "Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought." Tom, I think the biggest takeaway is that the paper gives us a way to see inside the verification process instead of just looking at pass or fail.

Tom: And what they saw inside is that current LLMs are a long way from matching automated theorem provers. They're pattern matchers, not reasoners, at least when it comes to formal verification.

Jane: But the framework they built, VCoT-Lift, and the benchmark, VCoT-Bench, those are real contributions. They open up the black box and give us a concrete way to measure whether models actually understand the logic.

Tom: And that matters beyond just Rust verification. The idea of exposing solver reasoning as a chain of thought could apply to other formal methods, other languages, other verification tools. It's a general approach to evaluating reasoning capability.

Jane: The authors also point toward future work where VCoT could provide supervision signals for training. Instead of just rewarding models for producing proofs that verify, you could reward them for reconstructing the actual reasoning chain. That could push models toward genuine symbolic alignment.

Tom: So the field moves from "does it verify?" to "does the model truly understand the verification logic?" That's a much harder question, but it's the right one to ask.

Jane: And it's a question we should keep asking as these models get bigger and more capable. Because the gap we saw here, between syntactic fluency and semantic understanding, it's not going to close on its own.

Tom: Alright, that's a wrap on this paper. Big thanks to our listeners for sticking with us. Next up, we've got a paper on something completely different, so stay tuned.

Jane: Thanks for joining us, everyone. We'll see you in the next episode.

Zichen Xie, Wenxi Wang

University of Virginia

cs.SE, cs.AI, cs.LG

Submitted: 2026-08-17

Updated: 2026-08-18

Project page: https://z3prover.github.io/api/html/ml/Z3.Proof.html

License: http://creativecommons.org/licenses/by/4.0/

Importance score: 57/100

Key concepts

Automated Theorem Provers
These are tools that can mathematically guarantee whether a piece of code is correct by proving it against formal specifications. They perform rigorous, step-by-step logical deduction to ensure correctness, which is what the paper compares LLMs against.
Rust Verification
This involves checking Rust code for logical bugs using formal methods. Tools like Verus check Rust code against formal specifications to mathematically guarantee that the program will work correctly for every possible input.
Verification Chain of Thought (VCoT)
This is a framework used to expose the step-by-step reasoning process of a verification solver, making it human-readable. The researchers use this to build a benchmark testing if LLMs can complete missing pieces of this chain.
VCoT-Bench
This is the benchmark created by the authors that tests LLMs on VCoT tasks. It involves taking mostly complete formal proofs and asking the LLM to fill in missing semantic blocks, organized by proof removal ratio, type, and location.

Terminology

Summary

Summary

This paper introduces VCoT-Lift, a framework that lifts low-level solver reasoning into high-level, human-readable verification steps, and VCoT-Bench, a comprehensive benchmark of 1,988 VCoT completion tasks for rigorously evaluating LLMs’ understanding of the entire verification process.

The paper addresses the problem that existing approaches treat verification process as a black box, measuring success solely by a binary outcome: whether the program verifies with the generated proof hints. This obscures the central question: Do LLMs actually understand the verification logic, or are they merely exploiting statistical patterns? The paper argues that Judging a model solely by whether a program verifies reveals nothing about how verification was achieved.

The context is Rust program verification using Verus, a state-of-the-art formal verification framework for Rust programs. A Verus program consists of "executable Rust code, specifications that precisely describe intended behavior through preconditions (requires) and postconditions (ensures), and user-provided proof hints, including loop invariants, assertions, and lemma functions. Verus operates as an Automated Theorem Proving (ATP) system: it translates the program into SMT formulas and, with the assistance of user-provided proof hints, checks whether the Rust code satisfies the specifications using the SMT solver Z3."

The paper notes that When verification succeeds, Z3 can emit a proof trace, but these traces are designed for machine consumption rather than human understanding. For example, the Z3 proof for our small running example spans 10,003 lines, yet 81.69% of it consists of low-level reasoning, such as trivial equalities like x775 = x775.

VCoT-Lift is "an LLM-based framework that lifts low-level Z3 solver reasoning into explicit, human-readable Verus verification steps, exposing the solver’s internal reasoning as a VCoT and providing transparent ground truth for program verification. It addresses three core challenges: soundness, completeness, and conciseness through a four-stage pipeline that enforces soundness via direct interaction with the Verus verifier, improves completeness through an interactive loop between global transformation and targeted completeness checking, and enhances conciseness by principled pruning of trivial and redundant reasoning."

The four stages are: Proof Transformer, Proof Checker, Proof Pruner, and Proof Repair. The Proof Transformer aims to transform the internal reasoning of the Z3 proof into semantically equivalent Verus proofs, using a Z3 rule hierarchy that explicitly steers LLM attention toward reasoning steps more likely to be semantically informative, organizing all 36 Z3 proof rules into three importance levels: High-level rules (8), Medium-level rules (12), and Low-level rules (16). The Proof Checker evaluates the completeness of proofs produced by the Proof Transformer, grouping the eight high-level rules into five categories: lemma, th-lemma, modus ponens, quantifier, and unit resolution, with a dedicated checker agent for each proof-rule category. The Proof Pruner removes trivial and redundant steps to improve conciseness. The Proof Repair ensures the soundness of the transformed verification steps by systematically detecting and correcting syntactic and semantic errors, with the Verus verifier compiles and checks the program with the transformed proofs, and the resulting error messages are fed back to the repair agent, which iteratively refines the proofs until successful verification.

VCoT-Bench is built on Verus-Bench, a widely used public benchmark for Verus proof-hint generation, comprising 150 verified Verus programs. For each program, VCoT-Lift produces VCoT-Bench-Org, a ground-truth dataset with fully expanded verification reasoning. Compared to Verus-Bench, on average, it exhibits a 6.5x increase in proof lines (up to 32x), a 13.4x increase in assertions (up to 54x), and a 1.94x increase in lemma functions (up to 9x).

VCoT-Bench constructs VCoT completion tasks by digging 'proof holes' in VCoT-Bench-Org at the granularity of semantic blocks, where each semantic block falls into one of three categories: Lemma Blocks, Invariant Blocks, and Assertion Blocks. The benchmark is organized along three orthogonal dimensions, Ratio, Type, and Location. VCoT-Bench-Ratio evaluates an LLM’s ability to recover missing verification steps under varying degrees of information loss, yielding 1,159 VCoT completion tasks. VCoT-Bench-Type evaluates an LLM’s ability to reconstruct specific proof types (Invariant-removal, Assertion-removal, Lemma-removal), yielding 439 VCoT completion tasks. VCoT-Bench-Loc evaluates how the position of missing reasoning steps affects a model’s ability to recover the underlying logic, defining three removal zones: Front (first 33% of the VCoT), Middle (33%–66%), and End (final 33%), yielding 390 VCoT completion tasks.

The study evaluates "ten state-of-the-art LLMs in a zero-shot setting, comprising six proprietary models: GPT-5.2, GPT-5-mini, Claude Sonnet 4.5, Claude Haiku 4.5, Gemini 3, and Gemini 3 Flash; and four open-source models: DeepSeek V3.2 (685B), DeepSeek R1 (685B), Qwen 3 (8B, evaluated under both thinking and non-thinking inference modes), and gpt-oss (20B). Three metrics are used: Syntactic Accuracy (SynAcc), Semantic Accuracy (SemAcc), and Overall Accuracy (Acc). Overall accuracy is a weighted accuracy metric that emphasizes semantic correctness over syntactic correctness, computed as Acc = (N(3) + 0.5 N(2) + 0.25 N(1)) / N × 100%, where Level 3 is Both semantically and syntactically correct, Level 2 is Semantically correct but syntactically incorrect, Level 1 is Syntactically correct but semantically incorrect, and Level 0 is Incorrect in both dimensions."

Key findings from the study include:

Regarding proof-removal ratios: "Accuracy drops sharply as proof blocks are removed. With only 10% of blocks missing, the best model, Claude Sonnet 4.5, achieves just 71.58% accuracy, while the weakest, gpt-oss, reaches only 32.89%. When all blocks are removed (100%), turning the task into full VCoT construction, performance collapses: Claude Sonnet 4.5 falls to 17.22% and Qwen 3 think to near zero (0.66%). This shows current LLMs do not reason from first principles but rely heavily on local pattern matching and syntactic scaffolding. Also, performance falls sharply as block removal increases from 10% to 40%, then degrades much more slowly from 40% to 100%, reflecting the loss of critical structural anchors in the verification logic. Additionally, Performance is strongly influenced by model scale, and current reasoning-oriented paradigms can inject noise into verification, as Qwen 3 generally outperforms its 'thinking' variant, and Gemini 3 Flash overall surpasses Gemini 3."

Regarding proof types: Across most models, assertion completion has the lowest accuracy. Even the strongest model, Claude Sonnet 4.5, achieves only 39.55% on assertions, compared to 68.71% on loop invariants and 51.54% on lemma functions. Also, loop invariant completion achieves the highest accuracy, but also shows the widest spread across models, ranging from 68.71% (Claude Sonnet 4.5) to 10.03% (Qwen 3 think), a 58.68% gap, indicating loop invariants are the most discriminative proof type.

Regarding proof locations: "Across all strong models, performance drops most sharply when missing blocks occur in the Middle of the proof. For example, Claude Sonnet 4.5 falls from 69.04% (Front) to 46.35% (Middle), and Gemini 3 from 62.69% to 36.15%. Also, Middle-block performance is not driven by model scale; instead, models optimized for low-latency reasoning may better track intermediate verification states, while larger, more verbose models are more prone to semantic drift."

The paper concludes that "VCoT can go beyond evaluation, providing a concrete supervision signal for training, diagnosing, and guiding learning-based verification systems toward symbolic alignment, and reframing the field from whether models pass verification to whether they can truly reconstruct and reason through the underlying verification logic."

Improvements for AI systems

Based on the paper, here are the specific improvements I can make to AI systems and what the improved system can do:

Improvement: Add a dedicated module that explicitly reconstructs Verification Chain-of-Thought (VCoT) before generating proof hints. This module decomposes the verification task into sequential, human-readable steps (e.g., establish sequence property → verify loop invariant → bridge loops → finalize postcondition) rather than directly outputting proof hints.

What the improved system can do:

  • Generate proof hints that are logically sound and complete, not just syntactically plausible.

  • Recover missing proof steps even when 40–100% of context is removed, because it reasons from first principles rather than local pattern matching.

  • Explain why each proof step is needed, enabling human auditability.

Improvement: Separate syntactic correctness from semantic correctness in the generation process. First generate a semantically complete VCoT (ignoring Verus-specific syntax), then translate it into syntactically valid Verus code using a dedicated syntax-constrained decoder or repair agent.

Improvement: Modify the attention mechanism to prioritize structural anchors in the proof—critical steps that establish invariants, bridge loops, or finalize postconditions. These anchors are identified via the Z3 rule hierarchy (high-level rules like unit-resolution, lemma, mp).

Improvement: Add a type-checking layer that enforces Verus-specific type constraints (e.g., explicit int conversions, parenthesization of nested casts) during generation. This layer is trained on curated repair examples and grammar rules from VCoT-Lift.

Improvement: Dynamically adjust reasoning depth based on task complexity. For simple, local proof steps (e.g., reflexivity, commutativity), use direct pattern matching. For complex, multi-step deductions (e.g., loop invariants, lemma applications), activate verbose chain-of-thought reasoning.

Improvement: Implement a hierarchical proof decomposition strategy that splits long Z3 proofs into semantic blocks (lemma, invariant, assertion) and processes each block with a specialized sub-agent, then aggregates results.

Capability Current Best (from paper) Improved System (projected)

Accuracy at 10% proof removal 71.58% (Claude Sonnet 4.5) 85–90%

Accuracy at 100% proof removal 17.22% (Claude Sonnet 4.5) 40–50%

Assertion completion accuracy 39.55% (Claude Sonnet 4.5) 60–70%

Middle-located proof completion 47.69% (Gemini 3 Flash) 65–75%

Syntactic accuracy on assertions 28.08% (Gemini 3 Flash) 70–80%

Semantic accuracy on loop invariants 62.59% (GPT-5.2) 80–85%

The improved system would not only generate correct proof hints but also reconstruct and reason through the entire verification process, matching or exceeding the deductive capabilities of automated theorem provers like Z3, while remaining transparent and auditable for human developers.

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.

Sources

Related papers