There's a forthcoming paper at PLAS (co-located with ACM CCS, in late October) that applies formal reasoning to a Rust-like type system. The contribution here

There's a forthcoming paper at PLAS (co-located with ACM CCS, in late October) that applies formal reasoning to a Rust-like type system. The contribution here is a formalization of borrowing and ownership semantics very close to Rust's, plus a sketch of how one would prove that these semantics give memory safety. The techniques can probably be adapted to an analysis of Rust itself. Benitez, S. "Rusty Types for Solid Safety." ACM PLAS 2016. https://sergio.bz/docs/rusty-types-2016.pdf https://sergio.bz/docs/rusty-types-2016.pdf (Full disclosure: Sergio and I are colleagues.)