sel4 day announcement

_news-items/2026-07-29-sel4-day.html

@@ -0,0 +1,33 @@
+---
+# Copyright 2025 seL4 Project a Series of LF Projects, LLC.
+# SPDX-License-Identifier: CC-BY-SA-4.0
+title: Happy seL4 day!
+anchor: sel4-day
+
+link: /
+img: /images/seL4.svg
+img_class: w-1/3
+alt: seL4 logo
+---
+
+<p>
+  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&apos;s
+  first formally verified kernel with a machine-checked code-level proof came
+  into existence.
+</p>
+<p>
+  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 <a href="{{ '/use.html' | relative_url }}">use</a>
+  it enjoys today.
+</p>
+<p class="mt-8">
+  A big thank-you to all for your continued support!
+</p>
+<p>
+  Learn more about the <a href="{{ '/About/history.html' | relative_url
+  }}">history</a> of seL4.
+</p>