The problem is that the training required for "proof monkeys" is higher than for programmers, so they'll be even more expensive (plus you need to know the speci

The problem is that the training required for "proof monkeys" is higher than for programmers, so they'll be even more expensive (plus you need to know the specified C semantics to prove C code, something even many/most C programmers don't know), and second, the proving effort is not something that can usually be done separately and after-the-fact. The program needs to be written in a way informed by the proving effort. Moreover, every time the program is changed, the amount of proof that needs to be rewritten could be large, especially if the programmers are unfamiliar with the proofs. Hopefully, there are more efficient formal methods than the one that is currently the least efficient of them all.