[ahelwer]

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.