The key is to structure the program so that only a tiny trusted core is verified but the properties extend to untrusted code. For example, the sel4 microkernel is formally proven to not crash (barring hardware), so any program running on it will not crash the entire computer, just itself. Or (only parts of it are formally verified, but) the Rust borrow checker practically guarantees any Rust code without `unsafe` will not produce memory errors; any amount of lines of Rust code, without any proofs themselves, are covered by the relatively tiny trusted core that is the borrow checker.