オーストラリアの民間研究機関Information and Communications Technology Centre of Excellence（NICTA）の研究者らは現地時間8月12日、ミッションクリティカルなシステム向けの中核ソフトウェアが安全であることを検証する方法を発表した。 研究者らによると、この方法により、飛行機や自動車におけるシステムの安全性とセキュリティを管理するソフトウェアが、エラーを含む大型クラスを持たないことを数学的に検証できるという。 NICTAは、汎用OSカーネルに対する、マシンチェックによる初のフォーマル検証が完了したと発表した。このカーネルは、「Secure Embedded L4」（seL4）マイクロカーネルと呼ばれる。 ケンブリッジ大学のコンピュータ研究所で演算論理学の教授を務めるLawrence Paulson氏は、英国時間8月13日にZDNe
