You might want to look at the Why3 meta-solver framework. It uses an intermediate language, Why3ML, that can be run against an array of different SMT solvers, i

You might want to look at the Why3 meta-solver framework. It uses an intermediate language, Why3ML, that can be run against an array of different SMT solvers, including Z3 and CVC4. If you run into something that SMT can't figure out in a reasonable time-frame, you can use Coq to manually-prove your theorems too. Languages like SPARK and Frama C generate Why3ML as an intermediate output that then gets transformed to run against whatever solvers are available during the verification phase of development. Since the verification/proof phase is separate from compilation, you can write your code with fewer checks initially, and then add conditions as you go to prove functional correctness. I'd be surprised if C++ is ever touted seriously as a language suited for formal verification. I think the language just has too many corners and escape hatches to be able to nail down its semantics in a way that automated provers can handle. Having said that though, I'm pretty sure the MSVC Driver Verifier tool uses an SMT solver to try and prove the absence of certain types of errors, so who knows?