FWIW sel4 could have verified the C, they simply decided to verify the machine code so that they didn't have to trust that the compiler correctly complex the ve

FWIW sel4 could have verified the C, they simply decided to verify the machine code so that they didn't have to trust that the compiler correctly complex the verified software. The issue with more broad formal method use is that it's quite a bit of work. The code to be verified has to be designed on the onset for verification, which limits design choices in interesting ways, and even then the verification code far outweighs the code being verified, at about 25:1.