[CakeML] Verifying CakeML programs

Magnus Myreen magnus.myreen at gmail.com
Thu Aug 11 07:51:42 UTC 2016

Hi Gergely,

> upon reading
> https://cakeml.org/popl14.pdf

You'll find a a more up-to-date description here:


> I see that the CakeML system is a verified implementation of the CakeML
> language, where the compiler is not written in CakeML (yet), but it is
> directly encoded as higher order logic formulae.

We automatically generate a CakeML implementation of CakeML compiler.
This was done for version 1 (POPL'14) and is part of the bootstrapping
of the compiler that the POPL paper is talking about. For version 2
(ICFP'16), bootstrapping is not yet complete; we are working on it
right now.

> And, it is not a program verification system for CakeML programs (yet).
> Is the above correct? Will there be an extension where I can verify CakeML
> programs, down to machine code?

Yes. For the last 5 months Armaël Guéneau has been visiting Chalmers
(where I'm based) and has formalised Arthur Charguéraud's
characteristic formula (CF) technology for CakeML. You can read more
about CFML here:


CakeML's CF framework is very new and has not been used on serious
examples yet. I expect the CF program verification system for CakeML
to become practically usable in the next 3-4 months.


More information about the Users mailing list