We are collaborating with colleagues at Mozilla to investigate and help guide the design of the Rust language by reasoning about the soundness of its type system. By creating formal models of key features, we can identify challenging test cases to type-check as well as (hopefully) prove type soundness. We are particularly interested in modeling Rust's novel support for statically checked manual memory management.