Já que pelo que eu vi o pessoal comentou sem nem ler a reportagem, aqui vai um trecho importante:
"O usuário de computadores tradicionais deverá esperar um pouco antes de poder usufruir do acréscimo de segurança e confiabilidade oferecido por um sistema operacional livre de erros.
O kernel 100% correto pertence a um sistema operacional do tipo embarcado (embedded system), que roda em computadores dedicados a tarefas específicas - seu nome é Secure Embedded L4 (seL4).
A nova técnica de verificação, contudo, poderá ser utilizada no desenvolvimento de qualquer outro programa, seja um sistema operacional ou outro aplicativo qualquer."
O que eles desenvolveram, na verdade, foi uma técnica de verificação, que permitiu a eles criarem um SO 100% sem falhas. Se esse SO em si é aberto ou fechado ou não, não importa, até porque ele é para dispositivos embarcados. Na própria matéria eles dizem que isso ai vai servir pra coisas de alta precisão, como robótica, sistemas de controle de aviões, etc...
O que é interessante é que essa técnica de verificação vai poder ser usada para desenvolver programas e SOs sem erros. Mas não vai ser uma mágica. Na própria matéria eles dizem que essa técnica que eles desenvolveram permitiu a eles criarem e provarem matematicamente que o kernel não possui falhas. Isso ocupou uma equipe de 6 pessoas durante 6 anos. E eu acho que eles devem ter feito um kernel não muito grande (tem um gráfico com as funções do kernel que eles desenvolveram, e garanto que o Linux ou o kernel do Windows devem ter umas 10 vezes mais do que isso).
Agora, se eles liberarem essa técnica de verificação (não sei como funcionam as patentes para essas coisas, mas acho que eles vão liberar, já que é um trabalho científico desenvolvido numa universidade), vamos poder usá-la no Linux. Já pensaram quanta gente e quanto tempo será necessário pra isso?