Hi Irwan,
Short answer: yes I agree. (and noting that Coq changed name to Rocq recently)
Thinking more deeply, I like their description of a continuum from accessible, low complexity methods to full automated proofs. Model checking - which is usually how TLA+ is used - is on their diagram, and it's also not the simplest technique. Calling out that the simplest thing is to just write more tests (up to some point of saturation) is an interesting reality check when considering the value of any formal methods type work.
I think integrating TLA+ with other techniques and having modeling interact well with other engineering processes is good. For instance, linking testing with a TLA+ model, like we've been doing with trace validation recently, is nice. It means your new TLA+ model might be checked against implementation code in CI, and the client could be reminded that the model exists whenever they break the validation step. I'm sure other things could add this type of value too.
I was actually at a presentation of this idea a few months ago by coincidence, and that's the sort of impression it left on me.
Best,
-Finn