http://www.nicta.com.au/news/home_page_content_listing/world-first_research_breakthrough_promises_safety-critical_software_of_unprecedented_reliability
NICTA announced the completion of the worlds first formal machine-checked proof of a general-purpose operating system kernel, promising safety-critical software of unprecedented levels of reliability.
