There is a pervasive, cultural lack of formal verification in software, and it's risky, terrible, and should be stopped. Formal verification can takes multiple forms and operates at different spans across the layers of the stack. We need more of it to prove the correctness of compilers, libraries, and programs. It is a lot of work, but it's critical to proving things are as good, as say, seL4.

We need more Ada / SPARK!

there is a culture of type safety which is a very watered down machine checked proof that the thing entering a function has affordances X,Y and Z. Its not the end to end functional verification you are talking about but its not nothing either.

Yes, it opens a large attack surface for a group of people who thinks “memory-safe” is only possible when that word appears on the top of a language’s features list.