CleanQ Proofs in Isabelle/HOL

The CleanQ proofs in the Isabelle/HOL theorem prover.

License

See the LICENSE file. For the dependencies, see their licenses.

We provide make targets for building the proof documetation. For this, make sure you obtained the dependencies either manually, or using make deps

Then you can build the proofs and the documentation using

make

This should build a PDF build/cleanq-proofs.pdf.