4 ms·
The correctness proof of the seL4 microkernel supposedly makes no assumptions of the compiler and verifies the binary output. I don't know the details.
by WallWextra 10y ago
The correctness proof of the seL4 microkernel supposedly makes no assumptions of the compiler and verifies the binary output. I don't know the details.