Type systems and proofs have their limitations, if just because for a proof to be worth anything, I need a perfect description of what I want, and that doesn't make any sense outside of trivial cases.
I once worked with a relatively well known, prove everything developer that you might know by name. He's written books and everything. He built an algorithm to make a distributed system of equal peers figure out when it needed to start more nodes, or could shut some of them down. He wrote a proof, in code. He wrote a paper. When in production, the system would not work as advertised, and he blamed it on other pieces, because the algorithm was proven correct! So the problem stayed there for months.
After he left the company, I decided to figure the problem out, so I read through the proofs, the paper, and the code: All the single letter variables you could possibly want. I figured out that yes, the algorithm was flawless, as long as every operation in the system was atomic and instantaneous. Instead of the proof, I built a small simulator that didn't have such flawed assumptions, and got the exact same behavior as the production system. So the proof was perfect, as long as we made assumptions that are impossible in our universe. And the entire algorithm was less than 200 lines of code.
So whenever we have a reality that is difficult to model (and let me tell you, distributed systems fit the bill), dependent types will not save you, haskell or no haskell. Proofs will always be limited by your assumptions.
So while the tools you mention are nice. They hit the same limits as everything else we build. Whether to write a proof in idris, use generative testing, or just some example testing, is really all a tradeoff, but you will never escape from bad specification, as all specifications are bad.