VCC[1] was a substantial piece of research from MSR aimed at supporting the verification of C (not C++) via a theorem prover. However, it appears in a study[2] of its application to parts of the Hyper-V code-base, there were some practical difficulties relating to proving performance in the developer workflow.

Still, fascinating to see work like this on real-world code-bases with established languages. You can also see very similar work in languages like Dafny[3].

[1] https://github.com/microsoft/vcc [2] http://moskal.me/pdf/tphol2009.pdf [3] https://github.com/dafny-lang/dafny