Does this prove that the current borrowck rules are sufficient to catch all possible mistakes? For example, does it catch stuff like https://github.com/rust-lang/rust/issues/31287 or https://github.com/rust-lang/rust/issues/38899?
This helps demonstrate that one of the fundamental design goals of Rust, have a simple but limited system of borrowing built into the language, and allow more complex forms of managing reference types safely built on top of it as library features using `unsafe`, is a fundamentally sound design. In other words, you don't have to treat the language and all libraries using `unsafe` as one large system that you need to prove soundness of, but you can do modular proofs of the core language, and each library that adds a new type of memory and reference management, independently.
Those bugs you reference are simply bugs in Rust's borrow checker. The language used for the RustBelt paper, LambdaRust, is a language that is much simpler than Rust itself, making the borrow checking much easier but the language not as convenient to use (it is not intended to be used at all, just to act as a model of Rust).
The things you reference are simply bugs, but because of the fairly expressive syntax that Rust offers actually getting the borrow checker right can be be difficult in some cases.
I don't think that there are any theoretical concerns about the ability to write a correct borrow checker, just practical issues with the current implementation not correctly handling certain cases.
Is it really that trivial? When looking through https://github.com/rust-lang/rust/blob/master/src/librustc_b..., it is not at all clear that these rules cover everything to me. There are some complex side conditions, isn't it easy to miss something there?
The RustBelt work addressed one of the big open questions; is it possible to treat `unsafe` code in a modular fashion, or does all analysis of unsafe code have to consider all possible interactions with all other modules which use `unsafe` code as well?
That was in many ways quite a big question about the design of Rust; can you prove or very each module which uses `unsafe` independently?
The borrow checker, on the other hand, is an entirely local analysis. It can get quite complex, especially as you allow for more fine-grained borrow checking to make it convenient to use compound objects, and introduce non-lexical lifetimes which help reduce the number of restrictions on what you can do, but since it's entirely local, it's a much more tractable problem.
I think that it would be good to eventually formalize the full Rust borrow checker, and of course it's always good to fix these soundness bugs, but there are some more important open questions right now like fully specifying Rust's memory model (https://github.com/nikomatsakis/rust-memory-model) so it's possible to know what kinds of aliasing you can actually do in `unsafe` code, and which will be safe even under future versions of the compiler.
The RustBelt work so far is just a nice foundation getting Rust to be more formally analyzed and specified. There's a lot of work left to be done.