The Candle Interactive Theorem Prover
Candle = HOL Light implemented on top of CakeML
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.
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.
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.
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
Kernel.print_thm function on a value of type
:thm from the REPL.
Kernel.print_thm prints to stdout.
You can redirect this output yourself by editing the function
ffikernel_ffi() in the file
before rebuilding CakeML.
If you have any issues, contact us on Slack on the