Comment by Panzerschrek

> We claim that C achieves real-time program verification, i.e., the user can carry out verification as they program the implementation code incrementally. It achieves this goal by orchestrating the symbolic-execution engine and the LCF-style proof kernel together, creating a proof-supporting runtime that runs proof-code blocks and symbolic execution of program segments in an interleaving manner

That's why such thing is mostly useless. C is used in places where performance is important and nobody want to sacrifice performance for such proofing. Even more, if such proofing is too slow, it's better to use something like Fil-C.