Verified Proof Checking

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

Examples include:

cake_lpr for CNF unsatisfiability proofs (TACAS'21);
cake_pb a family of tools and problem frontends for pseudo-Boolean proofs, with support for decision and optimization problems (AAAI'24);
cake_xlrup for CNF-XOR unsatisfiability proofs,
cake_vipr for mixed-integer linear programming results.

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 .

Motivation

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.

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:

CakeML's translation mechanism readily turns logical definitions of proof systems into CakeML source code implementations.
CakeML's binary code extraction pipeline, including verified compilation, allows us to verify all of our tools down to their machine code implementations. Note that CakeML includes its own verified bignum library, garbage collection, and memory management (heap/stack layout).

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

The HOL definitions of the input parsers and the formalized semantic definitions for the logic or problem of interest.
The formal HOL model of CakeML's binary execution environment and its correspondence with the real system, e.g., ISA, foreign function interfaces, and memory layout. CakeML's target architecture models have been validated extensively.
The HOL4 theorem prover, namely its logic, LCF-style kernel implementation, and execution environment (i.e., your system).

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!