This is a bounded verification record for the shared type-family map and coordination layer. It records observed results, including failures and checks whose scope is narrower than their success message suggests.
The previous June affirmation remains available as a historical snapshot in Git. Its dates, paths, toolchain and proof inventory are not current verification receipts.
| Field | Observed value |
|---|---|
Repository |
|
Branch |
|
Checked commit |
|
Check session |
2026-09-09 UTC; anchor captured at |
Working tree |
Clean at the checked commit; the map regenerated without a diff. This affirmation is added after the checks and does not claim to verify itself. |
Local toolchain |
Just 1.56.0; Bash 5.2.37; Git 2.47.3; Agda 2.6.4.3; Graphviz 2.42.4 |
Checked commit signature |
|
Canonical metadata |
|
The observation horizon is this commit’s coordination files and the named checks below. Whole constituent proof suites, production deployments and general mathematical novelty are outside this record.
| Command | Exit | Meaning and limit |
|---|---|---|
|
0 |
SVG regenerates from its DOT source without a diff. |
|
0 |
The recipe’s required files, metadata and policy markers are present. |
|
0 |
Its required metadata/project markers are present; this is not a complete A2ML parser. |
|
0 |
The repository’s ownership boundary check passes. |
|
0 |
The named pipeline documents and descriptiles
agree on the guarded chain, invariants and dates ( |
|
0 |
The recipe’s licence/README/file-name checks pass. Its source-header scan examines at most 20 matching Rust/ReScript/Gleam files; this is not an exhaustive SPDX audit. |
|
0 |
The recipe’s licence-text marker check passes; it does not establish licence consistency across every file. |
|
0 |
The three prohibited credential-file
paths checked by this recipe are absent. Separately, the deterministic
|
|
0 |
All 28 workflows have lockfile coverage. The tool notes an inline validator SHA; it matches the lockfile’s reviewed pin. Offline coverage does not establish that mutable upstream refs have not moved. |
The actual validate-state recipe was also exercised against isolated fixtures:
valid metadata passed; missing metadata, missing project and absent state failed.
The aggregate just validate failed for each invalid fixture. These controls
establish failure propagation, not complete syntax validation.
The workflow SPDX check passed the repository and controls for a valid opening
comment header, a missing identifier and an identifier placed after YAML content.
The downloaded gh-actions-lock v0.1.6 linux-amd64 binary matched SHA-256
4181ec1da5408b34b9a542a7ee5c6ce3a4d6ac815c7d0206a00ceca8a817f4e3
and successfully ran the same offline coverage check.
| Command | Exit | Observed result |
|---|---|---|
|
0 |
No |
|
0 |
No |
|
1 |
One match: the comment saying "zero postulates"
in |
|
1 |
Unfilled setup placeholders, template references
and the Groove port-zero marker remain. |
|
1 |
The |
These are existing maintenance obligations, left visible. This record does not turn an empty proof loop or a failed scanner into evidence of verification. The current Agda cross-project files are present but were not rechecked here.
The first residual milestone belongs to residual-evidence-types.
Its latest checked publication
passed the minimal Agda core, three expected-rejection controls and two direct
comparisons with the published Echo and Epistemic interfaces. See the
proof status at that revision
for exact statements, pins and standard-library warnings.
The shared glossary links those bounded results. The map’s dashed arrows express conceptual relationships and further obligations. Composition, evidence revision, a certified finite checker and explorer correspondence remain open in the owning project.
Use the checked commit above and run each command in the tables independently, retaining its exit status and output. A later successful hosted check does not erase the listed local failures. A later source change needs a new record.
This record was prepared by Codex from the actual local runs and linked hosted results. The checked commit’s signature result is recorded separately from these claims; no additional maintainer attestation is asserted here.