Re: formal verification in general, most of the research has been moving towards making it easier to use and giving programmers some of the benefits of verification for free. I don't have any problem with the compiler telling me that my code is going to crash before the crash happens in production. That's unquestionably a valuable thing. Idris (and other languages) are trying to give you those sorts of benefits without reducing productivity or breaking your brain. It might not be there yet, but the progress is exciting.
Finally, both of the problems you identified (complex interactions and edge cases) are things that formal techniques are well suited to address... so I'm not sure how they support your case. Again, the only problem seems to be that the cost outweighs the benefits. But the cost is decreasing quickly.
To go beyond "protocols", UI form data to server response back to UI display in a web app is a source of major bugs. So many things are broken. Recently I had to add a spurious lap infant to book a flight due to JavaScript template being broken when rendering 0 children.
I'd love to QuickCheck the diapers out of this method.
The idea of a protocol in this sense encompasses pretty much any communication between things. This includes web service calls, user input via a UI, transactions between multiple systems, or even modules within the same program.
In fact, I question most of the value of formal verifications for non critical software. Most of the problematic bugs that make it through in my experience are either a complex combination of multuple parts of the system interacting together in a way that doesn't end up behaving the way it was intended, or programmers implementing the wrong thing on edge cases.