chore(licence): AGPL-3.0-or-later -> MPL-2.0 code, CC-BY-SA-4.0 docs …

.clusterfuzzlite/Containerfile

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

.clusterfuzzlite/Dockerfile

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 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: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 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: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 language: rust

.containerization/Containerfile

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # 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: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # 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: AGPL-3.0-or-later\n\
+    printf ';;; SPDX-License-Identifier: MPL-2.0\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: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # 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: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # 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: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # Build ECHIDNA container images using Podman
 set -euo pipefail
 

.echidnabot.toml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # SPDX-FileCopyrightText: 2026 Hyperpolymath
 #
 # echidnabot configuration for echidna

.editorconfig

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # 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: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # RSR-compliant .gitattributes
 
 * text=auto eol=lf

.github/CODEOWNERS

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # 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: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # 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: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # 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: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 version: 2
 updates:
   - package-ecosystem: "cargo"

.github/hooks/validate-a2ml.sh

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

.github/hooks/validate-k9.sh

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

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

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

.github/workflows/boj-build.yml

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

.github/workflows/bridge-gate.yml

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

.github/workflows/cargo-audit.yml

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

.github/workflows/cflite_batch.yml

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

.github/workflows/cflite_pr.yml

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

.github/workflows/chapel-ci.yml

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

.github/workflows/codeql.yml

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

.github/workflows/container-ci.yml

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

.github/workflows/dogfood-gate.yml

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

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

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

.github/workflows/formal-verification.yml

@@ -1,5 +1,5 @@
 # This workflow is managed by gh actions-lock.
-# SPDX-License-Identifier: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # 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,5 +1,5 @@
 # This workflow is managed by gh actions-lock.
-# SPDX-License-Identifier: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.

.github/workflows/ghcr-publish.yml

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

.github/workflows/governance.yml

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

.github/workflows/hypatia-scan.yml

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

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

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

.github/workflows/live-provers.yml

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

.github/workflows/mirror.yml

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

.github/workflows/mvp-smoke.yml

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

.github/workflows/pages.yml

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

.github/workflows/proof-safety.yml

@@ -1,5 +1,5 @@
 # This workflow is managed by gh actions-lock.
-# SPDX-License-Identifier: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # This workflow is managed by gh actions-lock.
 name: Proof Safety
 on:

.github/workflows/rust-ci.yml

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

.github/workflows/s4-loop.yml

@@ -1,5 +1,5 @@
 # This workflow is managed by gh actions-lock.
-# SPDX-License-Identifier: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # 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,5 +1,5 @@
 # This workflow is managed by gh actions-lock.
-# SPDX-License-Identifier: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.

.github/workflows/secret-scanner.yml

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

.github/workflows/security-scan.yml

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

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

@@ -1,5 +1,5 @@
 # This workflow is managed by gh actions-lock.
-# SPDX-License-Identifier: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # 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,5 +1,5 @@
 # This workflow is managed by gh actions-lock.
-# SPDX-License-Identifier: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.

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

@@ -1,5 +1,5 @@
 # This workflow is managed by gh actions-lock.
-# SPDX-License-Identifier: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # 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,5 +1,5 @@
 # This workflow is managed by gh actions-lock.
-# SPDX-License-Identifier: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # 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: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # RSR-compliant .gitignore
 
 # OS & Editor

.gitlab-ci.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: AGPL-3.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # SPDX-FileCopyrightText: 2024-2025 ECHIDNA Project Contributors
 #
 # ECHIDNA GitLab CI/CD Pipeline

.guix-channel

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

.machine_readable/contractiles/_base.ncl

@@ -1,5 +1,4 @@
 # SPDX-License-Identifier: MPL-2.0
-# (MPL-2.0 is automatic legal fallback until PMPL is formally recognised)
 #
 # _base.ncl — Shared contractile base
 #

.pre-commit-config.yaml

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