Formally Evaluated Microkernel Sourcecode

Australian researchers have published a formal proof of the correctness of a L4 microkernel. They used the theorem prover Isabelle to achieve this. L4 is a microkernel, not an operating system. It performs only very elementary functions like memory management and controlling processes as well as interprocess communication.
Additional operating system functionality, like networking or file systems are implemented outside of the kernel.
If this works out, meaning that the proof holds and the kernel runs at a reasonable speed, this would mean thet this the world's fist bug-free operating system kernel source code. Note the defensive wording, there might still be errors in the specification, the services outside of the service or the C compiler.
Unfortunately, it wont't run on smart cards, as it's target architecture is ARM11 and x86. Also, to gain a formally proven secure smart card kernel one would have to prove also security against hardware glitches and attacks.