Why all the skepticism? Of course you can't prove that it works how people imagine it, but the spec can be a lot higher level than the program itself. You can

Why all the skepticism? Of course you can't prove that it works how people imagine it, but the spec can be a lot higher level than the program itself. You can already prove a lot of things about a large class of programs, depending on the language and tools, like the absence of buffer overruns, etc. This project has a spec written in Haskell and then a proven 1:1 mapping at a certain level of detail between that spec and the kernel itself. You can prove an awful lot of things that way that do make a kernel like this more trustworthy and stable.