Formal Verification

Formal Verification

proofs/STATUS.md is the single authoritative registry. Where any other document — including this page — disagrees with it, that registry wins.

Status vocabulary

The project uses these terms precisely, and the distinction is load-bearing:

Term	Meaning
machine-checked	A proof assistant accepts it today (Qed / no holes) and it runs in CI
locally-checked	Accepted by the proof assistant locally; not yet in CI
conformance-checked	An implementation shown to refine a verified spec by differential testing — not a refinement proof
proved-on-paper	A written proof exists; not mechanised
statement-only	The theorem is stated (typed hole / Admitted); the proof is a tracked obligation
definitions-only	Syntax and rules defined; no theorems yet
absent	Does not exist, regardless of prose elsewhere

No proof hole is ever described as "proved." A statement-only theorem is an obligation, not a result.

What is proved

On the Coq track (authoritative), all real Qed. and axiom-free (Print Assumptions reports "Closed under the global context", asserted per rung in CI):

Solo core

• Progress (F1.3) and Preservation (F1.4, with the QTT substitution lemma ht_subst), plus affine_pres — budget preservation for the affine layer, a genuinely distinct theorem rather than an alias.
• Parametric soundness (R2–R4): the whole core is a functor SoloCoreF (M : ORDERED_SEMIRING). Include Linear3 recovers the concrete language; the Tropical (min-plus, infinite carrier) instance reuses the functor unchanged and remains axiom-free — an acceptance test proving the soundness argument never relied on a finite carrier.
• Executable checker (R5): check with check_correct : has_type G D t a ↔ check G t = Some (a, D) — sound and complete — plus aff_type_dec.

Elaboration

• M1: me → solo elaboration with me_wt_sound over the whole me_tm.

Session types (Ensemble metatheory)

A standalone development in SessionPi.v (~3.5 kLOC):

• Subject reduction, session fidelity, and progress / deadlock-freedom for the binary fragment (S1).
• Duet by projection (S2): projection_duality — a two-party choreography projects to dual local types — and corollaries transporting the whole binary guarantee across projection, so a projected config is deadlock-free by construction.
• n-party projection totality (S3a): projection_total, the first theorem quantifying over a genuine n ≥ 3 role space.
• Static n-party configuration (S3b), label-union merge (S3c.0), union-projection (S3c.1), n-ary located operational semantics (S3c.2), and head-coupled message + choice subject reduction (S3c.3-msg, S3c.3-choice) — the first earned n-party safety halves.

What is not proved

Stated plainly, because the fences matter:

• n-party progress (S3c.4) is open and research-hard. Note wf_assignment ra → deadlock-free is provably false, so this needs a coherence⇒safety argument rather than an extension of existing lemmas.
• Run-ahead / permutation subject reduction (S3c.3-perm) is open.
• μ typing up-to-unfolding (S1.3b-meta) is open.
• The Idris2 track is graded locally-checked, not machine-checked: its CI job runs idris2 --build with no hole assertion, and a typed hole type-checks. (Tracked as debt P-2.)
• The #typeck gap: the Rust checker is tested against the verified check, not proved equal to it. Closing this is the headline correctness goal.

The trusted base

grep '^\s*Admitted\.' over the proof tree returns zero. There are no sorry / admit / postulate / ?todo holes.

The 16 Axiom/Parameter occurrences in ResourceAlgebra.v are Module Type interface fields (SEMIRING, ORDERED_SEMIRING, RESIDUE_MEASURE), which is legitimate — they carry an explicit TRUSTED-BASE NOTE, and the scanner exemption for them is scoped and documented.

Running the proofs

just proofs        # both tracks
just proofs-coq    # coq_makefile + make — the authoritative track
just proofs-idris  # idris2 --build

CI runs the same in .github/workflows/proofs.yml, followed by ~10 separate Print Assumptions gate steps that fail the build unless "Closed under the global context" appears.

⚠️ That workflow currently triggers only on paths: proofs/verification/**, so a change to the checker or the QTT bridge does not re-run it — precisely the change most likely to break the spec↔implementation correspondence. Tracked as debt P-1.