[zozbot234]

> Spending time trying to "prove" in Coq an incorrect, flawed specification is an insane waste of time. A model checker can show you the problems in (literally) seconds.

Sure, if there's anything a TLA+ model checker is good at it's searching for counterexamples. But in pretty much any case where such a search is computationally viable, it's also easy to set it up in a proof assistant. By and large, model checkers use the exact same toolset under the hood as the "sledgehammer" automated proof search in a proof assistant, such as SAT and SMT satisfiability solvers.

> It resulted in a verified implementation, that to the best of my knowledge, no one uses is production.

No one uses a TLA+ model directly in production either, because that's not what TLA+ is. The question only makes sense for a tool like Coq where one can work end-to-end with an actual implementation.

[erichocean]

> No one uses a TLA+ model directly in production either

This is false. Many, many companies use software derived from TLA+ models "directly in production." Amazon and Microsoft (Azure) are the two biggest examples. Neither relegate TLA+ usage to "R&D" on experimental system. Both are using it to develop and harden actual production systems used by millions (billions?) of people daily, and the TLA+ toolset is used daily by normal production engineers, not academics (as is true of Coq).

Coq is great, I like it a lot. As of 2021, it's not very practical for the kinds of problems normal software engineers encounter whereas TLA+ is.