Homepage: https://sel4.systems/
Github: https://github.com/seL4/seL4
Related course (already posted on HN i think but can't find its associated thread): http://www.cse.unsw.edu.au/~cs9242/14/lectures/
Also, the link http://sel4.systems/FAQ/proof.pml is a 404 (linked within the article where it says "Last year, Heiser’s team proved mathematically that their kernel is unhackable."). I guess this is meant to link to http://sel4.systems/Info/FAQ/proof.pml (where the claims are far more measured).
"Integrity means that data cannot be changed without permission, and confidentiality means that data cannot be read without permission." seL4 claims both. I think "unhackable" is a good enough summary.
Also, saying a piece of software is "unhackable" is akin to saying a ship is "unsinkable".
Unfortunately, it's true that might not be enough to prevent attacks in some settings. For example, see Govindavajhala and Appel's "Using Memory Errors to Attack a Virtual Machine".
https://www.cs.princeton.edu/~appel/papers/memerr.pdf
In this case, they show that even given correct software safety guarantees, they can write a program which requires only one bit flip in any of a large number of RAM locations in order to achieve privilege escalation or violate the safety guarantees. They can then heat or irradiate the DRAM chips and make such a bit flip likely to occur. Since they can't control which bit will flip, it might sometimes crash the computer, but it's more likely to make their attack succeed.
So, one thing to study with systems like this is whether hardware fault injection can compromise the security guarantees in a way that would allow an attack to succeed.
The problem, if not specific attack, has been known a long time. The Tandem NonStop architecture assumed that its memory, I/O, and key components could fail. So, they designed system to work correctly regardless plus linear scaling of resources. My proposal was to integrate above technologies with older, non-patented version of NonStop for high security and availability.