This project is investigating the potential for language-based security techniques in the construction of low-level systems software. The specific focus is on the development of an open, capability-enhanced microkernel whose design is based on seL4, a "security enhanced" version of the L4 microkernel that was developed, by a team in Australia, as the first fully verified, general purpose operating system.