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

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.

I'm a researcher in formal verification; my thesis was building a tool to do this kind of stuff and I agree with the grandparent (though I would say probably closer to 5-10x slowdown not 100x).

Proofs are hard and often not for interesting reasons; its stuff like proving that you won't overflow a 2^64 counter which you only increment (aka something which won't happen for another couple billion years).

Current tools are only useful for specific kinds of problems in specific domains; things where a life really depends on correctness. Outside of those cases, lightweight techniques provide much more bang for your buck imo.

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.