// SPDX-License-Identifier: CC-BY-SA-4.0
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>

= TRG Qualifying Provers — v1.0
:status: v1.0 — annual re-baseline
:date: 2026-04-12

This document defines the *qualifying prover set* referenced from
`TOOLCHAIN-READINESS-GRADES.adoc` §6.2. A "fully-proven program" under
TRG must be machine-checked by at least one prover from this set
(grade D, C), at least two independent provers from this set
(grade B), or at least three independent provers from this set with
at least one having a published kernel-soundness proof (grade A).

== v1.0 qualifying set

[cols="1,2,4",options="header"]
|===
| Prover | Tradition | Why qualifying

| *Idris2* | Dependently-typed functional / Edwin Brady's lineage from Idris1 | Active development, dependently-typed core, strong totality and termination checks, used as the *preferred backend* for hyperpolymath proofs per estate convention; published kernel design. *Hyperpolymath default.*
| *Lean 4* | Microsoft Research / Leonardo de Moura's lineage; foundation of mathlib4 | Extremely active community, mathlib4 is the largest single body of machine-checked mathematics in any prover, kernel is a small core based on Calculus of Inductive Constructions, published kernel-soundness arguments by de Moura et al.
| *Rocq* (formerly Coq) | INRIA / Calculus of Inductive Constructions | Foundational tool of formal-methods practice for over 30 years; CompCert and seL4 are written in/verified with Rocq; small trusted kernel; well-studied metatheory; published kernel-soundness work by Sozeau et al.
| *Agda* | Chalmers / Norell's PhD lineage; Martin-Löf type theory | Cubical Agda extension is the leading tool for HoTT-style proofs; strong universe polymorphism; well-suited to constructive mathematics; active community; published kernel design.
|===

== Qualifying criteria

To remain in the qualifying set at the annual re-baseline, a prover MUST satisfy:

. *Active maintenance.* At least one core-team release in the
  preceding 12 months. Abandoned provers are removed from the set.
. *Kernel design is published* and reviewable. The trusted computing
  base must be small enough that a determined reviewer can audit it.
. *Public test suite* covering the kernel and the standard-library
  proof obligations.
. *Public reference manual* describing the language, the type theory,
  and the proof tactics.
. *Reproducible builds.* The prover binary must be reproducibly
  buildable from a clean environment.
. *Community of at least 1000 distinct users* — measured by
  downloads, active issue/PR contributors across multiple
  jurisdictions, or equivalent. Single-organisation provers do not
  qualify.
. *No known soundness bugs* outstanding for more than 90 days. A
  prover with an unaddressed soundness bug is removed from the set
  until the bug is fixed.
. *Banned-construct discipline.* The prover must distinguish clearly
  between *axioms* (acceptable, must be declared) and *escape
  hatches* (`Admitted`, `sorry`, `postulate`, etc.). The prover must
  emit a clear warning when an escape hatch is used.

== A-grade kernel-soundness criterion

For *A-grade* TRG components, at least one of the three qualifying
provers used in cross-validation MUST have a *published kernel
soundness proof* — i.e. a paper or technical report by the prover's
authors or independent reviewers establishing the consistency of the
prover's kernel relative to a well-understood meta-theory.

As of v1.0:

* *Lean 4* — kernel-soundness work by de Moura, Carneiro, Ullrich,
  and others. Multiple peer-reviewed publications.
* *Rocq* — Sozeau et al., "Coq Coq Correct! Verification of Type
  Checking and Erasure for Coq, in Coq" (POPL 2020); MetaCoq project.
* *Idris2* — kernel design published by Brady; less mature
  meta-theoretic verification work than Lean / Rocq but actively
  pursued.
* *Agda* — kernel design published; meta-theoretic verification of
  Cubical Agda's kernel is an active research area but not
  comprehensively peer-reviewed yet.

For v1.0, *Lean 4* and *Rocq* unambiguously satisfy the
kernel-soundness criterion. *Idris2* and *Agda* are in the
qualifying set but should not be the sole kernel-soundness anchor
in an A-grade signoff until their meta-theoretic verification work
matures further.

== Re-baseline cadence

This document is reviewed annually on 2026-04-12 + N years. At each
review:

. The qualifying-criteria checks are re-applied to every prover in
  the current set.
. Any prover that has fallen below the criteria is *removed* (with
  90 days notice to dependent components).
. New provers that meet the criteria are *considered for addition*
  (with co-signing by at least two reviewers).
. The kernel-soundness criterion is re-evaluated against the latest
  published metatheoretic work for each prover.
. Components that depended on a removed prover are notified and
  given a transition window to migrate to a remaining prover.

The annual review is itself a public process. The review minutes
are archived at `audits/qualifying-provers-review-<year>.adoc` in
this repo.

== Type-theory frontier

TRG explicitly anticipates new provers joining the set as type
theory advances. Areas of active interest:

* *Cubical type theory* (Cubical Agda, Lean cubical extensions) —
  enables computational interpretations of higher-inductive types
  and Univalence
* *Observational type theory* — quotient types and proof-irrelevance
  with definitional equality
* *Two-level type theory* (2LTT) — separating fibrant and pre-fibrant
  layers for mixed classical/constructive reasoning
* *Linear / affine dependent type theory* — Granule, LinearML, and
  the Idris2 quantitative type theory work
* *Refinement type systems* with SMT integration — Liquid Haskell,
  F*, RefinementML

Hyperpolymath toolchain projects are *expected to contribute* to
this frontier where they reach it. The type-theory upstream
contribution requirement at A-grade (per
`TOOLCHAIN-READINESS-GRADES.adoc` §5.7.3) makes this expectation
load-bearing, not aspirational.

== Open invitation

If you think a prover is missing from the qualifying set or should
be removed from it, propose the change with the criteria checks
filled in. If you think the criteria themselves are wrong, propose
a tightening with evidence.
