| > TLA+ is not generally used for end-to-end checking of actual program code, unlike Coq. To my knowledge, TLA+ is never used for checking program code. At least, I've never heard of anyone doing it. > model checking is helpful in some cases, but it's not a generally useful tool I strongly disagree. 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. Consider Raft, for instance, which was formally verified in Coq. You know what they did first? Write a TLA+ model, and then model check that until they got the design right. Trying to start in Coq (with an incorrect design) would not have been smart. Model checkers are extremely useful tools. ---- Going further, the TLA+ spec of Raft is less that 500 lines. The Coq proof of TLA+ is ~50,000 lines. It resulted in a verified implementation that to the best of my knowledge, no one uses in production. It's a nice achievement, but in terms of usefulness? TLA+ has Coq beat by a country mile. |
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.