Here's an interesting blurb about how they were using TLA+. TL;DR is is that, unsurpisingly, model checking trumps proving in roi:<p>We have found formal specification and model-checking to yield high return on investment. In addition
to model checkers, many formal specification methods also support formal machine-checked proof.
TLA+ has such a system. The TLA+ proof system has several compelling benefits; for example, it supports
hierarchical proof. After doing only a small number of such proofs, author C.N. has found that
hierarchical structure is an effective way to handle the otherwise overwhelming amount of detail that
arises in formal proofs of even small systems. Another benefit of the TLA+ proof system is that it takes<p>as input the same specification text as the model-checker. This allows users to find most of the errors
quickly using the model-checker, and switch to the proof system if even more confidence is required.
Even though formal machine-checked proof is the only way to achieve the highest levels of confidence
in a design, use of formal proof is rarely justified. The issue is cost; formal proof still takes vastly more
human effort than model-checking. We are continuing to experiment with the TLA+ proof system, but
currently model-checking remains the sweet spot in return on investment for our problem domain. We
suspect that proof will only be a worthwhile return on investment for one or two of the most critical
core algorithms.