That is the point some seem to fail to understand: said model is absolutely irrelevant if we already have production releases of an implementation of Rust.
A standard is not supposed to be academically rigorous. A standard is a specification of the current behavior so that multiple implementations can meet the current requirements, and thus ensure interoperability and compatibility.
It makes absolutely no sense to talk about "a formalized model" because rust is already used in production without said formalized model. The absence of said formalization is irrelevant. The only thing that matters is that the current behavior is specified and set in stone so that it serves as a target set in stone that anyone in the world can target and expect to interoperate.
It's terribly simple: if a rust v1.25 exists then it's behavior and interfaces can be described. Obviously. That description is what a standard is: an implementation target set in stone that others can use as a reference.
If all you have as a reference is a bunch of test cases without any underlying reasoning as to why input A leads to output B, then that's not really a useful target to implement against. At that point you can just go the direct route, not bother with any standard and just implement directly against the Rust compiler.
I don't know how to describe it differently as GP, but I'll give it a try. Until a formalised model is built, there is no way to describe it's behaviour that wouldn't come down to writing down the implementation that's currently in the compiler (apart from specifying it by example, which would be even more expansive).
It _might_ (don't quote me on this) be possible to more easily formalize and standardize borrow checking if you leave out non-lexical lifetimes (which were added rather recently), but that's a bad idea because you would lose a lot of functionality, and an alternative compiler with an incompatible implementation of NLLs could split the ecosystem, which obviously nobody wants.