> RustBelt is a formal model of Rust’s type system, together with a soundness proof establishing memory and thread safety. [1]

[1] https://people.mpi-sws.org/~jung/thesis.html