Here's a specification of the BNF grammar of the ASCII syntax used by SANY. It's not a full specification of the syntax, which includes much more than just a BNF grammar.
Here and here you can find some specifications of PlusCal.
Part 4 of Specifying Systems contains a mathematically precise and complete, but not entirely formal specification of TLA^(+). The Temporal Logic of Actions has a similar treatment of just TLA.
For one, K Framework didn't exist then. For another, it's not a formal specification of TLA^(+); an informal mathematical specification is quite a common way for specifying formal systems. Finally, I'm not even sure K could specify TLA^(+); TLA^(+) is not a programming language and has no useful operational semantics, i.e. you can't interpret TLA^(+) in the same way you can a programming language (in fact, it's trivial to write TLA^(+) specifications of noncomputable "systems"). While TLA^(+) has much simpler semantics than any programming language, K, AFAIK, is not a general formal system specification language, but rather designed for the special case of programming languages (the TLA^(+) "rewrite rules" are "ordinary" inference used for proofs and don't correspond to the computations described by TLA^(+)).
Even TLC is not an interpreter for TLA^(+) in any conventional sense that we can talk of operational semantics as we normally do. TLC checks in a second an uncountable infinite number of computations, each of infinite length. Clearly, this is not done by interpretation in the same sense as for programming languages (model checkers for programming languages are abstract interpreters for those languages, but TLA^(+) isn't a programming language...).
In short, when we say that TLA^(+) isn't a programming language we don't mean it in a stylistic way or that it's not primarily designed for programming, but that the relationship between TLA formulas and the computations that they describe is different from that of a programming language in a very fundamental, mathematical way (even from languages like Agda, that are fundamentally programming languages). Crucially, the computations that a TLA formula describe do not correspond to the computations that arise from applying rewriting rules to it (i.e. its "operational semantics"). That's why a simple TLA formula can specify the behavior of a universal "halting decider", even though no such program exists. This difference is what gives TLA^(+) a unique combination of simplicity and power.
It's possible that K could specify TLA's inference rules as it does for type systems, but I don't think that doing that would specify the semantics of TLA in any meaningful way.
Perhaps as an addition: there's also a TLA+ encoding in the Isabelle proof assistant. To my knowledge, there are multiple encodings to TLA but this is a full fledged logic independent of HOL.
Just note that it isn't an encoding of TLA^(+) but of TLA (on top of HOL), and not quite TLA, either, but "raw" TLA, the stuttering-sensitive TLA-simplification.
Here's a specification of the BNF grammar of the ASCII syntax used by SANY. It's not a full specification of the syntax, which includes much more than just a BNF grammar.
Here and here you can find some specifications of PlusCal.
Part 4 of Specifying Systems contains a mathematically precise and complete, but not entirely formal specification of TLA^(+). The Temporal Logic of Actions has a similar treatment of just TLA.
Thanks. It's rather unusual to see a language specification in TLA rather than in something like K Framework.
For one, K Framework didn't exist then. For another, it's not a formal specification of TLA^(+); an informal mathematical specification is quite a common way for specifying formal systems. Finally, I'm not even sure K could specify TLA^(+); TLA^(+) is not a programming language and has no useful operational semantics, i.e. you can't interpret TLA^(+) in the same way you can a programming language (in fact, it's trivial to write TLA^(+) specifications of noncomputable "systems"). While TLA^(+) has much simpler semantics than any programming language, K, AFAIK, is not a general formal system specification language, but rather designed for the special case of programming languages (the TLA^(+) "rewrite rules" are "ordinary" inference used for proofs and don't correspond to the computations described by TLA^(+)).
Even TLC is not an interpreter for TLA^(+) in any conventional sense that we can talk of operational semantics as we normally do. TLC checks in a second an uncountable infinite number of computations, each of infinite length. Clearly, this is not done by interpretation in the same sense as for programming languages (model checkers for programming languages are abstract interpreters for those languages, but TLA^(+) isn't a programming language...).
In short, when we say that TLA^(+) isn't a programming language we don't mean it in a stylistic way or that it's not primarily designed for programming, but that the relationship between TLA formulas and the computations that they describe is different from that of a programming language in a very fundamental, mathematical way (even from languages like Agda, that are fundamentally programming languages). Crucially, the computations that a TLA formula describe do not correspond to the computations that arise from applying rewriting rules to it (i.e. its "operational semantics"). That's why a simple TLA formula can specify the behavior of a universal "halting decider", even though no such program exists. This difference is what gives TLA^(+) a unique combination of simplicity and power.
It's possible that K could specify TLA's inference rules as it does for type systems, but I don't think that doing that would specify the semantics of TLA in any meaningful way.
Perhaps as an addition: there's also a TLA+ encoding in the Isabelle proof assistant. To my knowledge, there are multiple encodings to TLA but this is a full fledged logic independent of HOL.
Just note that it isn't an encoding of TLA^(+) but of TLA (on top of HOL), and not quite TLA, either, but "raw" TLA, the stuttering-sensitive TLA-simplification.