Sure — if and when I get around to writing them :) Looking at your proofs will probably make this a lot easier. After all, the principles of proof are very similar in pretty much every system. But if you want to get a sense of what a methematical proof in TLA+ looks like (as opposed to algorithm proofs, which make up most TLA+ examples), see the appendix to this paper: https://lamport.azurewebsites.net/pubs/proof.pdf
But it’s very important to know that TLA+ has very different usage goals from Coq/Lean/Isabelle, and so makes very different design tradeoffs. The tools are certainly not interchangeable.
Coq, Lean and Isabelle are first-and-foremost research tools. As such, they are completely general purpose, very powerful, but also very, very complicated. TLA+, on the other hand, was designed for use by ordinary engineers to specify and verify large, real-world digital (software or hardware) systems. This means that TLA+ is not generally appropriate for doing high math (e.g., because it’s untyped, it doesn’t even have operator overloading, which alone would make it unappealing for serious math; then again, not much serious math is done formally, anyway), and isn’t designed for logicians to explore various logics (it’s classical logic only). In addition, it’s syntactic/symbol manipulation capabilities are very limited, so while you could specify a programming language, as you’ve done, the result is going to be much messier (although specifying low-level languages with simple syntax, like machine- or byte code, can be very elegant).
OTOH, TLA+ is truly exceptional in its ease of learning and its capabilities when it comes to specifying and verifying systems and algorithms. In many respects, it’s computational theory is richer than Coq’s (although Coq is so general that some people have embedded TLA, the computational theory of TLA+ in Coq; but TLA+ has it out of the box). In addition, when used in industry, people hardly ever use TLA+’s proof system. Not because it’s inadequate for proving the correctness of algorithms — it truly excels at that — but because formal proofs are, in general and regardless of the choice of tool, not very cost effective. Instead, TLA+ has a model checker that lets you verify your propositions about your system completely automatically — you just state them and press a button — albeit, only on small, finite instances. This is more than sufficient for industry use, as, while there have been multiple cases of informal (published and peer-reviewed) correctness proofs later found to be wrong with a model-checker, I am not aware of any cases where a model checker result was found wrong, despite running on small instances, and so not qualifying as proof.
So the choice between TLA+ and Coq/Isabelle/Lean is usually simple. If you’re an academic researching new logics, new programming languages, or complex formal mathematics, you’ll choose Coq/Isabelle/Lean. If you’re an engineer trying to design a complex or subtle system or algorithm, you’ll likely choose TLA+.
