[tlaplus] Re: Experience proving liveness with TLAPS

[Kant Seemee <kant.seemee1776@xxxxxxxxx>]

A very interesting read! Thanks for documenting the issues you ran into with TLAPS.

On Thursday, January 1, 2026 at 11:50:50 AM UTC-6 tal...@xxxxxxxxx wrote:

I've been learning how to prove liveness properties with TLAPS, and I've now succeeded in updating my old vchan specification to do that. If anyone is interested, I've written up my notes about it here:

https://roscidus.com/blog/blog/2026/01/01/tla-liveness/

In particular, I've included a list of problems I encountered, along with solutions/work-arounds.

-- 
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 visit https://groups.google.com/d/msgid/tlaplus/b12e3f0f-647f-4d90-ab2f-68245dc7446fn%40googlegroups.com.