As per the previous message, I think wombat2 is a good fit for TLA+, both at the pluscal level and the TLC/TLAPS level.
So I think a more useful thing to do than my current effort will be to create a typed version of TLA+, using my type system. I think it is possible to create a full general purpose programming language that contains TLA+ (approximately) as a part.
I plan to match the syntax very closely, within the limitation that my syntax system can't do backtracking.
Don't hold your breath. I'm guessing it will take years. If anyone wants to help please leave a comment. Left to my own devices I will plan to use: my syntax system; python; copy the TLAPS method of talking to backend solvers (however when there is a proof I eventually want to bring it into the language as wombat2-style code). I'm open to alternative plans (that don't mention java).
Firstly I need to get into actually using TLA+ for a while.
