It's not a specification, but an interesting project is to formalize and prove safety guarantees of Rust: http://plv.mpi-sws.org/rustbelt/#publications http://

It's not a specification, but an interesting project is to formalize and prove safety guarantees of Rust: http://plv.mpi-sws.org/rustbelt/#publications http://plv.mpi-sws.org/rustbelt/#publications In order to do this, there also needs to be an unambiguous formal semantics of Rust, so one might even hope that this will turn into some form of official language specification.