chore(licence): reconcile SPDX headers to the AGPL ruling — three-part split

.clusterfuzzlite/Containerfile

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 FROM gcr.io/oss-fuzz-base/base-builder-rust@sha256:73c1d5648db54100639339d411a5d192cbc8bf413ee91e843a07cf6f0e319dc7
 
 COPY . $SRC/echidna

.clusterfuzzlite/Dockerfile

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 FROM gcr.io/oss-fuzz-base/base-builder-rust@sha256:73c1d5648db54100639339d411a5d192cbc8bf413ee91e843a07cf6f0e319dc7
 
 COPY . $SRC/echidna

.clusterfuzzlite/build.sh

@@ -1,5 +1,5 @@
 #!/bin/bash -eu
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 cd "$SRC"/echidna
 cargo +nightly fuzz build
 # `fuzz` is excluded from the workspace (`Cargo.toml:154-157`), so

.clusterfuzzlite/project.yaml

@@ -1,2 +1,2 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 language: rust

.containerization/Containerfile

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # SPDX-FileCopyrightText: 2024-2025 Jonathan D.A. Jewell <jonathan.jewell@open.ac.uk>
 #
 # ECHIDNA Minimal Containerfile - Multi-stage build for Podman

.containerization/Containerfile.full

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # SPDX-FileCopyrightText: 2024-2025 Jonathan D.A. Jewell <jonathan.jewell@open.ac.uk>
 #
 # ECHIDNA Full Containerfile - Includes a curated prover set
@@ -135,7 +135,7 @@ COPY guix-channel/echidna.scm /channel/echidna/
 
 # If no guix channel file exists, create a stub
 RUN if [ ! -f /channel/echidna/echidna.scm ]; then \
-    printf ';;; SPDX-License-Identifier: MPL-2.0\n\
+    printf ';;; SPDX-License-Identifier: AGPL-3.0-or-later\n\
 (define-module (echidna)\n\
   #:use-module (guix packages)\n\
   #:use-module (guix build-system cargo)\n\

.containerization/Containerfile.mcp

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 #
 # ECHIDNA MCP Container — exposes ECHIDNA as a Model Context Protocol server

.containerization/Containerfile.wave3

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 #
 # ECHIDNA Wave-3 (Tier-3, weekly) prover images — CONSOLIDATED multi-target

.containerization/build.sh

@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # Build ECHIDNA container images using Podman
 set -euo pipefail
 

.echidnabot.toml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # SPDX-FileCopyrightText: 2026 Hyperpolymath
 #
 # echidnabot configuration for echidna
@@ -12,7 +12,7 @@ type = "formal-verification"
 [architecture]
 enforcement_level = "normal"
 primary_language = "rust"    # Core prover backends
-secondary_languages = ["julia", "rescript", "idris2", "chapel", "spark"]
+secondary_languages = ["julia", "affinescript", "idris2", "chapel", "spark"]
 
 [provers]
 # ECHIDNA is self-hosting - can verify its own Idris2 ABI definitions

.editorconfig

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 # EditorConfig helps maintain consistent coding styles

.gitattributes

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # RSR-compliant .gitattributes
 
 * text=auto eol=lf

.githooks/pre-commit

@@ -3,7 +3,7 @@
 # ECHIDNA Pre-commit Hook
 # Enforces npm ban and runs checks
 #
-# SPDX-License-Identifier: MPL-2.0 OR AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 
 set -euo pipefail
 

.githooks/validate-a2ml.sh

@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # validate-a2ml.sh — A2ML manifest validation script

.githooks/validate-k9.sh

@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # validate-k9.sh — K9 configuration file validation script

.github/CODEOWNERS

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # CODEOWNERS - Code ownership for ECHIDNA
 # See https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-code-owners
 

.github/FUNDING.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # Funding platforms for hyperpolymath projects
 # See: https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/displaying-a-sponsor-button-in-your-repository
 

.github/canonical-references/prover-counts.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 #
 # R5 canonical-reference rule: bare prover counts in load-bearing

.github/dependabot.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 version: 2
 updates:
   - package-ecosystem: "cargo"

.github/settings.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 #
 # Repository settings for probot/settings GitHub App.
 # https://github.com/probot/settings

.github/workflows/agda-meta-checker.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # CI workflow for ECHIDNA Agda meta-checker
 # Type-checks all formal proofs verifying trust pipeline correctness

.github/workflows/boj-build.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 name: BoJ Server Build Trigger
 on:

.github/workflows/bridge-gate.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 #

.github/workflows/cargo-audit.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #

.github/workflows/cflite_batch.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 name: ClusterFuzzLite batch fuzzing
 on:

.github/workflows/cflite_pr.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 name: ClusterFuzzLite PR fuzzing
 on:

.github/workflows/chapel-ci.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 name: Chapel Accelerator CI
 

.github/workflows/codeql.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 name: CodeQL Security Analysis
 

.github/workflows/container-ci.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 #
 # container-ci.yml — Container build verification.

.github/workflows/dogfood-gate.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #

.github/workflows/dogfood-proofs-ci.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # Gates the ECHIDNA dogfood proof corpus: every theorem under proofs/{coq,lean,agda}
 # must type-check. These proofs had no CI coverage before this workflow -- the other

.github/workflows/formal-verification.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #

.github/workflows/generator-generic-ossf-slsa3-publish.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # This workflow uses actions that are not certified by GitHub.
 # They are provided by a third-party and are governed by

.github/workflows/ghcr-publish.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 name: Publish to GHCR
 

.github/workflows/governance.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 name: Governance
 

.github/workflows/hypatia-scan.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 name: Hypatia Security Scan
 

.github/workflows/idris2-abi-ci.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 name: Idris2 ABI Type-Check
 

.github/workflows/live-provers.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # ECHIDNA — Live-Prover CI
 #

.github/workflows/mirror.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 name: Mirror to Git Forges
 

.github/workflows/mvp-smoke.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 name: MVP Smoke (Best Effort)
 

.github/workflows/rust-ci.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # Rust CI — thin wrapper calling the shared estate reusable in
 # hyperpolymath/standards. Configure once, propagate everywhere.

.github/workflows/s4-loop.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # S4 loop-closure CI — brings up verisim-api as a service container and
 # runs the echidna s4_loop_closure integration test.  Filed once

.github/workflows/scorecard.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 name: OSSF Scorecard
 

.github/workflows/secret-scanner.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 name: Secret Scanner
 

.github/workflows/security-scan.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 
 name: Security Scan

.github/workflows/server-boot-gate.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # Server boot gate — builds the echidna binary, boots the server, and
 # verifies that /api/health, /api/provers, and a session {id} route all

.github/workflows/spark-theatre-gate.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # Estate SPARK Theatre Gate — thin caller of the reusable workflow in
 # hyperpolymath/standards (#135 / #141). Pinned by commit SHA per the

.github/workflows/verification-proofs-cron.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # Weekly verification of the heavier self-proof corpora that are too slow and too
 # network-heavy to gate on every PR: currently Isabelle/HOL (proofs/isabelle). The

.github/workflows/workflow-linter.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # This workflow is managed by gh actions-lock.
 # Prevention workflow - validates all workflows have proper security config
 name: Workflow Security Linter

.gitignore

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # RSR-compliant .gitignore
 
 # OS & Editor

.gitlab-ci.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # SPDX-FileCopyrightText: 2024-2025 ECHIDNA Project Contributors
 #
 # ECHIDNA GitLab CI/CD Pipeline
@@ -100,17 +100,6 @@ build-julia:
       - .julia/
     expire_in: 1 day
 
-build-rescript:
-  stage: build
-  image: docker.io/denoland/deno:debian-1.40.0
-  script:
-    - cd src/rescript
-    - deno task build || echo "ReScript build completed with warnings"
-  artifacts:
-    paths:
-      - src/rescript/dist/
-    expire_in: 1 day
-  allow_failure: true
 
 build-container:
   stage: build

.guix-channel

@@ -1,4 +1,4 @@
-;; SPDX-License-Identifier: MPL-2.0
+;; SPDX-License-Identifier: AGPL-3.0-or-later
 ;; Guix channel definition for ECHIDNA
 (channel
   (version 0)

.machine_readable/contractiles/README.adoc

@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: MPL-2.0
+// SPDX-License-Identifier: CC-BY-SA-4.0
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 = Echidna Contractiles
 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>

.pre-commit-config.yaml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # Pre-commit hooks for hyperpolymath RSR repos.
 # Install: pip install pre-commit && pre-commit install
 # Run manually: pre-commit run --all-files