The Self-Checking Prover Study is Task 2 of the Foundations of Secure Formal Methods project. The main goal of this task was the design and development of a prover/checker pair for the HOL theorem proving system; that is, a version of the HOL prover modified to record and output the proofs that are made in the system, and a companion checker to determine whether such proofs are logically sound.

• proofchecker.ps