An interactive theorem prover consists of a logical foundation governing expression and interaction of ideas, and a kernel that checks whether programs follow the foundation's rules.

“An interactive theorem prover has two basic components, a logical foundation, which determines how ideas are expressed and interact with each other, and a checker program, called a kernel, which verifies that programs correctly adhere to the rules of the logical foundation.”