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/au-ts: Our main repository
• https://github.com/sel4: The repository of the seL4 Foundation, some of our projects migrate there after being adopted by the Foundation
• https://github.com/sel4proj: This is an unmaintained repo of seL4-related work that generally precedes the seL4 Foundation's creation.

Specific projects with their own repos

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/.

Pancake

The Pancake sources are on GitHub under the CakeML organisation.

Pancake Playground

Pancake Playground is a live environment where anyone can try the Pancake language.

Device specification

The current specifications developed by the Device formalisation project are on GitHub under our Trustworthy Systems organisation.

Former Projects

Unmaintained repos of some of our former projects.

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/au-ts/cogent/.

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.

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.

eChronos

eChronos is an RTOS for MMU-less microcontrollers.