But when it's trivial to try QUADRILLION fuzzing operations (sixteen four gigahertz cores do this many operations every 4.1 hours) do you really need formal correctness? Can't you brute-force correctness, by literally trying each and every possible input and output, and literally trying every possible state?

We have so much power it's obscene. We're producing SHA-1 collisions without damaging or analyzing the algorithm, just using brute force. Why not take that approach to kernel security?

I'd sooner trust code whose quintillion input and output states have been exhaustively brute-forced over a few months (so that literally every possible path and value that code can take has ACTUALLY been run), than code which has been formally proven to be correct but without having been subject to such a test.