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.
Pancake is a new low-level programming language designed specifically for the verification of device drivers and other low-level system programs. Pancake compiler reuses significant parts of the CakeML compiler backend, which is formally verified.
CakeML is a verified compiler for a high-level functional language, suitable for application-level software.
CakeML is a collaborative project by researchers at multiple institutions. Here at Trustworthy Systems, our work focuses on applying CakeML to systems programming, and verifying the behaviour of CakeML programs in the context of larger systems.
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.