iirc the formal correctness of Rusts memory model was proven by Ralf Jung https://research.ralfj.de/thesis.html