CakeML: A Verified Implementation of ML

About

CakeML is a functional programming language with a proven-correct compiler and runtime system.

CakeML is based on a substantial subset of Standard ML. Its semantics is specified in higher-order logic. The compiler algorithm, also specified in higher-order logic, has been proven to transform CakeML programs to semantically equivalent machine code. The compiler implementation is a CakeML program that has been verified by a bootstrap method that executes the compiler specification on the compiler implementation to create a proven-correct compiler binary. The correctness proofs use validated ISA models for machine code. A verified binary of the CakeML read-eval-print loop is available for x86-64; binaries for ARM, MIPS, and RISC-V are anticipated.

A long-term goal is to make proof assistants into trustworthy and practical program development and implementation platforms. The CakeML compiler verification is an example of proof-assistant-based development; specifically, of proven-correct synthesis of machine code from higher-order logic specifications. The verified compiler is both a standalone tool and a component in the logic-to-binary synthesis toolchain.

CakeML is free software. So far it is the result of about ten person years of work by an international team of six core developers spread across three continents. The beta version of CakeML is undergoing evaluation by a US-based industrial collaborator. More project participants and evaluators are sought.

This website provides further details of the CakeML project, links to papers, courseware, auxiliary tools and suggestions for masters and doctoral level projects.

News

  • Our ESOP'16 paper (preprint) describes and advocates the use of functional big-step semantics for both reasoning about programming languages and compiler verification.

  • CakeML together with our formalisation of HOL in HOL is being used in research supported by the Future of Life Institute on AI safety, in particular on improving our understanding of reflective reasoning. Our ITP'15 paper on reflection precedes and supports the work on this project.

  • A new representation for pattern matching in HOL, as described in this ITP'15 paper on pattern matching, has been incorporated into the HOL-to-CakeML translator.

  • We gave a guest lecture in the Advanced Topics in Software Verification course at UNSW, about bootstrapping the verified CakeML compiler. (See the slides for Week 12, 2015.)

  • The beta (see item below) now also supports character literals.

  • A beta version of the verified CakeML implementation (version 1) is available here. To build and run the code: unzip, then make, and ./cake.

    Note that this is a beta version with a few known issues: (1) stack overflow is checked by the OS, leads to a segfault; (2) compiling on Mac OS produces some compiler warnings. If you stumble upon other issues, let us know on users@cakeml.org.

    This is verified software. Why might it have issues? The short answer is that we might not have checked our assumptions thoroughly enough. Is our model of the x86-64 machine accurate enough? Are we interacting with the unverified C code correctly? The assumptions have been tested, but one can never be 100% sure that testing caught all possible issues.

  • A preliminary version of the CakeML Compiler Explorer is available. This web service lets you run the verified compiler and see the results of various stages of compilation.

  • Our ITP'14 paper describes work on formalising the semantics and soundness of higher-order logic, including support for its principles of definition, and producing a verified implementation of the kernel of a theorem prover in CakeML. The paper describes a method for supporting definitions via translation into Stateless HOL.

    We have since developed a direct semantics for all of HOL (supporting both definitions and non-definitional context extensions including new axioms). This version was presented in our ITP'14 talk. It is described in more detail in our subsequent JAR paper.

  • We gave an MPhil course at Cambridge on specifying, implementing, and verifying functional programming languages.

  • Our POPL'14 paper describes CakeML and a verified x86-64 implementation of a read-eval-print loop for CakeML, using the bootstrapped compiler below, a verified translation from bytecode to x86-64, and a mostly-synthesised verified runtime.

  • We have written, verified, and bootstrapped a compiler (including lexing, parsing, type inference, and code generation) from CakeML to CakeML Bytecode. The correctness theorem covers both terminating and diverging programs, and says that the generated code behaves according to the semantics in either case. The compiler is written in HOL; we use the translator, mentioned below, to generate a verified CakeML implementation, and then evaluate the compiler on this implementation (bootstrap) to generate verified bytecode.

  • One of our initial target case studies is to construct a verified CakeML version of the HOL Light theorem prover. For this case study, we extended the translation tool, mentioned below, to be able to translate into stateful CakeML code. Initial results are described in our ITP'13 short paper.

  • We have developed a tool which translates functions from higher-order logic into CakeML. This tool is proof producing: for each translation it proves a theorem which states that the generated CakeML code correctly implements the original HOL function, according to the operational semantics of CakeML. See our ICFP'12 paper, and subsequent JFP paper, for more details.

People

Current developers:
Contributors:
  • Rob Arthan,
  • Gregorio Curello,
  • Trần Tiến Dũng (logo design),
  • Mike Gordon,
  • John Harrison,
  • Stephen Kell,
  • Christopher Pulte,
  • Konrad Slind,
  • Freek Wiedijk,
  • James Wood.

Acknowledgements

Code

The code for this project is hosted on GitHub.

Mailing list

For help and announcements, join CakeML Users.

Chat

Join the #cakeml IRC channel on freenode (webchat).

Projects

We maintain a list of project ideas for students, interns, and other contributors.