seL4 基金會在當地時間2024年4月29日正式披露蘋果公司（Apple Inc）加入 seL4 基金會，成為其普通會員，具有投票權，但不具有董事席位。seL4 基金會對此表示歡迎，並期待未來蘋果公司在形式驗證與 seL4 上的工作。
seL4 基金會成立於2020年，基金會創始成員包括 Cog Systems、DornerWorks、Ghost Locomotion、HENSOLD Cyber 與 UNSW Sydney，是 Linux 基金會 (LF) 下的一個項目，並遵循 LF 的既定結構。
seL4 在 2004 年開始開發，2009 年完成形式化驗證，2014 年開源，目前主要貢獻者和發起人是 Gernot Heiser。澳大利亞聯邦科學與工業研究組織 CSIRO/ Data61實現了對於其L4 內核的形式化證明，並創造出世界上第一個此類的實用操作系統內核 seL4。他們在2013年進一步證明了內核的信息流安全性，使得該系統成為最安全的操作系統內核之一。
seL4 是世界上第一個通過形式驗證，用數學方法被證明其安全 bug-free 的操作系統內核，並且在安全的基礎上擁有高性能。它對於計算系統的內核安全的可信賴度具會有極大意義，具體來看可能影響到航空航天電子、自動駕駛汽車、太空宇宙開發、醫療設備、關鍵基礎設施、國防等行業。理論上，SeL4 可以用作 Linux 和其它類 Unix 操作系統的底層基礎，甚至曾被考慮用於 GNU 計劃的內核項目 GNU Hurd。此前 Linus Tolvalds 在接受 LinuxStory 採訪時明確表示「形式驗證」會用於 Linux 內核的開發。
更多信息歡迎訪問 https://sel4.systems/
