seL4 is the world’s first operating-system kernel with an end-to-end proof of implementation correctness and is an excellent base to build high-assurance systems. This site is for members of the seL4 community, including researchers, engineers, industry partners and open source contributors. Discussions involve but are not limited to verification, (what guaraantees do the various proofs provide and what are the limitations, other verification techniques), seL4 kernel design and implementation, leveraging seL4 to build high assurance systems and trustworthy systems architectures in general.
The first paragraph of this pinned topic will be visible as a welcome message to all new visitors on your homepage. It’s important!
Edit this into a brief description of your community:
- Who is it for?
- What can they find here?
- Why should they come here?
- Where can they read more (links, resources, etc)?
You may want to close this topic via the admin 
(at the upper right and bottom), so that replies don’t pile up on an announcement.