Hacker News Reader

Because they use formal methods preventing this kind of thing from happening?

Even with your formal methods strawman, vulnerabilities like these are still possible in Linux and C. We need to move on.

You can formally verify C code against a spec though.