I think there's exceptions to this: most modern attempts to verify software has involved design decisions that are only practical when you're starting from scra

I think there's exceptions to this: most modern attempts to verify software has involved design decisions that are only practical when you're starting from scratch. Similarly, rewriting in a language with more static safety guarantees may lead to fewer bugs (or at least different, less critical ones).