Skip to content

Proof-Assistant Kernel Check

Software tool — instantiates Generate-and-Verify Separation

Re-checks a machine-generated proof term against a tiny fixed set of primitive inference rules, so trust rests only on a small kernel however elaborate the search that produced it.

In a proof assistant, an enormous, fast, heuristic layer — tactics, automation, decision procedures, sometimes a language model — searches for a proof and emits a proof term: an explicit object encoding every inference. Proof-Assistant Kernel Check discards all trust in that search and hands the term to a small, fixed kernel that re-derives it one primitive rule at a time. If the kernel accepts, the theorem holds; if the elaborator was buggy, adversarial, or hallucinating, the kernel simply rejects. The one idea that makes this mechanism and not its siblings is where trust lives — not in a verdict alone but in the kernel's smallness: a few hundred lines you can audit by hand, so an unbounded, untrusted generator is made safe by a checker small enough to trust completely.

Example

A mathematician closes a lemma in a system like Lean with a single automated call — a tactic that searches thousands of rewrite steps and produces a proof term hundreds of lines long that no human reads. Before the lemma enters the library, the kernel type-checks that term: it walks each application of a primitive rule (modus ponens, substitution, the induction principle) and confirms the term's type is exactly the statement of the lemma. Two failures are caught the same way. The tactic might have proved a slightly different statement — the kernel sees the type mismatch and rejects. Or it might have taken an unjustified step — the kernel finds no primitive rule licensing it. Only a term that survives the kernel's independent re-derivation is admitted. The elaborator that found the proof can be arbitrarily clever and wholly untrusted; the kernel that certifies it changes only across major releases and is small enough to be read line by line.

How it works

  • Ignore the search; keep only the artifact. The kernel receives the finished proof term, not the tactic script that built it, and owes the generator no cooperation.
  • Re-check every inference against primitives. Each node of the term must be licensed by one of the logic's fixed inference rules; the kernel re-runs the whole derivation rather than sampling it.
  • Bind the proof to the exact goal. Acceptance requires the term's type to be definitionally equal to the stated theorem — proving a neighbour does not count.
  • Concentrate all authority in the kernel. Everything outside it (tactics, libraries, elaboration) can be wrong without compromising soundness; only a kernel bug can.

Tuning parameters

  • Kernel surface area — how much logic lives inside the trusted core. A leaner kernel is easier to trust but forces more work onto untrusted layers; a richer kernel is more convenient but enlarges what you must believe.
  • Definitional-equality budget — how hard the kernel works to unfold definitions when matching the term's type to the goal. More unfolding accepts more proofs but slows checking and can diverge.
  • Independent re-implementation — whether a second, differently-written kernel must also accept. Catches kernel bugs at the cost of maintaining two.
  • Proof-term retention — whether terms are kept for re-checking or discarded after first acceptance. Retention enables re-verification under a future kernel; discarding saves storage.

When it helps, and when it misleads

Its strength is that it decouples finding a proof from trusting it, so you can point the most aggressive, opaque automation — including a model — at a goal and still accept only what a tiny, auditable kernel re-derives. That is the cleanest realisation of the archetype's asymmetry: proof search is unbounded, proof checking is small and fixed.

Its failure modes are quiet ones. The kernel certifies a proof in its logic, so a bug in the kernel, an inconsistent axiom the user added, or a mismatch between the formal statement and the informal theorem the mathematician meant all pass without complaint — the check is only as meaningful as the statement it binds to.[1] The classic misuse is trusting a large "verified" pipeline whose trusted base has quietly grown: every extra-logical extension, unchecked native evaluation, or trusted external oracle enlarges the kernel you were relying on being small. The discipline is to keep the trusted computing base minimal and explicit, and to treat statement-faithfulness — does the formal goal say what you think? — as a separate, human review.

How it implements the components

  • trusted_verifier_kernel — the mechanism is the kernel: the small fixed core that holds all soundness-critical authority.
  • checkable_acceptance_predicate — "this term type-checks against the primitive rules and has the goal's type" is the explicit, decidable accept/reject predicate.
  • candidate_evidence_binding — acceptance binds the proof term to the exact stated theorem, so evidence cannot be swapped for a proof of something else.

It does not model the generate-vs-check cost asymmetry or separate the two roles (generation_verification_cost_model, generator_verifier_role_separation) — that is Untrusted Solver with Trusted Checker — nor define the certificate contract and release gate an artifact carries across a trust boundary (witness_or_certificate_contract, verdict_and_release_gate), which is Proof-Carrying Artifact Gate.

Notes

The kernel checks proofs already expressed in its logic; it says nothing about whether the formalization faithfully captures the intended claim. That gap — between a verified statement and the theorem a human meant — is closed by no checker, and is the standard place formal "certainty" leaks.

References

[1] The de Bruijn criterion: a proof assistant is trustworthy if its proofs can be checked by a small, independent program simple enough to verify by inspection. It is an argument about the size of the trusted base, not a guarantee that the stated theorem matches informal intent. ↩