[Jtsummers]

> Additionally it requires someone to meticulously compare the mathematical model with the implementation code, to validate that what is written actually maps to what was designed.

This is a deficiency in TLA+ (and many other systems), but it's not a good enough reason to discard or dismiss it. The industry alternative to TLA+ is not something that traces fully and easily from spec to code, but mostly to use informal, largely prose, documents as their specification (if they specify anything at all). TLA+ is a massive improvement on that even if it's not a perfect tool. Same for Alloy and other systems. It's better if people model and specify at least portions of their system formally even if it still takes effort to verify the code correctly implements that specification, effort they have to expend anyways but with greater difficulty lacking any thing approaching a formal specification.