The De Bruijn Criterion and What a Proof Kernel May Assume

A proof assistant contains two programs that disagree about what a proof is. The tactic language, the elaborator, and the automation produce candidate proofs. The kernel decides whether a candidate is a proof. Everything the user interacts with is untrusted, and the kernel is the only component whose bugs can make a false statement provable. The property that makes this arrangement meaningful is that a proof is checked by reasoning about the proof object alone, without reproducing the search that found it. That is the de Bruijn criterion.

The criterion

De Bruijn formulated the requirement while designing AUTOMATH, a language for writing mathematics in a form a machine could check. The essential content is that a proof object carries enough information to be verified without repeating the search that produced it. A checker reads the object, applies the rules, and accepts or rejects. It does not need to be clever, and it does not need to know how the object was constructed.

The criterion has a corollary that shapes system architecture. If checking is independent of finding, then the finding machinery can be arbitrarily large, buggy, or heuristic, and the soundness of the system is unaffected. A tactic that silently produces a wrong proof is caught by the checker. This is the LCF arrangement: a small logical core, with tactics implemented as programs that construct proofs in the core, so that no tactic can produce a theorem the core would not accept.

The arrangement is not free. Producing explicit proof objects is expensive in space and in the time spent constructing them, which is why systems differ in how much of the object they materialise. Some store the full derivation; some store a certificate that a checker expands; some store nothing and re-run a deterministic checker. All three satisfy the criterion as long as the final check is independent.

What the kernel must contain

The kernel implements the typing rules of the core language and nothing else. Concretely it needs: a term representation with binders, an environment for definitions and constants, a conversion check for definitional equality, and the typing rules for the core’s formers. It does not need a parser, a pretty-printer, a module system, or a tactic engine.

That list is short, and keeping it short is the engineering problem. Every feature that reaches the kernel adds a case to its rules and a clause to its soundness argument. A kernel of a few thousand lines is auditable by a person; one of hundreds of thousands is not, and the difference is usually the accumulation of conveniences that were easier to put in the kernel than to encode outside it. The elaborator described in Elaboration is the clearest example of machinery that belongs outside.

The conversion check is typically the largest part. It needs the evaluator described in Normalisation by Evaluation for Conversion Checking, and the evaluator must be correct for the kernel’s soundness, not merely fast. A bug that makes two distinct types convert would let a proof of one statement be used as a proof of another, and no amount of re-checking elsewhere would catch it.

The trusted base is larger than the kernel

The kernel is the component that must be correct, and it is not the only thing that must be correct for a theorem to mean what the user thinks. The trusted base includes:

The definition of the logic. If the kernel implements a type theory with a universe that contains itself, the theory is inconsistent and the kernel faithfully checks proofs of falsehood. Soundness is a property of the specification, not of the implementation.

The axioms declared by the user. An axiom is a constant with a type and no body, and the kernel accepts it because it was told to. A user who declares an axiom of excluded middle in an intuitionistic system, or an axiom asserting the consistency of the system, has extended the trusted base by exactly that much. Systems track axioms so that a theorem’s dependencies can be reported, which is the only defence.

The compiler and runtime. A kernel written in a language with undefined behaviour, or one that relies on an optimising compiler that miscompiles an overflow check, is trusted at the level of the whole toolchain. Some projects address this by extracting the kernel to a simpler language, or by writing a separate checker in a different language and comparing answers.

The statement being checked. A theorem about a formalised definition says nothing about the informal concept unless the definition is right. This is not a soundness failure, and it is the most common way a verified result fails to mean what its author intended.

Reflection and its cost

Proof by reflection replaces a proof term with a computation. Instead of building a derivation showing that a boolean expression evaluates to true, the kernel evaluates the expression and accepts the result. This makes some proofs dramatically shorter, because the computation is performed once rather than encoded step by step.

The cost is that the evaluator now participates in soundness. A reflective decision procedure is correct only if the kernel’s evaluation is correct and the boolean it returns is a faithful encoding of the proposition. Both conditions are checkable in principle, and both are easy to get subtly wrong: an evaluator that is fast because it uses unverified arithmetic, or an encoding that omits a case, produces a kernel that accepts false statements while every individual proof term looks well-formed.

The standard discipline is to keep reflection inside a proved correct wrapper: the decision procedure returns a boolean, and a proved lemma states that the boolean is true exactly when the proposition holds. The kernel still evaluates, so the trusted base grows by the wrapper’s statement, and it does not grow by the procedure’s implementation.

Checking is not verifying meaning

A kernel that accepts a term establishes that the term has the type it claims, relative to the constants and axioms in scope. It does not establish that the type expresses the intended theorem, that the definitions match any external standard, or that the axioms are consistent.

Two consequences follow for how proofs are presented. First, a formalisation should state its main theorem in a form that can be read without unfolding definitions, so that a reader can compare it with the informal claim. Second, the axioms a proof depends on should be printed alongside it, because a proof that relies on an unproved assumption is a conditional result and should be reported as one.

The QED manifesto made the first point at scale. Its 1994 text proposed a long-term project to formalise a substantial body of mathematics with machine-checked proofs, and argued that the result would be worth little unless the formal statements were written in a form a mathematician could read and compare with the informal ones, and unless the checking could be repeated. The second point is a matter of tooling, and it is why systems provide commands to print the axioms used by a theorem rather than leaving the question to inspection.

Why independence matters more than size

A small kernel is easier to audit, and the deeper property is independence. Two checkers written by different people from the same specification, agreeing on a nontrivial proof, provide evidence that neither has a bug in the shared cases. One checker, however small, provides only the evidence that its authors were careful.

This is why some projects implement a second checker for the same proof format, and why the format matters. A proof object that can be exported and checked by an unrelated program is a portable certificate; a proof that exists only as a sequence of tactic invocations is not, because re-running the tactics requires trusting the tactic engine. The trade-off is between the size of stored proofs and the independence of the check.

The practical limit is that independence is expensive to achieve and rarely complete. A second checker usually shares the specification, the term representation, and often the parser, so agreement rules out implementation errors in the rules but not misreadings of the specification. That residual risk is why the specification itself, and the argument that the type theory is consistent, remain part of the trusted base no matter how many checkers agree.