Proving liveness with TLA - Thomas Leonard's blog
roscidus.com
The TLA Toolbox now has support for proving liveness properties (i.e. that something will eventually happen). I try it out on the Xen vchan protocol. …