TLA+ really is quite nice. I write most of my TLA+ specifications longhand and only bother with the toolbox when I think that refinement might be useful. Even then, it's mostly for SANY rather than TLC.
After noodling with with the spec for half an hour or so, I’ll usually have enough insight/confidence to start coding/debugging.
After noodling with with the spec for half an hour or so, I’ll usually have enough insight/confidence to start coding/debugging.