Incredibly, there are already proofs regarding memory safety of the Rust model: ftp://ftp.cs.washington.edu/tr/2015/03/UW-CSE-15-03-02.pdf