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

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 can systematically reconstruct the explicit deductive steps 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' ability to reconstruct 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 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.

As large language models are increasingly used to help develop software, it is important to know whether they can support programs that require strong correctness guarantees. This paper studies this question for Rust verification, where a program is mathematically checked against its intended behavior. Existing evaluations usually treat verification as a black box. They only check whether the final proof is accepted, without examining how the model reaches that result. We introduce VCoT-Lift, a framework that converts low-level solver reasoning into explicit, human-readable verification steps. Using this framework, we build VCoT-Bench, a benchmark that evaluates whether models can reconstruct missing steps in the verification process. Our experiments on ten state-of-the-art models show that current models remain fragile. Their performance drops sharply when proof context is removed, and they struggle especially with multi-step reasoning and state-dependent proof steps. These results show that final verification success alone is not enough to evaluate model capability. By exposing the intermediate reasoning behind verification, VCoT-Bench provides a fine-grained way to diagnose model failures and offers a richer training source for future proof-generation models.