> TLA+, which has gained quite a lot of popularity

Why do you think that? Outside of just toy examples, and vague examples of "AWS uses that", I don't know of any actual code which has TLA. Most of the things you can do with TLA, you can do with informal math notation quite easily.

Do you have any real world long term usage examples?