> Do you have a good paper about the full stack formalization/verification of a nuclear launch system?

Bwahahaha you're funny.

> If you try to formalize everything, you'll drown. If you strategically concede defeat and admit that some parts of the system aren't possible to formalize, you can get a lot of strong guarantees.

You're contradicting yourself again. There's a reason why weakness is a strength in formalisms.