Paper and pencil should be enough. The syntactic analyzer is nice to have but Lamport really pushes the value of writing down your thoughts in formal logic, as

Paper and pencil should be enough. The syntactic analyzer is nice to have but Lamport really pushes the value of writing down your thoughts in formal logic, as an act. Model checking isn't something you do iteratively - by the time you have a spec amenable to model checking, you'll pretty convinced it's correct. Mostly, model checking will catch errors where you didn't accurately translate your thoughts to TLA+.