The crucial thing about TLA+ is that because it's not actually executable code your investment in it is completely up to you. You could decide to put in 100x the time if you wanted, you could decide to put in 0.1x the time if you wanted. Your investment in it is totally up to you and completely independent of the time you'd spend in writing the code.
TLA+ makes development faster, not slower (once you get a feel for how to use it).
I mean, it would be slower if you'd spend time writing mechanically-checked formal proofs, but that's working 10x for just slightly more confidence than you can get with TLC (a model-checker for TLA+) alone, so in almost all cases people just stick to specifying and model-checking.
I was working on something similar to say, stepped away, and saw your post. So I'll add to it:
TLA+'s place is as part of your design process (you have one, right?). It's the thing you do before committing any code to the project or radically restructuring an existing project (prototype code fits in the design process, but it shouldn't be considered committed most of the time). By spending a bit of time thinking about the design, and using tools like TLA+ to validate that design, you can save yourself months and years of heartache down the road.
By way of anecdote, some colleagues were working on a concurrent algorithm, needing to share data between two embedded processors talking over a databus. A bit more time spent on the design, versus the rather slapdash approach they took, would've saved them 6 months of debugging and tweaking until it worked. The issues were subtle, so it "worked" but wasn't totally correct and tracing the errors they were seeing back to that code was non-obvious (and hard, debugging embedded isn't trivial). It was quite literally a case where skipping a couple weeks of design cost them months later.
> TLA+'s place is as part of your design process ... By spending a bit of time thinking about the design, and using tools like TLA+ to validate that design
I think you dramatically underestimate the amount of effort required to produce a formal model of any nontrivial system, and overestimate the stability of system definitions in response to changing business requirements.
Eh. I used TLA+ for a few projects inside Microsoft. It probably takes a couple of weeks to write a spec for a complicated problem. Then less time to implement it, because all the heavy lifting has already been done - in many cases you're directly transcribing the spec logic without having to think very hard.
The sort of things for which you write specs are generally "core" functionality that doesn't change very often. If people are constantly mucking around in that area without writing specs, your system will be a pile of crap.
I think you dramatically underestimate the benefit of writing a formal model! I've run classes where we've managed to discover bugs in the client's actual production system with an afternoon of modeling.
How important is it to discover new bugs? Surely any large production system already has a backlog of tons of known ones. So if I want to fix bugs in my system, I can just go to the issue tracker and pick one.
I'm not underestimating anything because I'm not suggesting producing a formal model of arbitrary, nontrivial systems. My critical point is: Design your system before committing any code to the end result [0]. Formal methods and models are one tool in your designer's kit.
[0] This statement should be qualified with: Especially if it's at all novel to you, your team, your organization, or the world. And the amount of time to spend varies based on its true novelty. A team that's made hundreds of RoR sites can churn a new one out in a week with minimal upfront design effort. A team that's making the next RoR should probably spend more time thinking about what that means before making, or committing code to, it.
In practice, the effort is smaller and cheaper than finding bugs in other ways. But yes, learning where and how to best apply TLA+ takes some practice (less than learning a programming language, but more than learning a new build tool).
Going through Lamport's video lectures (https://lamport.azurewebsites.net/video/videos.html) is a great way to get the basics down. It proceeds at a fairly lesiurely pace so if you just block off some amount of time every day (say a video or two a day which usually works out to 30min - 1 hour depending on how well you want to practice the concepts in the video) you'll be able to use TLA+ by the end of a week or so.
It's so low-level, every time I try to look into it I am reminded of the 6th normal form, it's such a mess to gather all the parts of the condition into one big conjunction...