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.