Skip to main content


CakeML is an activity of Trustworthy Systems.


Reducing the cost and increasing the guarantees of verified software.


  • Verified compilation: we have developed the world-leading verified optimising compiler (and runtime system) for functional programming.
  • Proof-producing code generation: we have developed methods for automatically producing (verified) CakeML implementations of algorithms defined and verified in higher-order logic.

Further information

See the CakeML project website.


CakeML is a collaborative effort by researchers at multiple institutions. At Data61, we have:



  • A New Verified Compiler Backend for CakeML, ICFP'16
  • Functional Big-step Semantics, ESOP'16
  • A Verified Type System for CakeML, IFL'15
  • Pattern Matches in HOL: A New Representation and Improved Code Generation, ITP'15
  • CakeML: A Verified Implementation of ML, POPL'14
  • Proof-Producing Translation of Higher-Order Logic into Pure and Stateful ML, JFP'14
  • Proof-Producing Synthesis of ML from Higher-Order Logic, ICFP'12
Served by Apache on Linux on seL4.