On 29th July 2009, the original functional correctness proof of seL4 was completed, a widely-recognised research breakthrough and the first big milestone in seL4's history. We obviously had a party then, and have since celebrated its anniversary, calling it, tongue-in-cheek, “International Proof Day”.
On the fifth anniversary we open-sourced seL4, which was another major milestone, which we referred to as “seL4 Freedom Day”.
Today marks the 12th anniversary of the proof, and the 7th anniversary of open-sourcing, and from now on we’ll refer to the date simply as "seL4 Day”.
The seL4 community is now definitely global. Still we would normally have a physical party in Sydney, but won’t be able to due to the renewed Covid-19 restrictions – so we’ll all be remote ;-)
Happy seL4 day everyone!
A virtual toast to you all, and a big thank-you to all for your continued support!
CEO of the seL4 Foundation
The seL4 Foundation is pleased to welcome Technical University of Munich as an associate member. The TUM, home of the Isabelle theorem prover used in the verification of seL4, has been a collaborator of the Trustworthy Systems team for many years.
The seL4 Foundation welcomes Second State as a member.
Second State is the creator and maintainer of WasmEdge, a CNCF / Linux Foundation project, which provides a high-performance, lightweight, cross-platform, polyglot, and secure software runtime/sandbox for edge computing. Based on the WebAssembly standard, WasmEdge could be 100 times faster than Docker and hypervisor-based solutions. It supports multiple programming languages, including DSLs, and can be embedded into multiple hosting environments.
Second State is currently porting WasmEdge to seL4. It will be on of the first software runtimes in the seL4 ecosystem. By working with members in the seL4 Foundation, Second State aims to create a real-time software sandbox for automotive and industrial (ie smart factories) applications.
With four new Premium Members joining the seL4 Foundation during the past few weeks, we now welcome their representatives on the seL4 Board. The new Board Members are:
Dr. Feng Zhou representing Horizon Robotics
Ian Xu representing Li Auto
Dr Matthew P. Grosvenor representing Jump Trading
Qiyan Wang represents NIO
More at https://sel4.systems/news.pml.html
For the complete seL4 Board see https://sel4.systems/Foundation/Board.html
Welcome aboard, Feng, Ian, Matt and Qiyan!