chore(checkpoint): 2026-06-05 repo reconciliation + docs/machine_readable refresh — resume tracker

Durable resume-point for the 2026-06-05 estate checkpoint (echidna + echidnabot), created so a compacted/next session continues without losing the audit. Spans the dogfood proof-CI work that just went green.

Decisions (owner-confirmed)

PR fix(proofs+ci): repair proof corpus, unbreak Agda CI, and gate every proof in CI #234 (proof corpus + dogfood proof-CI, all green): squash-merge.
Stale branches: delete only test-gpg-sign + test/ci-echidna-hypatia-fix (leave claude/dev-self-provision).
rsr-template ↔ standards divergence: attempt via WebFetch (repos outside this session's scope; no add_repo/list_repos).

Remaining actions

echidna

Squash-merge PR fix(proofs+ci): repair proof corpus, unbreak Agda CI, and gate every proof in CI #234 (flip draft→ready first). Squash msg drafted below.
Delete test-gpg-sign + test/ci-echidna-hypatia-fix. NOTE: git push origin --delete failed ("remote end hung up; Everything up-to-date") — retry via colon refspec git push origin :refs/heads/<b> or a delete-ref MCP path.
On a new claude/checkpoint-2026-06-05 branch off post-merge main (draft PR), refresh:
- .machine_readable/6a2/STATE.a2ml — bump last-updated → 2026-06-05; add dogfood-proofs-ci session entry.
- docs/ROADMAP.md + .machine_readable/ROADMAP.a2ml — record proof-corpus CI as a Stage-1 gate.
- .machine_readable/6a2/{META,AGENTIC,NEUROSYM,PLAYBOOK,ECOSYSTEM}.a2ml — reference the proof-CI gate.
- docs/wiki/* — add proof-CI + just proofs* local-run docs (must be bleeding-edge).
File issue: --features verisim 22 compile errors (only genuinely-untracked TODO item; docs/handover/TODO.md P2).
(minor) document why two ANCHOR.a2ml exist (anchors/ repo-identity vs 6a2/ SSG-build); note contractile-trident asymmetry (adjust/+bust/ carry full Nickel tridents; dust/intend/must/trust carry only the .a2ml).

echidnabot (branch already == main → new `claude/checkpoint-2026-06-05` + draft PR)

README.adoc — fix stale "129 tests / ~90%" → 184 and "12-prover enumeration" → ProverSlug dynamic (EXPLAINME.adoc already holds the truth).
Archive SESSION_SUMMARY_2026-01-29.md (stale, pre-hardening).
(minor) move contractiles/dust + contractiles/trust under .machine_readable/contractiles/ for alignment; root Mustfile is a stub.
.machine_readable/6a2/STATE.a2ml — bump last-updated → 2026-06-05.

rsr-template

WebFetch hyperpolymath/rsr-template + standards repo; report any divergence vs the RSR rules echidna/echidnabot embed.

Already-good — do NOT touch

echidna Dustfile.a2ml + Bustfile.a2ml fully written; k9 svc/ templates real; README/EXPLAINME/wiki have no stale proof claims.
Both repos: A2ML migration complete (no stale .scm), SHA-pins current — no alarming standards drift found within scope.
Out-of-checkpoint-scope branches (leave alone): dependabot/* (4), pr-183, chore/training-infrastructure-cleanups.

Squash message for #234

title: fix(proofs): repair proof corpus + gate it in CI (Coq, Lean, Agda, Idris2)
body: Repairs proofs/{coq,lean,agda} + src/idris so all type-check; adds .github/workflows/dogfood-proofs-ci.yml (Coq/Lean/Agda); extends idris2-abi-ci.yml to type-check the src/idris validator; adds just proofs* recipes. Fixes two latent bugs: proofs/lean/lakefile.lean now roots every module (lake build was silently broken) and src/idris/Validator.idr gained a main. CI uses plain run: installs (works around a taiki-e/install-action startup_failure) + GitHub-pinned agda-stdlib v1.7.3 (apt --fix-missing was silently dropping it).

Checkpoint progress — 2026-06-13

Shipped

echidna checkpoint(2026-06-13): record dogfood proof-CI in state/roadmap/wiki + harden Lean job #244 (draft, open): STATE.a2ml session entry + date; ROADMAP.a2ml Stage-1 proof-CI gate + dates; docs/ROADMAP.md governance note; docs/wiki/{Getting-Started,Home}.md just proofs* docs; + Lean CI hardening (pre-install pinned toolchain with retry/backoff — fixes the elan "failed to parse latest release tag" flake from fix(proofs+ci): repair proof corpus, unbreak Agda CI, and gate every proof in CI #234). CI green — Coq/Lean/Agda + Validate A2ML manifests all pass; ready for review/merge.
echidnabot fix(ci): rust-ci.yml use --features verisim, not --all-features (#85) #86 (MERGED): README test count 129 → 184 (×3) + 12-prover enumeration → ProverSlug-based addressing.
fix(verisim): cargo check --lib --features verisim fails with 22 errors #245 filed: --features verisim 22 compile errors (was only tracked in docs/handover/TODO.md P2).

Blocked / not possible from this tooling (need owner)

Delete test-gpg-sign + test/ci-echidna-hypatia-fix: git proxy returns HTTP 403 on ref deletes; GitHub MCP has no delete-branch tool. One-line owner action.
rsr-template ↔ standards divergence check: WebFetch https://github.com/hyperpolymath/rsr-template → HTTP 404 (private/moved); it's also outside this session's GitHub scope. Could not assess divergence — owner-side.

Deferred (entangled — flagged, not done blindly)

echidnabot STATE.a2ml date bump: triggers the dual-truth obligation (.machine_readable/ must land in both standalone and the echidna monorepo copy) — do deliberately with the mirror.
Archive echidnabot SESSION_SUMMARY_2026-01-29.md: listed in CANONICAL_SOURCE.md's "standalone → fleet shared surface" table; moving needs that table + fleet sync updated.
echidnabot contractile asymmetry: dust/must/trust only under root contractiles/, intend only under .machine_readable/contractiles/ — structural, needs reference-safe move.

Findings flagged (no change made)

Prover-count drift across surfaces: GH repo description "48" · ROADMAP.a2ml "105" · STATE.a2ml/echidnabot "113" · wiki "128". docs/PROVER_COUNT.md is canonical (R5a, owner-managed) — recommend reconciling, starting with the repo description.
echidnabot governance / Licence consistency fails (pre-existing): LICENSE has no SPDX-License-Identifier: header. Owner-only domain (src/rust/main.rs SPDX-FileCopyrightText hook blocks any commit (Owner = 'ECHIDNA Project Team' not canonical) #216/fix(licence): #3 isolated — clear scaffold-placeholder leak (echidna) #83) — left untouched.
echidnabot Hypatia scan: 83 findings (stale SONNET-TASKS.md; missing_timeout_minutes across 8 workflow YAMLs; curl|sh in echidnabot.yml). All pre-existing, none from the README PR.
estate-standardization-20260607 branch: no PR, behind main at the same SHA as chore/training-infrastructure-cleanups — looks abandoned.
TESTING-REPORT.scm (echidnabot, in CANONICAL_SOURCE.md): candidate for the .scm→.a2ml deprecation rule — worth an owner check.

Checklist items 1 (merge #234) ✓, doc/wiki/machine_readable refresh ✓ (via #244), verisim issue ✓ (#245). Remaining are the owner-only blocked items + deferred entangled items above.

Generated by Claude Code

checkpoint(2026-06-13): record dogfood proof-CI in state/roadmap/wiki…

Hand-off brief — branch reconciliation + remaining audit (2026-06-13)

Tee-up for a fresh thread (this one is context-heavy). Start by reading this issue top-to-bottom.

A. Branch reconciliation (live data, both repos)

All deletes are owner-only — the git proxy returns 403 on ref-deletes and the GitHub MCP has no delete-branch tool.

echidna

Branch	Verdict	Why
`chore/training-infrastructure-cleanups`	DROP	empty diff vs `main` — unsquashed source of #232 (merged)
`estate-standardization-20260607`	DROP	byte-identical dup of the above (same SHA `c73c40e`)
`pr-183`	RESCUE → DROP	53 behind; Chapel 2.3→2.8 = merged #183; tip `fix(ci): add missing timeout-minutes to all workflow jobs` (~10 workflows) is unmerged + valuable — same gap Hypatia flags. Re-apply fresh on `main`, then drop the stale branch (don't merge it — conflict-prone)
`test-gpg-sign`, `test/ci-echidna-hypatia-fix`	DROP	test branches, no unique value
`dependabot/github_actions/actions-9419e0c084` (PR #243)	MERGE (owner/automerge)	routine SHA-pinned bump (checkout 6.0.2→6.0.3, taiki-e 2.81.5→2.81.10). NB: the taiki-e bump won't fix the allowed-actions `startup_failure` — that's policy, not version

echidnabot

Branch	Verdict	Why
`estate-standardization-20260607`	DROP	`IN-MAIN` (0 ahead) — already merged

→ After the 6 deletes + #243, both mains are reconciled. Net-new task: rescue pr-183's timeout-minutes hardening (echidna) — also closes a Hypatia finding.

B. Remaining currency audit (horizontal sweep — do in a fresh thread)

Already cleared earlier (do NOT redo): Dust/Bust contractiles, k9 svc/, A2ML migration, SHA-pins, README/EXPLAINME/wiki proof claims. Still to verify/refresh (both repos):

6a2 siblings — add proof-CI reference to META/AGENTIC/NEUROSYM/PLAYBOOK/ECOSYSTEM.a2ml (low value).
Contractile currency — Must/Intend/Adjust/Trust (Dust/Bust done).
ANCHOR.a2ml — no realignment to record, but DO document the dual-ANCHOR asymmetry (anchors/ identity vs 6a2/ SSG-build) + contractile-trident asymmetry.
Sweep bot_directives/, self-validating/, anchors/, contractiles/ dirs — not audited this session.
echidnabot deferred trio — STATE date-bump (needs dual-truth mirror), SESSION_SUMMARY_2026-01-29.md archival (in CANONICAL_SOURCE.md table), contractile location asymmetry; + TESTING-REPORT.scm .scm→.a2ml deprecation check.

C. Owner-only (not doable from agent tooling)

Delete the 6 stale branches in §A (proxy 403).
rsr-template ↔ standards divergence (WebFetch 404 / outside session scope).
Prover-count drift: GH repo description 48 vs ROADMAP.a2ml 105 vs STATE/echidnabot 113 vs wiki 128 — canonical is docs/PROVER_COUNT.md; start with the repo description.
echidnabot Licence consistency (LICENSE missing SPDX header) + Hypatia 83 findings (workflow timeouts, curl|sh in echidnabot.yml, stale SONNET-TASKS.md) — license/SPDX edits stay owner-only (src/rust/main.rs SPDX-FileCopyrightText hook blocks any commit (Owner = 'ECHIDNA Project Team' not canonical) #216/fix(licence): #3 isolated — clear scaffold-placeholder leak (echidna) #83).

Start-here

Read #238 → both CLAUDE.md (note the Haiku-scout pattern before bulk edits) → do §B as one scoped PR per repo → keep license/SPDX owner-only.

Generated by Claude Code

ci: add timeout-minutes safety bound to every workflow steps-job

Checkpoint closed — done or relegated (2026-06-13)

Per "close all we can, issue-ify the rest," everything in this tracker is now either merged or a discrete issue. Closing as completed.

Merged this session

fix(proofs+ci): repair proof corpus, unbreak Agda CI, and gate every proof in CI #234 — proof corpus repaired + dogfood proof-CI
checkpoint(2026-06-13): record dogfood proof-CI in state/roadmap/wiki + harden Lean job #244 — STATE/ROADMAP/wiki refresh + Lean toolchain hardening
ci: add timeout-minutes to every workflow steps-job (rescues pr-183, closes Hypatia finding) #247 — timeout-minutes across all echidna workflow steps-jobs (rescued pr-183's only value)
echidnabot fix(ci): rust-ci.yml use --features verisim, not --all-features (#85) #86 — README test-count + ProverSlug fixes

Done now

echidnabot chore(deps): bump openssl from 0.10.79 to 0.10.80 in the cargo group across 1 directory #89 (draft) — the one real missing_timeout_minutes gap (echidna-fuzz rate-limit-check); other Hypatia timeout flags are caller-workflow false-positives (see licence(#7): PMPL-1.0 -> PMPL-1.0-or-later (owner carve-out, SPDX-only) #88)

Spun-out issues (one per remaining category)

echidna fix(verisim): cargo check --lib --features verisim fails with 22 errors #245 — --features verisim 22 compile errors
echidna fix(ci): formal-verification creusot-verify cannot apt-install alt-ergo #250 — creusot-verify can't apt-install alt-ergo
echidna docs: reconcile prover-count drift across surfaces #251 — prover-count drift reconcile
echidna chore: machine_readable + contractile currency audit (both repos) #252 — machine_readable + contractile currency audit (both repos)
echidna chore: delete reconciled stale branches (owner action) #253 — delete 6 reconciled stale branches (owner; proxy blocks ref-deletes)
echidna chore: reconcile RSR divergences vs standards (verified 2026-06-15) #254 — rsr-template ↔ standards divergence (needs repo access)
echidnabot fix(ci): .clusterfuzzlite/Dockerfile symlink -> Containerfile #87 — LICENSE missing SPDX header (owner)
echidnabot licence(#7): PMPL-1.0 -> PMPL-1.0-or-later (owner carve-out, SPDX-only) #88 — post-checkpoint hygiene + Hypatia follow-ups

Also: Dependabot #243 was closed unmerged (separately).

No remaining untracked work. ✅

Generated by Claude Code

ci: add timeout-minutes to echidna-fuzz rate-limit-check job

Navigation Menu

Repository navigation

chore(checkpoint): 2026-06-05 repo reconciliation + docs/machine_readable refresh — resume tracker #238

Decisions (owner-confirmed)

Remaining actions

echidna

echidnabot (branch already == main → new `claude/checkpoint-2026-06-05` + draft PR)

rsr-template

Already-good — do NOT touch

Squash message for #234

Checkpoint progress — 2026-06-13

Shipped

Blocked / not possible from this tooling (need owner)

Deferred (entangled — flagged, not done blindly)

Findings flagged (no change made)

Hand-off brief — branch reconciliation + remaining audit (2026-06-13)

A. Branch reconciliation (live data, both repos)

B. Remaining currency audit (horizontal sweep — do in a fresh thread)

C. Owner-only (not doable from agent tooling)

Start-here

Checkpoint closed — done or relegated (2026-06-13)

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

chore(checkpoint): 2026-06-05 repo reconciliation + docs/machine_readable refresh — resume tracker #238

Description

Decisions (owner-confirmed)

Remaining actions

echidna

echidnabot (branch already == main → new claude/checkpoint-2026-06-05 + draft PR)

rsr-template

Already-good — do NOT touch

Squash message for #234

Activity

hyperpolymath commented on Jun 13, 2026

Checkpoint progress — 2026-06-13

Shipped

Blocked / not possible from this tooling (need owner)

Deferred (entangled — flagged, not done blindly)

Findings flagged (no change made)

hyperpolymath commented on Jun 13, 2026

Hand-off brief — branch reconciliation + remaining audit (2026-06-13)

A. Branch reconciliation (live data, both repos)

B. Remaining currency audit (horizontal sweep — do in a fresh thread)

C. Owner-only (not doable from agent tooling)

Start-here

hyperpolymath commented on Jun 13, 2026

Checkpoint closed — done or relegated (2026-06-13)

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions

echidnabot (branch already == main → new `claude/checkpoint-2026-06-05` + draft PR)