fix(licence): project licence is AGPL-3.0-or-later — align LICENSE, badges, manifests (#312)

hyperpolymath · claude · web-flow · commit aff0319e2186 · 2026-07-07T11:09:35.000+01:00
## Owner decision (2026-07-07) The Governance **Licence consistency** gate has been red on main: `LICENSE` carried MPL-2.0 text while `Cargo.toml` — and 6 of 9 workspace crates — already declared `AGPL-3.0-or-later`. Owner ruled **AGPL**. ## Changes - `LICENSE` → verbatim GNU AGPL-3.0 text with an `SPDX-License-Identifier: AGPL-3.0-or-later` header. (The gate script establishes identity from the SPDX header; AGPL isn't in its body-template table, so the header is load-bearing — body then correctly WARNs 'manual review' without failing.) - `LICENSES/AGPL-3.0-or-later.txt` added (REUSE). - The three lagging interface crates (`grpc`/`graphql`/`rest`) aligned from MPL-2.0 to AGPL-3.0-or-later. - `guix.scm` licence field → `license:agpl3+` (was a palimpsest non-copyleft stub commented "MPL-2.0"). - README badge + licence section + BibTeX, CLAUDE.md licence lines. Documentation keeps its MPL-2.0/CC-BY-SA headers (intentional doc stance); the per-file source-header migration (thousands of MPL-2.0 SPDX lines) remains the owner-managed sweep and is called out in prose. ## Verification Ran the actual gate script (`standards/scripts/check-licence-consistency.sh`) against this tree: ``` [OK] SPDX header: AGPL-3.0-or-later [OK] Manifest licence (Cargo.toml): AGPL-3.0-or-later [OK] Licence identity matches manifest declaration. [OK] Licence consistency check passed. ``` REUSE lint findings are unchanged pre-existing debt (missing CC0/MIT/PMPL texts predate this PR). Closes the licence half of the Governance red; the other half (Validate Hypatia Baseline) is tracked separately. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
diff --git a/CLAUDE.md b/CLAUDE.md
@@ -8,7 +8,7 @@ Guidelines and context for working with Claude Code on the ECHIDNA project.
 
 - **Repository**: https://github.com/hyperpolymath/echidna
 - **Version + release history**: [`CHANGELOG.md`](CHANGELOG.md) (single source of truth; do not duplicate version strings elsewhere)
-- **License**: MPL-2.0
+- **License**: AGPL-3.0-or-later (owner decision 2026-07-07; per-file MPL-2.0 headers pending migration sweep)
 - **Architecture overview**: [`docs/ARCHITECTURE.md`](docs/ARCHITECTURE.md)
 - **Canonical prover count + tier table**: [`docs/PROVER_COUNT.md`](docs/PROVER_COUNT.md)
 - **Environment variables**: [`docs/ENV-VARS.md`](docs/ENV-VARS.md)
@@ -205,7 +205,7 @@ in `.github/workflows/`:
 - **RSR / CCCP compliance** — see [`RSR_COMPLIANCE.adoc`](RSR_COMPLIANCE.adoc) for the full hard-rule list and out-of-template adaptations.
 - **Justfile primary** (RSR-H14) — Just is the build entry point; no Make.
 - **Podman not Docker** (RSR-H15) — always Podman; `Containerfile` (not `Dockerfile`); `.containerization/Containerfile.wave3` for per-prover images.
-- **License**: MPL-2.0 across the documentation surface (intentional doc stance; see [`feedback_echidna_license_docs_mpl_intentional`](https://github.com/hyperpolymath/echidna/issues?q=license) — historical drift on individual files is owner-managed and not reconciled in routine PRs).
+- **License**: project licence is AGPL-3.0-or-later (owner decision 2026-07-07, matching `Cargo.toml`); documentation surface keeps its MPL-2.0 headers (intentional doc stance; see [`feedback_echidna_license_docs_mpl_intentional`](https://github.com/hyperpolymath/echidna/issues?q=license) — per-file header drift is owner-managed and not reconciled in routine PRs).
 - **Author**: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>.
 
 ---
diff --git a/LICENSE b/LICENSE
diff --git a/LICENSES/AGPL-3.0-or-later.txt b/LICENSES/AGPL-3.0-or-later.txt
diff --git a/README.md b/README.md
@@ -4,7 +4,7 @@ SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 
 [![OpenSSF Best Practices](https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity)](https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/echidna)
-[![License: MPL-2.0](https://img.shields.io/badge/License-MPL--2.0-blue.svg)](LICENSE) [![Green Hosting](https://api.thegreenwebfoundation.org/greencheckimage/nesy-prover.dev)](https://www.thegreenwebfoundation.org/green-web-check/?url=nesy-prover.dev)
+[![License: AGPL-3.0-or-later](https://img.shields.io/badge/License-AGPL--3.0--or--later-blue.svg)](LICENSE) [![Green Hosting](https://api.thegreenwebfoundation.org/greencheckimage/nesy-prover.dev)](https://www.thegreenwebfoundation.org/green-web-check/?url=nesy-prover.dev)
 
 \*E\*xtensible \*C\*ognitive \*H\*ybrid \*I\*ntelligence for
 \*D\*eductive \*N\*eural \*A\*ssistance
@@ -611,12 +611,13 @@ Headline shape (as of the most recent on-main work):
 - **Podman not Docker** — always Podman; `Containerfile`
   (`.containerization/` for the per-prover images) not `Dockerfile`.
 
-- **License**: MPL-2.0 (source files). See LICENSE.
+- **License**: AGPL-3.0-or-later. See LICENSE.
 
 # License
 
-This project is licensed under the [Mozilla Public License
-2.0](LICENSE).
+This project is licensed under the [GNU Affero General Public License
+v3.0 or later](LICENSE). Individual files may carry earlier MPL-2.0
+SPDX headers pending the header migration sweep.
 
 # Citation
 
@@ -626,7 +627,7 @@ This project is licensed under the [Mozilla Public License
   author = {Jewell, Jonathan D.A.},
   year = {2026},
   url = {https://github.com/hyperpolymath/echidna},
-  license = {MPL-2.0}
+  license = {AGPL-3.0-or-later}
 }
 ```
 
diff --git a/guix.scm b/guix.scm
@@ -84,8 +84,7 @@ supports 30 prover backends including Agda, Coq, Lean 4, Isabelle, Z3, CVC5,
 and more, with a comprehensive verification pipeline featuring solver integrity
 checking, proof certificate validation, axiom tracking, and confidence scoring.")
     (home-page "https://github.com/hyperpolymath/echidna")
-    (license (license:non-copyleft "https://github.com/hyperpolymath/palimpsest-license"
-                                   #:comment "MPL-2.0"))))
+    (license license:agpl3+)))
 
 ;; For development shell
 echidna
diff --git a/src/interfaces/graphql/Cargo.toml b/src/interfaces/graphql/Cargo.toml
@@ -5,7 +5,7 @@ name = "echidna-graphql"
 version = "0.1.0"
 edition = "2021"
 authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
-license = "MPL-2.0"
+license = "AGPL-3.0-or-later"
 description = "GraphQL interface for ECHIDNA theorem proving platform"
 repository = "https://github.com/hyperpolymath/echidna-graphql"
 readme = "README.adoc"
diff --git a/src/interfaces/grpc/Cargo.toml b/src/interfaces/grpc/Cargo.toml
@@ -5,7 +5,7 @@ name = "echidna-grpc"
 version = "0.1.0"
 edition = "2021"
 authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
-license = "MPL-2.0"
+license = "AGPL-3.0-or-later"
 description = "gRPC interface for ECHIDNA theorem proving platform"
 repository = "https://github.com/hyperpolymath/echidna-grpc"
 readme = "README.adoc"
diff --git a/src/interfaces/rest/Cargo.toml b/src/interfaces/rest/Cargo.toml
@@ -5,7 +5,7 @@ name = "echidna-rest"
 version = "0.1.0"
 edition = "2021"
 authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
-license = "MPL-2.0"
+license = "AGPL-3.0-or-later"
 description = "REST API for ECHIDNA theorem proving platform"
 publish = false
 
