This also makes it easier to develop a uniform resource management strategy with allocator abstraction. Being able to easily switch between tuned bucket, pool, or bump allocation strategies can do wonders for optimization.
It's possible to model check that downcasting is done correctly, by adding support for performing type checks at analysis time. In this case, a type variable is added to the base type that can be compared before casting. Since this is an analysis only variable, it can be wrapped in a macro so that it is eliminated during normal compilation. Static assertions checked by the model checker during analysis time may need to be refactored to extract the type information as a proof obligation made by the caller. This technique actually works quite well using open source model checkers like CBMC.
Either way, some C OOP is not only useful to provide some optimization knobs, but it's also quite useful for introducing annotations that can help to formally verify C but that don't actually incur any runtime overhead.