Not just that. F* is convenient for code-level specification, much like Ada SPARK, JML/OpenJML for Java, and ACSL/Frama-C for C, but it's quite hard to specify global correctness conditions in it, like "the database is always consistent", or "no data is ever lost", which is where TLA+ shines.
The gap between local, code-level correctness properties and global ones is a hard one to cross. I am not aware of any tool that can do both (i.e. end-to-end verification) in a way that isn't excruciatingly hard.
And not just _that_, but TLA+ is really good at expressing liveness conditions, like "the database is EVENTUALLY consistent" or "the algorithm will eventually terminate." Most other formal methods don't cover that.
Right; not out of the box, anyway (many proof assistants are powerful enough for deep embedding of arbitrary logics, but, of course, using them is beyond the affordable reach of nearly all software shops). Many can express termination out of the box, which, in theory, can suffice to express most (all?) liveness properties, certainly many useful ones, but again, this is expressed at the function level, and hard to do for global liveness properties.
The gap between local, code-level correctness properties and global ones is a hard one to cross. I am not aware of any tool that can do both (i.e. end-to-end verification) in a way that isn't excruciatingly hard.