Hi everyone,
For the past few months I've been working on a TLA+ Guide (www.learntla.com). It's aimed at a less rigorous audience than Specifying Systems or the Hyperbook are: it's a lot less comprehensive and in-depth and focuses more on patterns and troubleshooting. The hope is that it'll be useful for software developers who may not necessarily need the full power of TLA+ but would benefit from having something more sophisticated than unit tests.
It's still in early drafts but I would love to get some feedback. Feel free to check it out! And please let me know if something is confusing, explained poorly, or flat-out wrong. Writing v1 is the easy part, after all. ;)
Hillel
PS: While I think it's ready to share with you folks, it's definitely not ready to fully publicize, and I plan on doing five or six more rounds of editing to get it there. Doesn't even have exercises yet.