Programming languages
The design, specification and implementation of programming languages is essential for building trustworthy systems. Programs expressed in well-designed languages are easier to specify, verify, optimise, and maintain.
Cogent
Cogent combines the ease of verification of functional languages with innovative facilities for low-level systems programming.
CakeML
CakeML is a landmark implementation of a fully verified compiler for a high-level functional language.
MicroVM
The Micro Virtual Machine project aims to simplify language implementations, by providing a virtual machine layer that is efficient, reusable and amenable to formal verification.
L4.verified C semantics
We have developed a detailed formalisation of a large subset of the C language. This is implemented in our C parser and is used for our verification of seL4.