Software

From time to time we release software as open source, or occasionally under a binary-only licence.

Github

You can find most of our software on github:

• http://github.com/sel4
• http://github.com/sel4proj
• http://github.com/echronos

Cogent

Cogent is a programming language with a certifying compiler for developing high-assurance systems components. The code can be found at https://github.com/NICTA/cogent.

CakeML

CakeML is an impure functional language with an end-to-end-verified optimizing compiler. The code can be found at https://code.cakeml.org.

C Parser

The ML-Tool and Isabelle/HOL code that translates a subset of C-99 into something that Isabelle/HOL can understand is available from here.

AutoCorres

AutoCorres is an Isabelle/HOL tool that automatically abstracts and simplifies programs that have been translated by the C parser.

Graph refine

Graph refine is a collection of tools and Isabelle/HOL theories used to reason about programs in a particular graph representation.

WCET tools

WCET Tools are a set of tools to compute the worst-case execution time for ARM binaries.

The seL4 kernel

seL4 is a proven correct microkernel available under an open source licence. It is hosted on github, but read the instructions at http://docs.sel4.systems/ before attempting to get it.

Channel Matrix Tools

A set of tools for generating and analysing large, sparse channel matrices.

Bitfield Generator

A DSL compiler for co-generation of bitfield code and associated correctness proofs.

CAmkES

CAmkES is a component platform for seL4.