Experience proving liveness with TLAPS

[tal...@gmail.com]

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.

[Kant Seemee]

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