> First, you do realize that there already has been an OS that has been formally verified, right? It's called seL4. There is also a C compiler that has been formally verified. It's called CompCert. So there is a clear path to get there on the software side.
CompCert has not actually been formally verified - only the middle-end has. The C preprocessor and assembler aren't, the frontend formerly wasn't (but I think is now), and bugs have been found in those parts by fuzzing.
Plus being a faithful implementation of the C spec certainly leaves room for security issues…
(Why do we say "formally verified"? It sounds like weasel words. What is formal about it?)
Regarding "formally verified," I believe the "formal" refers to the formal in formal methods, but I agree that it can be weaselly.
In the case of seL4, however, I don't think it is because they are incredibly precise about defining their assumptions. They have verified the machine code for various architectures, subject to those assumptions.
CompCert has not actually been formally verified - only the middle-end has. The C preprocessor and assembler aren't, the frontend formerly wasn't (but I think is now), and bugs have been found in those parts by fuzzing.
Plus being a faithful implementation of the C spec certainly leaves room for security issues…
(Why do we say "formally verified"? It sounds like weasel words. What is formal about it?)