Just yesterday, we submitted our paper RustBelt: Securing the Foundations of the Rust Programming Language.
Quoting from the abstract:
Rust is a new systems programming language that promises to overcome
the seemingly fundamental tradeoff between high-level safety
guarantees and low-level control over resource management.
Unfortunately, none of Rust's safety claims have been formally proven,
and there is good reason to question whether they actually hold.
Specifically, Rust employs a strong, ownership-based type system, but
then extends the expressive power of this core type system through
libraries that internally use unsafe features. In this paper, we give
the first formal (and machine-checked) safety proof for a language
representing a realistic subset of Rust. Our proof is extensible in
the sense that, for each new Rust library that uses unsafe features,
we can say what verification condition it must satisfy in order for it
to be deemed a safe extension to the language. We have carried out
this verification for some of the most important libraries that are
used throughout the Rust ecosystem.