Verus：使用线性幽灵类型验证 Rust 程序

Rust 编程语言提供了一种强大的类型系统，检查线性和借用，允许代码安全地操作内存而无需垃圾回收，使 Rust 成为开发低级、高可靠性系统的理想选择。对于此类系统，形式验证可以用来证明功能正确性属性超越类型安全。本文介绍了 Verus，这是一个基于 SMT 的工具，用于正式验证 Rust 程序。通过 Verus，程序员使用 Rust 语言表达证明和规范，从而使证明能够利用 Rust 的线性类型和借用检查。我们展示了这如何允许证明操作线性类型的权限，从而使 Rust 代码安全地操作内存、指针和并发资源。Verus 使用一种新颖的模式系统组织证明和规范，该系统区分未检查线性和借用的规范与已检查线性和借用的可执行代码和证明。我们在一个小的 λ 演算中形式化 Verus 的线性、借用和模式，为此我们证明了规范和证明的类型安全性和终止性。我们通过一系列示例展示 Verus，包括操作指针的代码（基于异或的双向链表）、具有内部可变性的代码和并发代码.