Verified Proof Checking

We are building (or have built) several verified proof checkers using CakeML.

Examples include: The source code and proofs are freely available as part of CakeML (some binary releases are linked above).

Our cake_lpr and cake_pb tools are used to audit solver outputs in the annual international SAT solving competitions .


There is growing interest from various automated reasoning communities in building certifying algorithms, namely, tools that can not only solve a given problem, but output checkable evidence for the correctness of its solutions.

Such evidence often comes in the form of a proof log or certificate which can be independently audited by a proof checker, adding a layer of trust to automated reasoning results. A typical proof checking workflow is shown below.

A typical proof checking workflow

What CakeML brings to Proof Checking

First and foremost, verified proof checking means that the proof system and its checker implementation (including code optimizations) are proved sound/correct.

We see CakeML as a great fit for building such tools because:

This means that, to trust the output of CakeML-verified checkers, users need to trust little more than:

Such end-to-end verification results offer a minimal trusted base which is of the highest assurance standard for formally verified software.

Consequently, we see CakeML as a means for covering the last mile in trustworthy automated reasoning.

What Proof Checking brings to CakeML

Our efforts in building proof checkers have contributed to our understanding of pain points in the CakeML tooling and workflow for end-to-end verified software.

For example, we have improved our basis libraries and have ongoing plans to verify some new compiler optimizations to speedup our checkers.

We are also interested in extracting common components of our proof checkers into reusable libraries and frameworks that will enable others to easily build and verify their own CakeML-based checkers.

The Next 700 Verified Proof Checkers (Contact Us)

We are always interested in applying CakeML to build new proof checkers for various theories and certificate formats.

Get in touch with Yong Kiam Tan and/or Magnus Myreen with questions. Alternatively, join our Discord (with this link) and ping us there!