"The L4.verified project demonstrates that such contracts and proofs can be done for real-world software. Software of limited size, but real and critical.
"We chose an operating system kernel to demonstrate this: seL4. It is a small, 3rd generation high-performance microkernel with about 8,700 lines of C code. Such microkernels are the critical core component of modern embedded systems architectures. They are the piece of software that has the most privileged access to hardware and regulates access to that hardware for the rest of the system. If you have a modern smart-phone, your phone might be running a microkernel quite similar to seL4: OKL4 from Open Kernel Labs."
"Yes, yes, it's verified. But does it run Linux?
"We're pleased to say that it does. Presently, we have a para-virtualized version of Linux running on top of the (unverified) x86 port of seL4. There are plans to port Linux to the verified ARM version of seL4 as well."
"There is now a way to mathematically prove that the software governing critical safety and security systems in aircraft and motor vehicles is free of a large class of errors - long before the plane takes off or the car’s engine starts."
