AIUI, that is what the MIR formalization work is about, and it seems to be moving along fine. My impression is that covers essentially all the interesting parts of Rust worth specifying formally.