I think I've seen on HN stuff built on TLA+ but with a typescript-like syntax. A lot of people argue though that by making it more programming-language-like, vs math-like, that you're trading better tools for the job in exchange for what's familiar.

I don't use TLA+ yet, I'd like to learn, but I've followed a lot of discussions on HN regarding this.