It would way cheaper for them to verify their code than to probably follow these standards but bureaucracies are bureaucracies. Also, a little nitpicking in yo

It would way cheaper for them to verify their code than to probably follow these standards but bureaucracies are bureaucracies. Also, a little nitpicking in your write up but you should have also talked about type systems. They carry the spirit of formal methods but rather than being construct then check for correctness, are construction is correct by default. Type systems are widely accepted and show that some of these ideas can gain traction.