Respectfully, that's a rather extraordinary claim. There are model checkers that use separate specification languages, but there are also model checkers embedde

Respectfully, that's a rather extraordinary claim. There are model checkers that use separate specification languages, but there are also model checkers embedded in the host language. CBMC translates C -- the same language -- to an SMT solver. A different target but the same language. It is true that new idioms will often be discovered along the way of converting existing C to pass the bounded model checker in every branch condition and in every case. However, software that is already relatively safe will require very little modification. I've seen it go both ways. Simpler code bases can pass model checks relatively unscathed. More complex code bases require refactoring to pass model checking. To my point, the code base can remain in C, and can be model checked gradually. It doesn't have to be ported to a different language or platform. But, it will require added assertions and some refactoring to make the execution of code more clear. It's still in C. The specifications are specified in C using regular assertions. The only thing that changes is that one will often use shadow methods -- still written in C but simpler than the functions they are shadowing -- in order to model check other functions. Other bounded model checkers like JBMC, Kani, or PolySpace work in similar ways.