I was actually arguing that the Rust community should definitely look into formal methods, in particular TLA+ and Ada/Sparks.
The borrow-checher/free-of-data-races/fearless-concurrency taglines are only focused on memory bugs and unfortunately the community is still focused on memory bugs as well.
Thankfully, it didn't prevent the Tokio team that had to deal with concurrency bugs (beyond memory safety) to write a model checker for Rust code called Loom https://github.com/tokio-rs/loom.
Nethertheless this proves that Rust should grow beyond the fearless concurrency/borrow checker narrative because concurrency brings a lot of problems and memory/lifetimes are only part of the equation.
I assumed that statement was implying that understanding this problem in Rust is easier than in TLA+ which I disagree with.
I think TLA+ can state the problem and demonstrate it more clearly.
Apologies if I misunderstood! Text. I agree with your comment overall as a formal methods nerd/evangelist. :)