Rust aims to be a safe programming language applicable to systems programming applications. In particular, its type system has strong guardrails to prevent a variety of issues, such as memory safety bugs and data races. However, these guardrails can be sidestepped via the unsafe keyword, allowing more expressive control of memory at the cost of bearing responsibility to prevent undefined behaviour. This motivates a need to verify programs for an absence of safety issues in the presence of unsafe code. Moreover, safety aside, programs also need to be verified for functional correctness, ensuring that they meet their specifications.

In this research proposal, we explore what it means to do Rust verification. Specifically, we explore which properties are worth verifying for Rust; what techniques exist to verify them; and which code is worth verifying. In doing so, we motivate an effort to verify safety properties of the Rust standard library, presenting the relevant challenges along with ideas to address them.