Trustworthy Systems

The eChronos project @ TS and Breakaway



In collaboration with Breakaway Consulting, the eChronos project builds and formally verifies, a small, versatile, high-assurance real-time operating system (OS) for embedded micro-controllers. In contrast to other OS work at TS, the eChronos RTOS is for tightly constrained devices without memory management units. Current implementations are available for ARM Cortex M3/M4/M7, PowerPC e500 and Intel 80251 micro-controllers. The RTOS also runs on POSIX platforms (e.g., Linux, MacOS-X, Windows with cygwin or MinGW) for rapid prototyping.


The eChronos RTOS is open source, available github. For separate commercial licenses, please contact us (see below).


On modern powerful embedded hardware, like in smartphones, OS kernels such as TS's formally verified seL4 kernel can provide isolation and gatekeeper functionality — controlling what the user-level programs can do with the hardware, or with other programs. For instance, it could stop a malicious app from crashing your smartphone.

On less powerful hardware — such as small medical implant devices, extremely resource-constrained spacecraft, or simple logic controllers used in industrial plants — such gatekeeper functionality is not possible. Instead, these systems run small, so-called real-time operating systems (RTOS) such as the eChronos RTOS. The constrained nature of the hardware devices the RTOS runs on makes it even more challenging to provide assurance and evidence that it works reliably.

The eChronos RTOS is also used on the flight-control processor of the DARPA-funded SMACCM project's research vehicle.



Technical Overview


The eChronos RTOS is open source, available on github.

The eChronos RTOS is also available for commercial deployment. For separate commercial licenses, please contact us (see below) for further information.




Abstract PDF Darren Cofer, John Backes, Andrew Gacek, Daniel DaCosta, Michael Whalen, Ihor Kuz, Gerwin Klein, Gernot Heiser, Lee Pike, Adam Foltzer, Michael Podhradsky, Douglas Stuart, Jason Graham and Brett Wilson
Secure mathematically-assured composition of control models
Technical Report, Data61, CSIRO, September, 2017
Abstract PDF June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan and Christine Rizkallah
Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
International Conference on Interactive Theorem Proving, pp. 52–68, Nancy, France, August, 2016
PDF June Andronick, Corey Lewis and Carroll Morgan
Controlled Owicki-Gries concurrency: reasoning about the preemptible eChronos embedded operating system
Workshop on Models for Formal Analysis of Real Systems (MARS 2015), pp. 10–24, Suva, Fiji, November, 2015