一句话：提出基于预言的 Rust 依赖精化类型系统与推断工具 Thrust，实现自动化的函数正确性验证。
Thrust 是面向 Rust 函数正确性验证的新工具，兼顾自动化与对指针别名、借用等特性的精确推理。它提出带预言（prophecy）的依赖精化类型系统，并基于 CHC 求解器做精化类型推断，可自动合成循环与递归函数的不变式，也支持借助用户标注的半自动验证及函数/子表达式级模块化验证。系统将别名 XOR 可变性及 stacked borrows 意义上的 well-borrowedness 委托给 Rust 类型系统，并用预言变量把可变借用释放后的更新信息传播给原所有者。作者将其实现为 rustc 插件，在 RustHorn 及新增基准上评估，取得良好效果。
We introduce Thrust , a new verification tool for ensuring functional correctness in Rust , distinguished by its strengths in automated verification, including the synthesis of inductive invariants for loops and recursive functions. Thrust is built on a novel dependent refinement type system for Rust and refinement type inference techniques based on Constrained Horn Clause (CHC) solvers. Leveraging advantages of the type system, 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 modular verification at the function and subexpression levels. Thrust also achieves precise verification, especially for programs involving pointer aliasing and borrowing, without sacrificing the benefits of automated verification, by incorporating the notion of prophecy into the refinement type system: it not only enables strong updates by leveraging the “aliasing XOR mutability” guarantee provided by 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 of “aliasing XOR mutability,” and, more technically, the “well-borrowedness” of the program in the sense of the stacked borrows aliasing model, to Rust ’s type system, allowing us to focus on reasoning about functional correctness and propagating update information through prophecy variables. Compared to 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 Thrust , a refinement type inference tool as a plugin for the Rust compiler, and evaluated it using RustHorn benchmarks, as well as additional new benchmarks, including those that are beyond the capabilities of RustHorn and other semi-automated verification tools, obtaining promising results.
@article{paperbot3114,
title = {Thrust: A Prophecy-Based Refinement Type System for Rust},
author = {Hiromi Ogawa and Taro Sekiyama and Hiroshi Unno},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729333}
}