I don't think the connection between Haskell and Curry-Howard is that strong (it's stronger since GADTs were added, but still, functions are not even terminating). Rather, I think the main thing that makes Haskell "mathematical" and easy to reason about is that it is pure, so you can reason about things equationally.
That will help verification no matter what framework you are using. For example, look at the seL4 verification. That was done in Isabelle/HOL, so it doesn't use Curry-Howard in any way. But even so, they proceeded by writing two versions of the operating system, one in C, and one in Haskell to make it easier to reason about.
That will help verification no matter what framework you are using. For example, look at the seL4 verification. That was done in Isabelle/HOL, so it doesn't use Curry-Howard in any way. But even so, they proceeded by writing two versions of the operating system, one in C, and one in Haskell to make it easier to reason about.