Can someone explain to me what it means for a kernel to have an end-to-end proof of implementation? Does it just mean that the kernel is implemented bug-free? That it will never panic?
It's actually a very impressive piece of work, I can't wait to read about the details of how it was done.