From the projects they mention, the only one I can see really benefiting from TLA+ would be memcached. For most things it doesn't make a whole lot of sense to u

From the projects they mention, the only one I can see really benefiting from TLA+ would be memcached. For most things it doesn't make a whole lot of sense to use it, unless you're writing a potentially distributed app. If you just want to model a regular program, then you'd be better off looking at PlusCal, which is more oriented to regular programs that aren't designed to be distributed. It compiles down to TLA+ so you get the same benefits, but with an easier to understand syntax. Edit: Also if you want to learn about how famous programmers work, then there's no better source than the book Coders at Work by Peter Seibel. http://www.codersatwork.com/ http://www.codersatwork.com/