My old software page has not yet been ported to this new design. I’ll
get to it one of these days.
The TLA+ Proof System, a suite of tools for reasoning about
Leslie Lamport’s Temporal Logic of Actions. I built the
Proof Manager component of this system during 2007-2008. Since
2009, the maintenance and further development of this tool has been
taken over by Denis Cousineau.