It would be impossible. The whole point of TLA is to test & document the high-level design. You can only generate complete implementation for toy problems (and that is a feature)
I wouldn't say that's "the whole point." You can specify at any level you choose, even electronic circuits (in fact, TLA+ has been successfully used in the design of microprocessors). It's just that the most effective general-purpose use of formal methods, given our current technology, is in a high-level design (where high-level is relative to whatever your domain is), as formal methods are constrained by a certain amount of detail, and therefore it is best to use that budget on the actual tricky/subtle parts of the problem, rather than waste it on stuff that's fairly simple (translating the spec into code, which is simple but contains a lot of "uninteresting" detail).
I would still say that, though. For complex/ non-"toy" systems, the required level of detail increases so much, that if you specify it all in something like TLA+, even ignoring the performance aspects, it probably becomes too hard to understand it all and you lose most of the advantage that TLA+ is supposed to give you. It's not just about the "formal verification" part - it's about the whole cycle of model -> verify -> learn/improve understanding -> improve model.
And the fact that it was used to design microprocessors doesn't say that it can or should be used to specify all the details. I bet nobody ever attempted to do the layout from the TLA+ model; it's just like in software, TLA+ was used to design geo-distributed databases... but not to write any piece of the code; just to check that the general design is right.
> it probably becomes too hard to understand it all and you lose most of the advantage that TLA+ is supposed to give you.
Not necessarily. There are tools that compile C or Java to TLA+[1]. But, like all other code-level reasoning, when using them you are limited to very small programs.
> It's not just about the "formal verification" part - it's about the whole cycle of model -> verify -> learn/improve understanding -> improve model.
I agree, but again, that's because TLA+ is intended for industry use, not as a research tool, and as we simply don't have the technology to verify most real programs all the way down to code, TLA+ places an emphasis on the best ROI you can get from formal methods, in practice, given current technology.
