I find my biggest problem is interfacing with apis from complex dependencies I can't control, usually OSes and gui libs. I assume there isn't a ton formal methods can do for that unless I set up a VM I can tightly control?
At that point you're probably blowing up your verification/validation space to where it might be intractable , in both a machine and human sense. People have done research work in formal methods all the way down to the assembly level, of course, but could you even write the correctness properties for the software you're describing?
Where you can use these methods - think of the part of your program's behavior you can describe with the article's "whiteboard" methods mentioned in the post above - truth tables, decision tables (! TIL), state machines/statecharts. If you can formulate it that way, not only is it easier to reason about and to test, but if you can also work out what would make it correct, you can run it through an automated checker.
