> The number of people in industry who use either tool is incredibly small and is likely to remain so

I agree, but I see some chance of TLA+ of getting wide(r) adoption, precisely because it is rather easy to learn and uses math that most engineers are already familiar with. Also, it allows gradual verification: specification -> model-checking -> proof (with each additional step being completely optional)

> not that everyone and his brother can use formal methods for every WordPress website they churn out.

I don't know about WordPress websites, but Amazon engineers do use TLA+ to specify many (most?) AWS services.