Comment Comment by dead10ck "In short, the implementation is proved to be bug-free."This reeks of bull shit."We still assume correctness of hand- written assembly code, boot code, management of caches, and the hardware"Sorry, I don't think you can claim you have a mathematical proof of the correctness of your kernel when you assume this much.And where is this proof? I can't seem to find it anywhere on their web site. The only thing I can find is the publication"seL4: Formal Verification of an Operating-System Kernel" http://ertos.nicta.com.au/research/l4.verified/pubs.pmlwhich looks like it just talks about the proof, rather than providing it. Am I just blind?This looks interesting, but the confidence which they espouse is very suspicious. parent dead10ck 12 years ago
This reeks of bull shit.
"We still assume correctness of hand- written assembly code, boot code, management of caches, and the hardware"
Sorry, I don't think you can claim you have a mathematical proof of the correctness of your kernel when you assume this much.
And where is this proof? I can't seem to find it anywhere on their web site. The only thing I can find is the publication
"seL4: Formal Verification of an Operating-System Kernel" http://ertos.nicta.com.au/research/l4.verified/pubs.pml
which looks like it just talks about the proof, rather than providing it. Am I just blind?
This looks interesting, but the confidence which they espouse is very suspicious.