[tlaplus] Experience proving liveness with TLAPS

["tal...@xxxxxxxxx" <talex5@xxxxxxxxx>]

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/afe268c8-f590-4f3b-9c1f-c41b4085ff0an%40googlegroups.com.