Writing formal specs, and proving your code meets that formal specs, is very hard, very slow work. Data61 proved that their microkernel implements a formal spec. It took them 25 person-years to implement a 7500 line kernel. Very very few software projects justify that level of expenditure.
I agree that system programming should be moving to languages/environments that make safer programming easier though. Why we're still writing non-performance critical code with buffer overflows in 2016 is beyond me.