We introduce \textsc{Thrust}, a new verification tool for ensuring functional correctness in \textsc{Rust}, distinguished by its strengths in \emph{automated} verification, including the synthesis of inductive invariants for loops and recursive functions. \textsc{Thrust} is built on a novel dependent refinement type system for \textsc{Rust} and refinement type inference techniques based on Constrained Horn Clause (CHC) solvers. Leveraging advantages of the type system, \textsc{Thrust} also supports semi-automated verification utilizing user type annotations to complement CHC solvers in cases where automatic constraint solving is unsuccessful, as well as \emph{modular} verification at the function and subexpression levels.
\textsc{Thrust} also achieves \emph{precise} verification, especially for programs involving pointer aliasing and borrowing, without sacrificing the benefits of automated verification, by incorporating the notion of \emph{prophecy} into the refinement type system: it not only enables strong updates by leveraging the aliasing XOR mutability'' guarantee provided by \textsc{Rust}'s type system, but also achieves propagation of update information to the original owner upon mutable borrow release through the use of a prophecy variable. Incorporating prophecy into a refinement type system is itself challenging and requires certain tricks, as discussed in this paper, making a theoretical contribution and paving the way for further research into prophecy-based refinement type systems. While our type system addresses the challenge, we keep it simple for extensibility, specifically by delegating the guarantee ofaliasing XOR mutability,'' and, more technically, the ``well-borrowedness'' of the program in the sense of the \emph{stacked borrows} aliasing model, to \textsc{Rust}'s type system, allowing us to focus on reasoning about functional correctness and propagating update information through prophecy variables. Compared to \textsc{RustHorn}, another automated verification tool based on prophecy, our approach leverages the strengths of refinement types to support modular verification, higher-order functions, and refinement of data stored in algebraic data structures.
We implemented \textsc{Thrust}, a refinement type inference tool as a plugin for the \textsc{Rust} compiler, and evaluated it using \textsc{RustHorn} benchmarks, as well as additional new benchmarks, including those that are beyond the capabilities of \textsc{RustHorn} and other semi-automated verification tools, obtaining promising results.