Well, if you wrote the kernel in a type-safe garbage-collected language (e.g. Java), then the static proof would be trivial since it is by construction impossible to violate the language invariants (assuming the VM and low-level support code is correct).
Unfortunately this small addition at the end makes the whole thing useless: simple interpreter mode for languages like Java are too slow and thus "VM and low-level support code" is typically comparable in complexity to OS kernel (in some sense it is an OS kernel).
The real reason is that apparently nobody cares enough to do the work.
No. The real reason is that it takes time and does not pay.
Comments and public postings are copyrighted by their creators.
Linux is a registered trademark of Linus Torvalds