I think the pain only appears when you start trying to do "deep specification" of large systems. My research group has about 5-10 of us that have all built large systems (5-60 kloc) and verified them in Coq. I know each of us long list of gripes with the tooling.
My recent work has been on a verified JIT compiler and having to write tactics and lemmas to deal with facts about bit vectors seems stupid when SMT solvers are particularly good at this kind of reasoning.
When you say that you verified a large system in Coq, in what language did you write your system? does it mean that your language semantics has do be defined in Coq, or did you write your system using Coq as a programming language?
I'm with you that, depending on the problem, different verification approaches make the most sense. I wish it was easier to combine results from different tooling.
My recent work has been on a verified JIT compiler and having to write tactics and lemmas to deal with facts about bit vectors seems stupid when SMT solvers are particularly good at this kind of reasoning.