I am not aware of any significant use of TLAPS in industry yet, and quite frankly I don't think that it would be usable at this point for proving the correctness of any significant system. One of the problems is that it requires people to state a full inductive invariant. Of course, I'd be more than happy to be convinced of the contrary.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/02FA2C80-25FB-4A1C-AB0C-CCBEA521A607%40gmail.com.