> Most of the value I get from TLA+ is as a software design tool. It's also just a fun language to write stuff in.

This sounds very intriguing. It guess there's at least some learning curve, but maybe it'll be a fun experiment vs. P&P in future. ;)