Proof Carrying LLVM?
This is a project I've been thinking of venturing into for a few years now, and I was fortunate to have a very useful discussion about it at the time I started planning it with Chris Lattner (at the time, one of the main architects of LLVM, although better known these days perhaps for his work on Swift).

It does seem that there is a possibility of producing correctness proofs for a subset of C (or potentially C++) using LLVM.  There has already been some work done which would be useful:


As discussed in comments, memory safety is critical.  Without memory safety, type safety is essentially irrelevant.  A number of memory-safety related analyses and transformations have already been implemented for LLVM that could help.  These include:
"fat pointers", i.e. transformation of C style pointers into pointers into areas of defined size, in order to catch bound errors
a transformation applied to dynamic memory allocation that enables detection of use of pointers after they have been freed.  These two features are described in this paper.


For the subset of C programs that perform no type casts, applying these transformations may be adequate.  Of course, real C and/or C++ code often uses typecasts, and adding this facility is more challenging.  For performance sake, as many of these cases as possible must be caught at verification time rather than runtime, although in the end of the day the use of runtime type information and a dynamic casting implementation would be enough to allow for entirely safe C code.