Re: [tlaplus] Using TLAPS for industrial stuff?

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.

Stephan

On 12 Sep 2019, at 10:28, Thomas Gebert <thomasgebert@xxxxxxxxx> wrote:

This is a more generic question, but I had a bit of trouble finding concrete answers on this.

You can find a bunch of examples of industry usage of people using TLA+ with TLC to verify their designs, and that's really cool, but it made me wonder; does anyone know of any examples of using the proof system for that? Is this a silly question?

--
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/52189418-0691-4252-b43d-94a86782676d%40googlegroups.com.

--
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.