ci(proofs): audit the proof ledger, reconcile the local ruling with the estate policy, and stop the record lying

.github/workflows/actions.lock

@@ -32,6 +32,9 @@ workflows:
         - 'actions/checkout@v7.0.1'
         - 'actions/deploy-pages@v5.0.1'
         - 'actions/upload-pages-artifact@v5.0.0'
+    '.github/workflows/proof-ci.yml':
+        - 'actions/checkout@v7.0.1'
+        - 'actions/upload-artifact@v7.0.2'
     '.github/workflows/push-email-notify.yml':
         - 'hyperpolymath/smtp-notify-action@v0.5.0'
     '.github/workflows/quality.yml':

.github/workflows/workflow-linter.yml

@@ -70,9 +70,18 @@
           XDG_DATA_HOME: ${{ runner.temp }}/workflow-linter-data
         run: |
           # Binary extensions accept release tags, not source commit pins.
-          # Verify the v0.1.6 linux-amd64 release bytes before executing them.
-          gh release download v0.1.6 --repo github/gh-actions-lock --pattern linux-amd64 --output "$RUNNER_TEMP/gh-actions-lock"
-          echo "4181ec1da5408b34b9a542a7ee5c6ce3a4d6ac815c7d0206a00ceca8a817f4e3  $RUNNER_TEMP/gh-actions-lock" | sha256sum --check --strict
+          # Verify the v0.4.0 linux-amd64 release bytes before executing them.
+          #
+          # v0.4.0 bundles actions-lockfile go v0.0.6, which reads lockfile
+          # v0.0.3 — the version the current tool writes. The v0.1.6 binary
+          # pinned here before bundled go v0.0.4 and caps out at lockfile
+          # v0.0.2, so it aborted with "lockfile version v0.0.3 is newer than
+          # this binary supports" as soon as anything wrote the lock with a
+          # current release. That is a tool-version gate, not a finding about
+          # our pins: the pin has to track the schema the estate writes, or
+          # this step reports red on a perfectly covered lockfile.
+          gh release download v0.4.0 --repo github/gh-actions-lock --pattern linux-amd64 --output "$RUNNER_TEMP/gh-actions-lock"
+          echo "f9da98f2a6e9e0ae77deadf9a2319a8a86bb002b541cc3203b247cc59fb04842  $RUNNER_TEMP/gh-actions-lock" | sha256sum --check --strict
           chmod +x "$RUNNER_TEMP/gh-actions-lock"
           "$RUNNER_TEMP/gh-actions-lock" --verify-local
 
@@ -81,7 +90,7 @@
           echo "=== Checking for Duplicates ==="
           # Known duplicate patterns
           if [ -f .github/workflows/codeql.yml ] && [ -f .github/workflows/codeql-analysis.yml ]; then
             echo "ERROR: Duplicate CodeQL workflows found"
             echo "Delete codeql-analysis.yml (keep codeql.yml)"
             exit 1
           fi

.machine_readable/bot_directives/placement.a2ml

@@ -76,6 +76,11 @@ allowed-proofs = [
   "verification/proofs/agda/Verification.agda", # aggregator that typechecks the cross-project set
   "verification/proofs/agda/nextgen-typing.agda-lib",
 ]
+enforced-by = [
+  "just proof-enrolment (scripts/check-proof-enrolment.sh) -- FAILs when a proof is unlisted, when a registered entry has no file behind it, when this list and ALLOWED_PROOFS in scripts/check-coordination-boundary.sh disagree, or when zero proofs are enrolled; BLOCKED (exit 2) when a required prover is missing",
+  "just proof-scan-dangerous (scripts/proof-scan-dangerous.sh) -- FAILs on believe_me/assert_total/postulate/sorry/Admitted/unsafeCoerce/Obj.magic outside comments",
+  ".github/workflows/proof-ci.yml -- runs `just proof-witness-check` (audit verification/proofs/LEDGER.json, then compile every declared Rocq/Lean recheck leg) plus the both-ways instrument controls, on proof, ledger, manifest, tests/proofs, Justfile and workflow changes; a green run means the ledger is honest, NOT that XP-1 is verified in an independent kernel",
+]
 route-elsewhere = [
   "ABI/FFI/memory-layout proofs -> typed-wasm",
   "TypeLL kernel proofs -> typell",

.machine_readable/descriptiles/NEUROSYM.a2ml

@@ -3,15 +3,23 @@
 #
 # NEUROSYM.a2ml — Neurosymbolic integration metadata
 # Configuration for Hypatia scanning and symbolic reasoning.
+#
+# Local divergence from the fleet template written by gitbot-fleet
+# (robot-repo-automaton/templates/skeleton/): that template still says
+# report-format = "logtalk", removed as a Hypatia format on 2026-04-14.
+# Reported upstream: https://github.com/hyperpolymath/gitbot-fleet/issues/641
 
 [metadata]
-version = "0.1.0"
-last-updated = "2026-06-12"
+version = "0.2.0"
+last-updated = "2026-11-01"
 
 [hypatia-config]
 scan-enabled = true
 scan-depth = "standard"  # quick | standard | deep
-report-format = "logtalk"
+# JSON AssailReport from panic-attack. Logtalk was removed as a report format on
+# 2026-04-14 (hypatia .machine_readable/descriptiles/NEUROSYM.a2ml); the "logtalk"
+# value that shipped in the fleet template is dead and this repo emits no .lgt.
+report-format = "json"
 
 [symbolic-rules]
 # Custom symbolic rules for this project

.machine_readable/integrations/verisimdb.a2ml

@@ -2,16 +2,29 @@
 # OPTIONAL: VeriSimDB Feed — Cross-Repo Analytics Data Store
 # Delete this file if your project does not feed data to VeriSimDB.
 # See https://github.com/hyperpolymath/nextgen-databases for details.
+#
+# Local divergence from the fleet template written by gitbot-fleet's
+# scripts/fix-missing-verisim-feed.sh: that template says format = "hexad" and
+# destination = "verisim-data/feeds/", neither of which exists in VeriSimDB.
+# Reported upstream: https://github.com/hyperpolymath/gitbot-fleet/issues/640
 
 [integration]
 name = "verisimdb"
 type = "data-feed"
-repository = "https://github.com/hyperpolymath/nextgen-databases"
+# The engine is verisimdb; nextgen-databases is only the research parent.
+repository = "https://github.com/hyperpolymath/verisimdb"
+parent = "https://github.com/hyperpolymath/nextgen-databases"
 data-store = "verisimdb-data"
 
 [feed-config]
 emit-scan-results = true
 emit-build-metrics = true
 emit-dependency-graph = true
-format = "hexad"
-destination = "verisimdb-data/feeds/"
+# The record schema is the octad (8 modal witnesses). "HEXAD" is a LEGACY VCL
+# keyword for the octad source, kept in verisimdb's surface grammar v3.0 for
+# backward compatibility — it is a query keyword, not a wire format. Records
+# carry "schema": "verisimdb.octad.v1" (see verisimdb-data scans/octads/).
+format = "verisimdb.octad.v1"
+# The store's layout (verisimdb-data README): scans/ holds per-repo results and
+# scans/octads/ holds octad records. There is no feeds/ directory.
+destination = "verisimdb-data/scans/octads/"

.trusted-base-ignore

@@ -0,0 +1,12 @@
+# Comments start with `#`.
+# Each non-comment line is a path-fragment substring match against the
+# repo-relative file path. Narrow the fragment to avoid hiding adjacent
+# findings.
+#
+# Scanner test fixtures: exist solely to verify the detector fires.
+# tests/proofs/control/PlantedAdmitted.v and PlantedSorry.lean contain a real
+# `Admitted` and a real `sorry` on purpose. The instrument must reject them —
+# tests/proofs/run-controls.sh asserts that it does — so documenting them as
+# debt would be wrong twice: they are not soundness holes in this repository,
+# and the whole point is that they stay detectable.
+tests/proofs/control/

CLAUDE.md

@@ -49,7 +49,7 @@ katagoria → typell → typed-wasm → PanLL      (TypeFix Zero / μType₀ sit
 | TypeFix Zero / μType₀ calibration calculus | `typefix-zero` |
 | AffineScript / Ephapax language code | `affinescript` · `ephapax` |
 | Query-language type safety (SQL/GraphQL/Cypher/SPARQL/VQL) | `typedqliser` · `vcl-ut` |
-| Tropical / semiring type theory (Isabelle/Lean) | `tropical-resource-typing` |
+| Tropical / semiring type theory (Isabelle/Lean) | `tropical-types` (renamed from `tropical-resource-typing`, 2026-09-09) |
 | Transport-adapter / max-plus pathfinding | `protocol-squisher` |
 | Any compiler/app code, single-project ABI/FFI, benchmarks, or tests | the owning project repo |
 
@@ -61,6 +61,30 @@ The machine-readable form of this table is the source of truth:
 `.machine_readable/bot_directives/placement.a2ml`. It is enforced in CI by
 `.github/workflows/coordination-boundary.yml`.
 
+## Proofs and verification
+
+The normative policy is *outside* this repository:
+`3-practice/PROOF-POLICY.adoc` in `metadatastician/standards`, owner ruling
+2026-10-26, amended 2026-11-01, pinned at commit
+`46ee18323305d5b36e2eef936e47dd54c39ea736`. It is referenced, not vendored — a
+bare path is a dangling citation, so name the commit or the URL.
+
+It decides *where* a proof lives: theory → **Agda**, rechecked in **Rocq and
+Lean** (§2, with the canonical invocation in §2.1); engineering/ABI → **Idris2**;
+Rust → Creusot, Ada → SPARK. A gate that enforces it must be verified **both
+ways** (§7): it passes conforming input *and* fails a planted violation.
+
+Status lives in `verification/proofs/LEDGER.json`, never in prose:
+
+```bash
+just proof-witness-check        # CI target: registry gates + ledger audit + declared recheck legs
+just proof-grade                # the grade ladder and the delta to the next rung
+bash tests/proofs/run-controls.sh   # the §7 controls (ledger-form + kernel)
+```
+
+A missing prover is **BLOCKED**, never a skip. `docs/decisions/` records the
+local rulings where they differ from the policy, including what was superseded.
+
 ## After the boundary, follow the estate conventions
 
 1. Read `0-AI-MANIFEST.a2ml`, then `.machine_readable/descriptiles/STATE.a2ml`.