This link to the GitHub repository doesn't give a lot of the context about why this is exciting.
As others have mentioned, seL4 is "The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement." But for many years it was proprietary, and only available under commercial terms. The paper was published in 2009, so it's been five years that it was proprietary.
As of today at noon, the kernel was released under GPLv2 and userland under two-clause BSD. That is exciting.
As others have mentioned, seL4 is "The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement." But for many years it was proprietary, and only available under commercial terms. The paper was published in 2009, so it's been five years that it was proprietary.
As of today at noon, the kernel was released under GPLv2 and userland under two-clause BSD. That is exciting.