External-Prover Verification

Status: load-bearing CI gate. The kernel-soundness corpus is regenerated and re-checked through Lean 4 (lake build) and Coq / Rocq (coqc) on every release. Hard-error verdicts block merges. Honest IOUs (sorry / Admitted) are accountability surface, not failures — their count is pinned and surfaces immediately if it drifts.

1. Why this gate exists

Verum's kernel-soundness pipeline (verum audit --kernel-soundness) historically did three things:

1. Drift-checked the kernel rule registry against the .vr corpus.
2. Enumerated per-rule status (Proved / Admitted / DischargedByFramework).
3. Emitted parallel Lean 4 + Coq theory files into target/audit-reports/kernel-soundness/ for "independent re-checking".

Step 3 was load-bearing on paper but never invoked in CI. A foreign auditor was supposed to run lake build / coqc themselves. This is exactly the kind of trust-trap the pipeline was meant to prevent: the output existed, it looked plausible, and nothing mechanical confirmed Lean / Coq would actually accept it.

When this gate first ran it caught four type errors in the supposedly-proved lemmas — broken proof tactics that had been in the emitter for the entire history of the corpus:

Rule	Error	Root cause
K_Var_sound	ctx_lookup_sound Hrule Hwf applied a Prop where a CoreTerm was expected	proof emitter used the wrong names from intros
K_Univ_sound	exact universe_form_sound left ∀-residue	intros d Hrule consumed only 2 binders, leaving t T : CoreTerm
K_FwAx_sound	axiom_body_typed_in_prop body_prop — body_prop undefined	the emitter rcases'd a Prop as a tuple
K_Pos_sound	strict_positivity_sound strict_pos — strict_pos was a ByteArray	same rcases mistake

verum audit --kernel-soundness had reported the gate green for all four because it never asked Lean. verum audit --external-prover-replay fails immediately on this kind of regression.

2. What gets verified

2.1 Verum-side source of truth

• core/verify/kernel_soundness/ — the corpus (rule list, lemma names, admit reasons, framework citations).
• The kernel rule registry — the canonical 38-rule list with per-rule status (Proved / Admitted / DischargedByFramework).
• The cross-export pipeline — emits parallel Lean / Coq / Isabelle / Agda theory files from the rule registry.

The audit gate --kernel-soundness drift-checks all four.

2.2 Foreign-tool re-check

verum audit --external-prover-replay extends the gate with a real shell-out across four foundations:

Backend	Tool	Project	Invocation
Lean 4 (4.29.1+)	lake build	verification/external/lean/	builds VerumExternalReplay/KernelSoundness.lean
Coq / Rocq (9.0+)	coqc -Q . VerumExternalReplay kernel_soundness.v	verification/external/coq/	type-checks the export
Isabelle/HOL (2025-2+)	isabelle build -d . KernelSoundness	verification/external/isabelle/	re-elaborates KernelSoundness.thy
Cubical Agda (2.8+)	agda --cubical KernelSoundness.agda	verification/external/agda/	re-elaborates KernelSoundness.agda under cubical mode

The targets use different logics and export encodings. Their successful builds establish acceptance of those encodings under their declared assumptions. They do not automatically establish that all targets express the same theorem, or that the Rust implementation satisfies it. In particular, enabling Agda's cubical mode does not prove a postulated cubical rule sound.

Each backend reports one of four verdicts:

• clean — backend exited 0 with no diagnostics. The emitted declarations typecheck under their definitions and assumptions. A clean process exit does not certify axiom freedom.
• iou-only — backend exited 0; the only diagnostics are honest IOUs (typed-axiom declarations of shape axiom <Rule>_iou in Lean, Axiom <Rule>_iou in Coq, axiomatization blocks in Isabelle, postulate <Rule>-sound blocks in Agda) whose count matches the corpus's declared admit list. The IOU registry is currently empty (iou_axiom_specs() == vec![]) — every rule is structurally Proved or DischargedByFramework. A future brand-new rule that hasn't yet been proved would re-introduce an iou-only verdict; the audit gate's drift-check catches the re-introduction.
• hard-error — backend rejected the export with a real type / parse / scoping error. Load-bearing regression. Exits non-zero.
• not-available — backend binary missing. Advisory unless --strict; CI uses --strict.

3. The structural fragment (real inductive constructors)

An introduction-rule lemma proved by applying the corresponding constructor shows that the encoded judgment is closed under that constructor. This is useful for checking rule interfaces, but it does not prove that the Rust checker implements the judgment, that reduction preserves typing, or that the encoded system is consistent. Those require separate implementation correspondence and metatheory arguments.

The kernel-soundness export ships a real Typing predicate across all four foundations — never opaque well_typed t T placeholders. Each foundation declares the predicate in the shape its own elaborator handles best:

• Lean 4 and Coq / Rocq: a single inductive Typing : Ctx → CoreTerm → CoreTerm → Prop declaration with all 38 introduction rules. Lazy elimination-principle generation scales naturally to large constructor sets.
• Isabelle/HOL: a 9-rule inductive Typing covering the structural fragment (Var / Universe / Pi / Lam / App / Sigma / Pair / Fst / Snd) plus 29 independent per-rule axiomatization where T_<n>: "..." blocks for the cubical / refinement / quotient / modal / Diakrisis fragments. Independent blocks scope the type-inference unifier to one rule at a time. The export's main theorem is a lemmas kernel_full_soundness = bundle aggregating every per-rule lemma; auditors invoke print_facts kernel_full_soundness to enumerate the entire soundness corpus.
• Cubical Agda: per-rule postulate <Rule>-sound declarations whose signatures are still type-checked end-to- end (promoting these postulates to a structural data Typing : Ctx → CoreTerm → CoreTerm → Set mirrors the Lean/Coq trajectory and is tracked as future work).

Per-rule lemma proofs follow the foundation's idiom: apply (<constructor>) in Lean, apply (T_<n>) in Coq, apply (rule T_<n>) in Isabelle (against the axiomatization fact, uniformly for both inductive and axiomatized rules). Discharged-by- framework or admitted lemmas use the foundation's standard placeholder: sorry in Lean, Admitted. in Coq, sorry in Isabelle (registers the lemma as a fact so it stays referenceable from lemmas kernel_full_soundness), postulate in Agda.

Historically there were a handful of non-structural rules — those that genuinely depended on deep meta-theory not yet ported to mathlib / Coq stdlib / Isabelle's HOL — admitted via per-rule typed axioms named <Rule>_iou. The open-IOU set is now empty: every former IOU has been either promoted to a structural-premises constructor (the preferred route) or marked DischargedByFramework with a recorded upstream citation. A citation status does not itself instantiate or replay the cited proof for this implementation. The <Rule>_iou axiom shape is preserved so that future re-introductions stay drift-checked; each axiom takes the rule's actual operands and returns a Prop, so the soundness lemma's operand types are checked by the foreign tool even when the IOU itself discharges the conclusion.

So external-prover-replay verifies:

• ✅ Every emitted theorem statement parses and type-checks in the foreign tool.
• ✅ For every structural rule, the proof uses a real Typing constructor — not a placeholder. A bug in the structural emission (wrong arity, wrong name, missing premise) fails the build.
• ✅ Every IOU axiom name + arity + positional arg-type sequence matches the rule registry (drift-detected). The drift surface is closed in seven dimensions — every dimension fires a pin test at audit time with an actionable diagnostic:
  • Rule status ↔ IOU presence: per-rule status (Proved / Admitted / DischargedByFramework) is cross-validated against the actual <Rule>_iou axiom presence in the emitted theory files. Catches Admitted-without-axiom (status drift), Proved-with-orphan-axiom (incomplete discharge), and DischargedByFramework-with-axiom (redundant trust extension).
  • Registry ↔ each foundation (set): each foundation's IOU axiom block is parsed and its rule-name set asserted equal to the canonical IOU registry. Catches single- foundation-only edits (e.g. axiom added to Lean but forgotten in Coq).
  • Three-way set agreement: direct Lean = Coq = Isabelle set equality, separating axiom-name drift from rule-status drift in the audit output.
  • Three-way arity agreement: argument-arrow counts (→ / -> / \<Rightarrow>) are parsed per foundation; all three must agree per axiom. Catches same-name-different- arity drift (e.g. K_Refine_Intro_iou has 4 args in Lean but 5 in Coq).
  • Registry ↔ each foundation (arity): the IOU registry declares the canonical arity per axiom; pin tests assert each foundation's parsed arity matches the registry, anchoring the three-way agreement on a single source of truth.
  • Three-way per-position arg-type agreement: the positional type sequence (excluding Ctx and the return type) is parsed per foundation; all three must agree per axiom in both length and per-position type. Catches the drift class where one foundation has the same arity as another but with the args in a different order — invisible to arity-only checks.
  • Kernel registry ↔ Verum corpus (status + citations): core/verify/kernel_soundness/theorems.vr carries the parallel Verum-side narrative — per-rule KernelRule.K<Name> => LemmaStatus.<Status> entries plus, for every DischargedByFramework rule, the citation triple (lemma_path, framework, citation). Pin tests parse the .vr corpus and assert per-rule status + citation parity with the kernel rule registry (whitespace-normalized so multi-line continuations don't generate spurious diffs). Catches drift in the framework attribution that cites mathlib4 / Coq stdlib / ZFC upstream artifacts — the trust-extension surface a foreign auditor clicks through to verify a discharge.
• ✅ The shape of CoreTerm, CoreType, KernelRule mirrors the kernel's data definitions exactly (encoder bug surface).
• ✅ The IOU axiom registry is currently empty (iou_axiom_specs() returns vec![]) — every kernel rule has been promoted from open IOU to either a structurally-premised Proved constructor or a DischargedByFramework rule citing an attributed upstream result. This classification does not replay that result or establish its applicability. See framework axioms — IOU registry for the full discharge protocol. The historical IOU enumeration in §4 below is preserved as context — every entry there has since been closed; the drift-check in SoundnessExporter::drift_check continues to enforce the empty-registry invariant.

For a complementary check that exercises the runtime kernel — not just the meta-theory shape — see differential-lean-checker. That gate runs a 24-cert battery through both the trusted-base kernel and the Lean ReferenceChecker and asserts cert-by-cert verdict agreement.

4. Trust extension surface (steady state)

The kernel's trust-extension surface used to admit a handful of open IOU axioms — kernel rules whose soundness lemma was exported as axiom <Rule>_iou : Ctx → … → Prop rather than proved structurally. The registry is now empty: iou_axiom_specs() returns vec![], and every KernelRule carries either a Proved or DischargedByFramework status in canonical_rules().

Each entry below names how the rule is currently discharged. The historical "open IOU" framing is preserved alongside, since the same shape would re-apply if a brand-new kernel rule were added that hadn't yet been proved (the registry would re-acquire an Admitted entry plus an iou_axiom_specs row, the drift_check would notice, and the audit gate would flip until the structural proof landed).

Cubical (CCHM / HoTT mechanisation)

• K_Path_Ty_Form, K_Refl_Intro, K_Path_Over_Form, K_HComp, K_Transp, K_Glue — all Proved via the structural-premises template; the side conditions (CCHM regularity, Kan-filling compatibility, univalence-via-Glue) are the kernel's input contract — verified at runtime in support.rs::normalize_core rather than re-proved in the soundness theorem.

Refinement (predicate decidability at value)

• K_Refine, K_Refine_Omega, K_Refine_Erase, K_Refine_Intro — all Proved. K_Refine_Intro uses a 3-premise structural constructor (Typing Γ a base, Typing Γ base (Universe i), Typing Γ predicate (Pi x base (Universe 0))). Predicate-truth-at-the-introduced-value remains the kernel's runtime contract (mirroring K_Quot_Elim discipline).

Quotient (HIT)

• K_Quot_Form, K_Quot_Intro, K_Quot_Elim — all Proved with structural premises (scrutinee at the quotient, motive at the dependent universe, case_fn at the dependent product). The respect-of-equivalence side condition that mathlib's Quotient.lift requires its caller to discharge externally remains the kernel's input contract.

Inductive

• K_Inductive, K_Pos, K_Elim — all Proved. K_Elim uses the structural-premises template (mirroring K_Quot_Elim); K_Inductive is premise-free at the export layer — by the time the kernel sees an Inductive_(path, args) term, the strict-positivity invariant has already been verified at registration time by the inductive keyword analogue.

SMT / replay correctness

• K_Smt — Proved. Discharged via the structural premise T : Universe i ⇒ SmtProof solver_tag : T; the SMT-certificate replay is a kernel runtime contract enforced by replay_smt_cert.

Diakrisis (biadjunction + bridge-audit)

• K_Modal_Box, K_Modal_Diamond, K_Modal_Big_And, K_Shape, K_Flat, K_Sharp, K_Universe_Ascent, K_Epsilon_Of, K_Alpha_Of — all Proved via the wrap-preserves-typing template; the modal-depth recursion / cohesive adjunction content is the kernel's input contract.
• K_Eps_Mu — DischargedByFramework citing Mac Lane, Categories for the Working Mathematician, Theorem IV.7.3 (biadjunction triangle identities).
• K_Round_Trip — DischargedByFramework citing the internal bridge-audit specification.

These nine DischargedByFramework entries (the seven structural mathlib4 rules — K_Pi_Form / K_Lam_Intro / K_App_Elim / K_Sigma_Form / K_Pair_Intro / K_Fst_Elim / K_Snd_Elim — plus K_Eps_Mu and K_Round_Trip) are exactly what #print axioms kernel_soundness enumerates.

5. Running locally

# Prerequisites:
#   • Lean 4 via elan: https://leanprover.github.io/get_started/
#   • Rocq / Coq 9.x: brew install rocq  (macOS)
#                     apt install coq    (Debian/Ubuntu, pre-Rocq)

# Default — runs all three backends, soft-fails on missing tools.
verum audit --external-prover-replay

# Lean only (faster on a fresh machine — Lake bootstraps quickly).
verum audit --external-prover-replay --backend lean

# Isabelle only.
verum audit --external-prover-replay --backend isabelle

# CI-grade strict mode.  Fails the gate if any backend isn't
# installed; required reading for `--strict` is "if you can't
# install it, you can't claim it works".
verum audit --external-prover-replay --strict

# JSON for machine consumption.  Output written to
# target/audit-reports/external-prover-replay.json + stdout.
verum audit --external-prover-replay --format json

6. Wiring in CI

The gate is wired into CI via .github/workflows/audit-gates.yml. Three job tiers:

1. In-process gates (every push + PR, ~5 minutes) — --differential-kernel, --differential-kernel-fuzz, --kernel-soundness (which runs the drift guard), --kernel-rules, --kernel-recheck. No external toolchain.
2. Differential Lean checker (every push + PR, ~10 minutes uncached / ~2 minutes cached) — Lake artefacts cached.
3. Tri-prover replay (push to main only, ~30 minutes uncached / ~5 minutes cached) — Isabelle 2025-2 distribution
   • HOL heap cached; this caching is the load-bearing optimisation since first-build of the HOL heap takes 8-12 minutes on its own.

All three tiers upload target/audit-reports/ as workflow artefacts (14-day retention for tiers 1-2, 30-day for tier 3) so any drift / disagreement detected in CI has a downloadable forensic record.

The minimal manual --external-prover-replay invocation if you're scripting it outside CI:

- name: External-prover replay (Lean + Coq + Isabelle)
  run: |
    # elan + lake
    curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
      | sh -s -- -y --default-toolchain leanprover/lean4:v4.29.1
    source $HOME/.elan/env
    # rocq via apt or brew, depending on runner OS
    sudo apt-get install -y coq rocq-prover
    # isabelle 2025-2 (download + extract; brew --cask isabelle on macOS)
    curl -fsSL https://isabelle.in.tum.de/dist/Isabelle2025-2_linux.tar.gz \
      | sudo tar xz -C /opt
    export PATH="/opt/Isabelle2025-2/bin:$PATH"
    # pre-build HOL heap (slowest part on a fresh runner)
    isabelle build -b HOL
    # the tri-prover gate itself
    verum audit --external-prover-replay --strict

7. Maintenance

When adding a kernel rule:

1. Append the rule's identifier to the kernel rule enum.
2. Append a rule spec to the canonical rule registry with status set to admitted, citing the meta-theory dependency.
3. Mirror the entry in core/verify/kernel_soundness/theorems.vr (the drift gate cross-validates the two sides).
4. Run verum audit --external-prover-replay. The gate must stay green: iou-only is fine, hard-error means the Lean / Coq / Isabelle emission is broken — fix the emitter before merging.

When promoting an admit to a real proof:

1. Flip the rule's status from admitted to proved (or discharged-by-framework if upstream-cited), supplying a concrete tactic chain for each foundation.
2. Provide a tactic chain that closes the goal against the placeholder axioms (or — better — a real proof that doesn't rely on them).
3. Rerun the gate. The IOU count decreases; CI doesn't care about the absolute number, only about hard-errors.

8. Cross-references

• Trusted Kernel — the TCB this gate gives an external second opinion on.
• Differential Lean Checker — the complementary gate that checks runtime kernel verdicts against the Lean ReferenceChecker cert-by-cert. Different layer: this page proves theorem statements type-check; that page proves the operational kernel returns the same accept/reject judgements.
• Three-Kernel Differential — the within-process complement: the same 24-cert canonical battery also flows through three structurally-distinct in-process kernels (bidirectional / NbE / manifest-driven) and unanimity is asserted cert-by-cert.
• Verification Pipeline — the broader verification strategy this gate is one node of.
• verum audit CLI surface — full audit-flag table.
• Trust-extension report — enumerates every IOU axiom seen by external provers.