|
|
|
|
|
|
by arghwhat
1005 days ago
|
|
|
Formally verified OS kernels exist: 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. |
|
|