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

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 https://dl.acm.org/doi/10.1145/3158154 [1]: https://plv.mpi-sws.org/rustbelt/rbrlx/paper.pdf https://plv.mpi-sws.org/rustbelt/rbrlx/paper.pdf