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/
