Det finns ett operativsystem utan irriterande buggar, och det är matematiskt bevisat. Det handlar tyvärr inte om nästa version av Windows eller Mac OS X, utan om en mikrokärna för inbyggda system.
Operativsystemet heter SEL4, Secure Embedded L4. It-institutet Nicta i Australien har utfört det formella beviset, och avknoppningsbolaget OK Labs tänker nu försöka använda samma process med det kommersiella syskonsystemet OKL4.
