# CakeML: a Standard ML implementation whose correctness is proved in HOL4

> CakeML is a verified implementation of a significant subset of Standard ML, developed as source and proofs inside the HOL4 theorem prover. What is verified is unusually broad, covering lexing, PEG parsing, type inference, compilation to assembly and code generation down to x86 and ARM, but the cost is a build that the project itself describes as requiring significant resources.

**CakeML/cakeml** — CakeML: A Verified Implementation of ML

- Repository: https://github.com/CakeML/cakeml
- Website: https://cakeml.org
- Stars: 1,216 · Forks: 108
- Language: Standard ML
- License: BSD-3-Clause
- Published: 2026-10-19 · Updated: 2026-10-19 · Language: en
- Canonical page: https://hysenlabs.com/projects/cakeml-cakeml

## What a verified implementation actually claims

CakeML is described as a verified implementation of a significant subset of Standard ML. That phrasing is doing precise work, and the qualification matters in two directions. The implementation is verified, meaning there is a machine-checked proof of its behaviour, and the language is a subset, meaning it is not all of Standard ML.

The mechanism is unusual. The source and proofs for CakeML are developed in the HOL4 theorem prover, using the latest master version of HOL4 built on Poly/ML 5.7.1. So the compiler is not written in CakeML and then tested. It is written in a HOL-defined language, the correctness proofs are written in HOL, and the HOL kernel checks the proofs. The result is an artifact whose correctness follows from a kernel check rather than from a test suite.

The project describes the outcome as a significant subset of Standard ML, which puts it in a lineage with the other foundational implementations of the language. The language it implements is defined in the repository, not taken on faith, and the semantics directory holds the definition of the CakeML language including the concrete syntax, the abstract syntax, big step semantics in both a functional and a relational form, a small step semantics, the semantics of FFI calls, and the type system.

That directory listing is the honest summary of what verification means here. It is not a claim that a few properties hold. It is a formal model of the language at two levels, a small step and a big step, plus a formal account of foreign function interface calls and of the type system. Verification of a compiler against that model is a different, and much stronger, statement than a passing test suite.

The practical audience is narrow and clear. This is for people who want machine-checked claims about a compiler, not people who want an SML implementation to write an application in. The tutorial directory reinforces that, holding an extended worked example on using HOL and CakeML to write verified programs that was presented at PLDI and ICFP in 2017.

## The build needs Poly/ML, HOL4 and a machine you are not looking forward to

There is no pip install here, and there could not be. The README states that building all of CakeML, including the bootstrapped compiler and its proofs, requires significant resources, and points to built copies of the compiler and resource usage for the regression tests as being available online.

That is an important practical point. The prebuilt artifact is available for download from cakeml.org, so using CakeML as a language does not require you to run the verification. Verifying it yourself, or extending the proofs, does.

The build procedure is described in a script in the repository. build-instructions.sh is described as the file that describes how to install Poly/ML, HOL and CakeML, and the README links to it for example build instructions. The directory listing at the top level confirms the layout: a Holmakefile at the root, holproject.toml for the HOL project definition, and the script itself alongside the source directories.

The project uses the latest master version of HOL4 rather than a pinned release, which is worth flagging for reproducibility. Building on a moving upstream means your proof development tracks HOL4 master, and a HOL4 change can affect your build without any change on the CakeML side.

For a contributor, the practical sequence is to read build-instructions.sh, set up Poly/ML 5.7.1, build HOL4, and then work through the Holmakefile targets in the individual subdirectories. The developers directory holds scripts for automating routine tasks, such as generating README.md files, and the misc directory holds the glue between a standard HOL installation and what CakeML development needs, which tells you that CakeML expects to sit inside a HOL project rather than beside one.

The regression tests are run through cakeml.org/regression.cgi according to the README, so the test results are reported on the project site rather than only in the repository.

## compiler/ holds the whole pipeline, from lexing to ARM code generation

The compiler directory is where the verification effort concentrates, and the README describes it as a verified compiler for CakeML including lexing and PEG parsing, type inference, compilation to ASM assembly language, and code generation to x86, ARM, and more.

Read that list as a pipeline and the scope becomes clear. A front end that lexes and parses with a PEG parser, a type inference stage, a middle end that targets an abstract ASM assembly language, and a back end that generates native code for x86 and ARM. Verification of this much means proofs about the front end, about the type system, and about the correspondence between the abstract assembly and the concrete machine code.

The PEG parser detail is significant, because PEGs are not context free in the usual sense. They are unambiguous, which makes parsing behaviour easier to reason about in a proof than it is for a general context free grammar with ambiguity resolved by precedence rules, but the language of the grammar itself is more constrained. If you are porting a CakeML program from SML, a source construct that relies on ambiguous grammar may not have a direct translation.

The ASM intermediate is what makes the back end tractable. Verifying a compiler that goes from source directly to machine code is a much larger proof effort than verifying source to an abstract assembly language, and the abstract assembly is also where the FFI boundary can be placed. The semantics directory includes the semantics of FFI calls, so the boundary between verified and unverified code is a formal object in this development rather than a comment in a source file.

Two other directories in the same family are worth naming. The translator is a proof-producing translator from HOL functions to CakeML, and the cv_translator is a translator to the cv type used by cv_compute. Both are about moving between worlds: HOL's own function representation and CakeML's, and between the ordinary and the cv representations used by the verification machinery.

The candle directory holds something different again, a verification of a HOL theorem prover based on HOL Light, implemented in CakeML. That is a second-order effort: not only the compiler but a theorem prover implemented in CakeML.

## The basis library is only the beginnings of one

The basis directory is described as containing the beginnings of a standard basis library for CakeML, similar to the standard basis library of SML. The wording is precise and it is the honest position. This is a start, not a completion.

This is the practical constraint on using CakeML as a language today. The verification covers the compiler and the language semantics, but the library you would reach for in ordinary SML work is a work in progress. If a program needs string handling, file IO, or the collections modules, you are likely to hit the edge of what exists, and the README's phrasing is the only signal you get about where that edge is.

There is an unverified directory for the parts that are not yet inside the trusted base. It holds various unverified tools, for example tools for converting OCaml to CakeML and an SML version of the CakeML register allocator. The register allocator is the notable entry. A verified compiler to assembly language does not by itself give you a verified code generator down to the register level, and the SML register allocator in this directory is the unverified component that fills the gap in the pipeline described in the compiler directory.

That distinction is exactly what a project like this is usually trying to shrink, and the fact that it is visible in the directory layout is a good sign about how the project reports its own state. The same applies to the pancake compiler, a C-like compiler built from the lower parts of the CakeML compiler. Reusing the verified lower levels for a C-like language is a way of getting more value out of the same proof investment, and the existence of that experiment tells you the CakeML compiler is not a closed, single purpose artifact.

The characteristic directory holds a verified CakeML adaptation of Arthur Charguéraud's work on characteristic formulae for the verification of imperative programs, which is about how you reason about state in a verified program, and the tutorial directory contains the extended PLDI and ICFP 2017 worked example for people who want to see the whole process end to end.

## how-to.md is the document a new user should read first

For anyone who actually wants to write CakeML rather than study its proofs, the README points to a document that does the explaining. how-to.md introduces how to use the CakeML compiler and provides, in particular, a description of how to invoke the CakeML compiler, a list of how CakeML differs from SML and OCaml, and a number of small CakeML code examples.

The differences list is the part to read with care, and it is a reminder of what the subset qualifier in the project description means in practice. A CakeML program is not SML source that compiles, it is a language close to SML with a documented set of departures, and the departures are exactly where your port will break.

The examples directory shows what verified programs look like in practice, and the file names are a good index to the scope. There are scripts for a hello program, a hello error program, a cat program, a diff program, a div program, a double argument program, an echo program, a filter program, an insert sort program, a longest common subsequence script, a lisp program, an md5 program and a grep program, plus an array search program. Each of these is packaged with a Holmakefile, and the subdirectories, cnf/, compilation/, deflate/, flover/, lpr_checker/, opentheory/ and pseudo_bool/, indicate that the collection is not only toy programs but also real pieces of work.

The deflate and md5 entries in particular are the kind of thing that distinguishes a demonstration from a serious effort. A verified implementation of a compression format or a hash function has to deal with byte-level semantics, which is exactly where naive formalisation of a language tends to fall apart.

For a language with a thin standard basis, the practical workflow is to start from one of these examples rather than from an empty file, because the examples show which library functions exist and which need proving.

## Branches, releases and what a version tag means here

The versioning scheme is unusual enough to explain. The recent release tags are v3479 on 2026-08-26, v3400 on 2026-06-19 and v3304 on 2026-04-25, with tag names of the form CakeML v3479. These are not semantic version numbers, they are build identifiers that increase with each development snapshot.

The branch structure is described in the README. The master branch contains the latest development version of CakeML, and there are separate version2 and version1 branches for previous versions. A project with numbered version branches alongside an ever-advancing master suggests a distinction between a stable reference point and the moving edge, and the practical consequence is that you choose a branch rather than a version number to pin your work to.

The repository is not archived and the last push was on 2026-10-15, so the development branch is being worked on actively. The three listed release tags carry dates of 2026-08-26, 2026-06-19 and 2026-04-25.

The licence is BSD 3-Clause, and the LICENSE file is at the top of the repository, which is a permissive licence with a required notice. For a research project that is the expected choice, and it means the compiler sources and the proof development can be reused in commercial and academic work without copyleft obligations.

One more thing to keep in mind when you plan a build. The project uses the latest master version of HOL4, and HOL4 itself has its own compatibility requirements around Poly/ML. So the chain you are installing is Poly/ML 5.7.1, then HOL4 master, then CakeML, and each layer constrains the one below it. That is the main source of friction in getting a CakeML build working, and the build-instructions.sh script is where the answers are.

## Conclusion

CakeML fits a formal methods group that wants a programming language implementation with machine-checked proofs of its compiler and semantics, and that has a Poly/ML and HOL4 toolchain to work with. It is the wrong tool for shipping an application, since the deliverable is a proof development rather than a general purpose SML, and the subset of Standard ML it covers is explicitly partial. Before adopting, read the how-to.md document for the list of differences from SML and OCaml, and plan for the resource cost the project states, because building the bootstrapped compiler and its proofs is not a laptop task.

## FAQ

### What is CakeML and how is it verified?

CakeML is a verified implementation of a significant subset of Standard ML. The source and proofs are developed in the HOL4 theorem prover built on Poly/ML 5.7.1, and the semantics directory holds the formal definition of the language including concrete and abstract syntax, big step and small step semantics, FFI semantics and the type system.

### How do I build CakeML from source?

The README points to build-instructions.sh, which describes how to install Poly/ML, HOL and CakeML. Building all of CakeML including the bootstrapped compiler and its proofs requires significant resources, and built copies of the compiler are available from cakeml.org for anyone who only needs the artifact.

### What does the CakeML compiler actually verify?

The compiler directory covers lexing and PEG parsing, type inference, compilation to ASM assembly language, and code generation to x86, ARM and more. The translator directory holds a proof-producing translator from HOL functions to CakeML.

### Is there a full Standard ML standard basis library in CakeML?

Not yet. The basis directory is described as containing the beginnings of a standard basis library for CakeML, similar to the SML standard basis. The how-to.md document also lists how CakeML differs from SML and OCaml, which is the place to check before porting code.

## Sources

- [CakeML/cakeml on GitHub](https://github.com/CakeML/cakeml)
- [License: BSD-3-Clause](https://github.com/CakeML/cakeml/blob/master/LICENSE)
- [Project website](https://cakeml.org)
- [README](https://github.com/CakeML/cakeml/blob/master/README.md)
- [Releases](https://github.com/CakeML/cakeml/releases)

---

Hysen Labs editorial analysis, written from the project's own repository and release notes. Cite the canonical page: https://hysenlabs.com/projects/cakeml-cakeml