Concise TLA+ tutorial with state enumerating and symbolic model checking

Here are a set of TLA+ tutorials for beginners. The aim is to quickly teach a sufficient and necessary skill set to do real interesting work in TLA+. The cheatsheet is even valuable for those with TLA+ experience.

Links

• Full writeup
• Markdown with syntax highlighting
• Permalink
• TLA+ cheatsheet