3 ms·

seL4 despite being formally verified contained gnarly bugs, like [1]. Thus, it's not a silver bullet as some people think. Yes, it improves the quality, but onl

by xvilka 4mo ago

seL4 despite being formally verified contained gnarly bugs, like [1]. Thus, it's not a silver bullet as some people think. Yes, it improves the quality, but only one of the aspects of hardening software, like ASAN, SAST, fuzzing, strict languages, and so on. [1] https://github.com/seL4/seL4/issues/1199 https://github.com/seL4/seL4/issues/1199

gr_norm 4mo ago
> Since it is the unverified SMP config of the kernel I don't disagree with your point (formal verification does not rid you of all bugs), but this is not the subject of the linked issue. This was a bug in an unverified path.