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.
On July 29, 2014, "seL4 day" became a double-celebratory day: the seL4 code and proofs became open source, paving the way to the widespread use [0] it enjoys today. A big thank-you to all for your continued support! Learn more about the history [1] of seL4. [0] https://sel4.systems/use.html [1] https://sel4.systems/About/history.html -- Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 [email protected] [email protected] _______________________________________________ Announce mailing list -- [email protected] To unsubscribe send an email to [email protected]
