This checklist is the internal "HOL-grade" filter for papers whose core value depends on mechanized reasoning, theorem precision, and proof/artifact parity. Use it after the stable release gate and before venue-specific packaging.
It is intentionally stricter than a generic preprint bar. Passing this checklist does not guarantee acceptance at any specific venue; failing it means the work should not be presented as proof-heavy or theorem-grade yet.
See also Publication Pre-Flight Standard.
| Check | Requirement |
|---|---|
Central claims are theorem-sized |
The abstract, introduction, and conclusion state the actual theorem-level contribution, not a vague safety impression. |
Claim vocabulary is disciplined |
Use "prove" only for mechanized results, "show" for empirical evidence, and "conjecture" for unproven statements. |
Parameters and scope are explicit |
Every central theorem states its fragment, semantic model, trust boundary, and side conditions. |
Assumptions are ledgered |
Crypto assumptions, solver assumptions, parser totality assumptions, oracle models, and trusted FFI boundaries appear in one explicit assumption ledger. |
| Check | Requirement |
|---|---|
Proof artifacts compile cleanly |
Idris2/Lean4/Agda/Coq files build cleanly with no open holes, placeholders, or banned escape hatches. |
No hidden escape hatches |
|
Central claims are mechanized |
Every theorem that carries the paper’s contribution is represented in the proof artifact, not left as prose. |
The mechanization is project-specific |
Proof files are not template scaffolding, copied examples, or empty wrappers that only give the appearance of rigor. |
| Check | Requirement |
|---|---|
The theorem statement matches |
Quantification, hypotheses, and conclusions in the paper match the mechanized theorem without omitted side conditions. |
The implementation boundary is honest |
The paper distinguishes the proven core from unchecked tooling, runtime glue, external libraries, and foreign interfaces. |
Examples are representative |
Worked examples and case studies exercise the same fragment and assumptions described by the proofs. |
Benchmarks and tests do not outrun the theory |
Performance, integration, or safety claims outside the proven core are clearly labelled as empirical rather than proven. |
| Check | Requirement |
|---|---|
Build path is documented |
A reviewer can find the commands needed to build proofs, run tests, and regenerate paper tables or counts. |
Reviewer time is bounded |
The strongest claims can be checked in a reasonable session without private infrastructure or hidden steps. |
Supporting evidence is in repo |
Proof logs, benchmark commands, metadata, and bibliography are colocated with the paper or linked unambiguously. |
Release state is honest |
Repository maturity metadata, README wording, and paper wording all describe the same current release state. |
| Check | Requirement |
|---|---|
Related work is real and comparable |
Comparison claims cite real systems and specify the exact axis of comparison. |
Novelty claims are defendable |
"First" or "no prior work" statements are supported by a serious literature check, not intuition. |
Proof audience expectations are met |
Foundational and recent formal-methods references are present where they materially shape the claim. |
- GREEN
-
All central theorem claims are mechanized, parity is clean, and the paper can be defended to a proof-heavy audience without soft wording or hidden assumptions.
- YELLOW
-
Mostly there, but 1-3 repairable issues remain: missing side conditions, mislabelled claims, incomplete bibliography cleanup, or weak proof/artifact cross-linking.
- RED
-
The mechanization does not yet carry the paper’s core contribution, the proof story and implementation story diverge, or the theorem posture would collapse under close reading.