On July 29, 2009, the last “sorry” of the seL4 functional correctness proof was eliminated. A “sorry” is an assumed theorem lacking a complete proof. “0 sorries” meant there was nothing left to prove: the project was finished. We now celebrate this day every year to mark the seL4 day, when the world’s first formally verified kernel with a machine-checked code-level proof came into existence.
In July 2014, on the 29th to make the “seL4 day” a double-celebratory day, the seL4 code and proofs became open source, paving the way to the widespread use it enjoys today.
A big thank-you to all for your continued support!
Learn more about the history of seL4.
