Skip to main content

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 combines the ease of verification of functional languages with innovative facilities for low-level systems programming.


CakeML is a landmark implementation of a fully verified compiler for a high-level functional language.


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.