[ausimian]

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

[mmoskal]

There are also efforts at ETH to verify Rust using SMT solvers using methods similar to VCC and Dafny, see https://www.pm.inf.ethz.ch/research/prusti.html

Adding verification once you have code is generally more difficult, though in case of VCC it was helpful to have a large example code base to make sure the tool would cover the major patterns, especially relating to concurrency primitives.