Just a few days ago I became aware of CertiKOS, which is apparently a formally verified kernel [0] [1]. I think these two aspects--formal verifiability and bein

Just a few days ago I became aware of CertiKOS, which is apparently a formally verified kernel [0] [1]. I think these two aspects--formal verifiability and being open source--are key for a truly secure OS of the future. [0] http://news.yale.edu/2016/11/14/certikos-breakthrough-toward-hacker-resistant-operating-systems http://news.yale.edu/2016/11/14/certikos-breakthrough-toward... [1] https://www.usenix.org/conference/osdi16/technical-sessions/presentation/gu https://www.usenix.org/conference/osdi16/technical-sessions/...