3 ms·
It's my recollection that seL4 was proven correct at the binary level.
by pavpanchekha 13y ago
It's my recollection that seL4 was proven correct at the binary level.
- pgeorgi 13y ago"We present our experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation." http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf Of course they might have improved on that later, this paper is ~5 years old now.