Not my experience (with Alloy and TLA+, some FM are very very hard and time intensive), it takes me a day to have a decently sized proof of some pretty complex difficult to test algorithms. The idea is not to use it for everything. But testing, thinking about and ensuring the validity of my solution with TLA+ is a lot faster than without TLA+. Not only that, but if any time in the future you need to add something to the system you can add that in half an hour and make sure all your important invariants hold without having to put yourself again in "paranoid mode" and having to remember everything about the system. Tests help, but some things are very very hard to test properly.

As everything it is a tradeoff, a lot of things do not deserve a proof, but for the ones that do you are a lot more productive.

It also depends on the level of the proof, I want to make sure the idea is valid and it takes some time to know what to abstract and what not to (it is a model after all). So if you are aware of what you are testing and at ehat level the tool and your proof is working it is very beneficial

My formal proofs for C or C++ take almost no time to write at all, because I'm using the right tools. Some asserts, some _CPROVE_assume hints, and mostly limitation of big for loops or recursions. If it works for 6, it also should work for 1000.

The visible "productivity" as in manager friendly LOC. The actual productivity goes up.

Managers don't want that though, for reasons that already Dijkstra has outlined.