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.

Joanna Rutkowska on Processor-Level Security

Tomshardware runs an interview with Joanna Rutkowska on malware targetet against the BIOS and even the processor firmware. The issue here is that the operating system can't defend itself against malware targetting lower layers of the system like the processor firmware. Here Joanna sees a task for the vendors of BIOSes and firmware.