No spec, because technical details are complex, but spec, when it is written, will just be an elaboration of "It is an error to access a place, when an access conflicts with a loan, and the loan is live". This has never changed since Rust 1.0, more than 5 years. Spec will just need to define "place" and "live" and that takes time.