As part of defining the Rust semantics they will certainly tackle the question of the memory model. Dreyer and company have a track record of providing semantics and reasoning principles for weak memory models (like C11).

You might have to wait a while for a rigorous semantics though.