All of my formal verification experience comes from using it in hardware, so the following comment may not apply so well to software where I have no experience

All of my formal verification experience comes from using it in hardware, so the following comment may not apply so well to software where I have no experience of formal methods (beyond learning about it at university). I think the mistake the author is making here is seeing formal verification as an all or nothing affair. Either you formally prove your program to be correct or it's useless. I would agree with them that doing this is a huge amount of effort and potentially just not feasible for real systems. However there's a huge amount of value in formal verification as an extra tool to assist you in your verification efforts. By combining traditional verification techniques (normal testing in software terms) with formal methods you have a whole new way to find bugs, one which works rather differently and hence tends to find different bugs. You may not get anywhere near confidence you've formally proved everything (for one I find the more interesting properties just never get proven, but leaving the tool to run for a while often throws up bugs that are tricky to find via other means) but it does accelerate your verification efforts. It's also a useful tool for exploring certain scenarios you as the designer (or programmer) may be worried about. You can overconstrain it to just look at certain behaviour and you can ask it to show you some specific execution that hits a particular property. Maybe there's some code path that's very hard to stimulate for whatever reason and you want to check out it's functionality. You can get the formal tool to hit it and then see what it does.