The closest thing is probably RustBelt [0], which proved the soundness of a subset of Rust that included borrowing/lifetimes. This was later extended to include relaxed memory accesses [1].

Neither of these papers include the trait system, unfortunately, and I'm not aware of another line of research that does (yet?).

[0]: https://dl.acm.org/doi/10.1145/3158154

[1]: https://plv.mpi-sws.org/rustbelt/rbrlx/paper.pdf