The Candle Interactive Theorem Prover

Candle = HOL Light implemented on top of CakeML

About

Candle is a fully verified interactive theorem prover for higher-order logic, more specifically: a fully verified clone of HOL Light running on top of CakeML. We have proved an end-to-end correctness theorem for Candle that guarantees the soundness of the entire Candle system down to the machine code that executes at runtime. This theorem states that every exported fact produced by this machine-code program is valid in higher-order logic. The Candle implementation consists of a read-eval-print loop (REPL) that executes the CakeML compiler internally. When designing Candle, we have strived to make the REPL of the new system provide a user experience as close to HOL Light's as possible. To this end, we have, e.g., made Candle parse the same variant of OCaml syntax as HOL Light. The verification of the Candle prover has been carried out in the HOL4 theorem prover.

Downloads

Candle is hosted on Github together with a fork of the HOL Light sources: github.com/CakeML/candle.

There is also a Dockerfile available here: Dockerfile.candle. The Dockerfile contains instructions on how to get started in comments.

Requirements

Candle requires a recent x86_64 Linux machine, a C compiler, and Make.

Installation and running

See this page for instructions on how to install and run Candle.

Printing theorems

The top-level correctness theorem for Candle is stated in terms of what is output on a special kernel-controlled FFI channel. To print a theorem and its logical context on this channel, call the Kernel.print_thm function on a value of type :thm from the REPL.

By default, Kernel.print_thm prints to stdout. You can redirect this output yourself by editing the function ffikernel_ffi() in the file basis_ffi.c before rebuilding CakeML.

If you have any issues, join our Discord (with this link) and see the #candle channel.