3 ms·
Formally 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 ver
by arghwhat 3y ago
Formally 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.