Proving liveness with TLA - Thomas Leonard's blog

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