> If your understanding of the domain isn't thorough, is TLA+ going to be much help? I suspect it could, actually, because it lets you formalize and work with

> If your understanding of the domain isn't thorough, is TLA+ going to be much help? I suspect it could, actually, because it lets you formalize and work with the implications of the understanding you do have without getting bogged down in the details of actual coding. Seems like this could give you the opportunity to debug your mental model much earlier in the process. (I confess I haven't actually tried TLA+, but I plan to.)