Exactly what I was feeling in my gut... but then what is the overwhelming advantage over rust that as far as I know is designed specifically for this kind of problems but is much easier to reason about, at least coming from standard programming?
This is not a shortcoming of Rust in particular. No programming language can be as expressive and as simple as a specialized specification language like TLA+ (it could be by essentially embedding a specification language in some specification tier of the language -- like the type level in languages with dependent types like Idris or the contract level like languages with formal contracts like Java with JML or SPARK, but this comes at the cost of either less expressive power and/or much increased complexity)
Then, as a consequence of clearly expressing all the behaviors my system might express, TLC (the TLA+ model checker) is able to exhaustively search these possibilities for bugs. This is at best intractable for any system where you are unable to abstract out the things that "don't matter", like in Rust. There are just too many variables (literally) in the search space.
That said, there's nothing particularly special about TLA+, or especially PlusCal. They just provide language features such as first-class sets and clearly-defined atomic state transitions that make it very easy to describe a system without too much irrelevant "stuff". The only particularly notable feature of the modelling portion of the languages is nondeterminism, which is necessary to express the boundaries of your model (e.g. nondeterminism is how you model the "receive from network" function as "a function that either returns some data or throws some error").
One could even imagine using Rust (to use your example) as a modeling language. You'd need to add nondeterminism (or another means of specifying contracts), and a way to specify temporal invariants to check. And also annotate which functions act as mutexes and which may block waiting for I/O. And you'd probably want to stub out container types so the model checker doesn't have to model their implementations. But once you've done all that, your mutant Rust is starting to look a heck of a lot like PlusCal, only more complicated.
TLA and the TLA tools form a model checker. The TLA language is not used to do computations,but, rather, is used to describe properties and behavior of complex systems. The TLA tools then machine validate the descriptions to assure that the evolution of a system with the given behaviors will satisfy expected correctness properties. A TLA specification tells you that if your system is implemented (in a computer language, like say Rust) according to the description then the systems operation will satisfy the validated correctness properties.
TLA is about answering the question "Do I properly understand my problem and will my solution logic satisfy problem needs?". Rust doesn't help answer that question.