3 ms·
You can't formally verify that your interface to the operating system works as it is supposed to work. You can only formally verify your own functions against
by maweki 3y ago
You can't formally verify that your interface to the operating system works as it is supposed to work.
You can only formally verify your own functions against some specification. And where do you get a bug-free specification from?
- arghwhat 3y agoFormally verified OS kernels exist: https://sel4.systems/Info/FAQ/proof.pml https://sel4.systems/Info/FAQ/proof.pml. There are caveats, but not "you cannot verify interfaces" or anything else that would somehow disqualify validation of network packet processing - something a mere unit-test could handle. The real counter to formal verification is that it is too much work and not a normal thing to do.