Things I never want to hear about flight control systems before I board a plane: “if things compile there's a high chance it's correct”
Compiling does not differentiate between True and False, so no safety for that escape pod door.
But I definitely want as much as possible to be automated and formally correct, which is why I wrote what I wrote.
We're not quite there yet, but while regular programming is quite tough for AI due to how fuzzy it is, formal proofs are something AI is already very good at.