chore(licence): normalise to MPL-2.0 + CC-BY-SA-4.0 (canonical pair)

.github/copilot-instructions.md

@@ -1,5 +1,5 @@
 <!--
-SPDX-License-Identifier: MPL-2.0
+SPDX-License-Identifier: CC-BY-SA-4.0
 Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 ## Code Review Guidelines

.github/workflows/scorecard.yml

@@ -1,5 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
-# SPDX-License-Identifier: CC-BY-SA-4.0
+# SPDX-License-Identifier: MPL-2.0
 name: Scorecards supply-chain security
 on:
   branch_protection_rule:

.github/workflows/secret-scanner.yml

@@ -1,5 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
-# SPDX-License-Identifier: CC-BY-SA-4.0
+# SPDX-License-Identifier: MPL-2.0
 name: Secret Scanner
 on:
   pull_request:

.machine_readable/licensing-policy.toml

@@ -1,5 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
-# SPDX-License-Identifier: CC-BY-SA-4.0
+# SPDX-License-Identifier: MPL-2.0
 # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
 #
 # Machine-readable form of LICENSING.adoc. Tools enforce from this; humans read

CHANGELOG.md

@@ -1,5 +1,5 @@
 <!--
-SPDX-License-Identifier: MPL-2.0
+SPDX-License-Identifier: CC-BY-SA-4.0
 Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 # Changelog

CODE_OF_CONDUCT.md

@@ -1,5 +1,5 @@
 <!--
-SPDX-License-Identifier: MPL-2.0
+SPDX-License-Identifier: CC-BY-SA-4.0
 Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 # Code of Conduct

CONTRIBUTING.md

@@ -1,5 +1,5 @@
 <!--
-SPDX-License-Identifier: MPL-2.0
+SPDX-License-Identifier: CC-BY-SA-4.0
 Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 # Contributing to Phronesis

LICENSE

@@ -35,7 +35,7 @@ Mozilla Public License Version 2.0
     means any form of the work other than Source Code Form.
 
 1.7. "Larger Work"
-    means a work that combines Covered Software with other material, in
+    means a work that combines Covered Software with other material, in 
     a separate file or files, that is not Covered Software.
 
 1.8. "License"
@@ -357,7 +357,7 @@ Exhibit A - Source Code Form License Notice
 
   This Source Code Form is subject to the terms of the Mozilla Public
   License, v. 2.0. If a copy of the MPL was not distributed with this
-  file, You can obtain one at https://mozilla.org/MPL/2.0/.
+  file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
 If it is not possible or desirable to put the notice in a particular
 file, then You may include the notice in a location (such as a LICENSE

LICENSING.adoc

@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: MPL-2.0
+// SPDX-License-Identifier: CC-BY-SA-4.0
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = Phronesis — Licensing
@@ -20,7 +20,7 @@ syntax:
 
 [source]
 ----
-SPDX-License-Identifier: MPL-2.0
+SPDX-License-Identifier: CC-BY-SA-4.0
 SPDX-License-Identifier: CC-BY-SA-4.0
 ----
 

SECURITY.md

@@ -1,5 +1,5 @@
 <!--
-SPDX-License-Identifier: MPL-2.0
+SPDX-License-Identifier: CC-BY-SA-4.0
 Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 # Security Policy

academic/formal-verification/agda/Phronesis.agda

@@ -1,5 +1,5 @@
 -- SPDX-License-Identifier: MPL-2.0
--- SPDX-License-Identifier: CC-BY-SA-4.0
+-- SPDX-License-Identifier: MPL-2.0
 -- Phronesis Formalization in Agda
 -- Intrinsically typed representation with dependent types
 

academic/formal-verification/agda/PhronesisEcho.agda

@@ -1,5 +1,5 @@
 -- SPDX-License-Identifier: MPL-2.0
--- SPDX-License-Identifier: CC-BY-SA-4.0
+-- SPDX-License-Identifier: MPL-2.0
 -- Copyright (c) 2026 Jonathan D.A. Jewell
 --
 -- =====================================================================

academic/formal-verification/coq/Phronesis.v

@@ -1,5 +1,5 @@
 (* SPDX-License-Identifier: MPL-2.0 *)
-(* SPDX-License-Identifier: CC-BY-SA-4.0 *)
+(* SPDX-License-Identifier: MPL-2.0 *)
 (* Phronesis Formalization in Coq *)
 (* Complete mechanized proofs of type safety, termination, and security properties *)
 

academic/formal-verification/lean4/Phronesis.lean

@@ -1,5 +1,5 @@
 -- SPDX-License-Identifier: MPL-2.0
--- SPDX-License-Identifier: CC-BY-SA-4.0
+-- SPDX-License-Identifier: MPL-2.0
 -- Phronesis Formalization in Lean 4
 -- Mechanized proofs of type safety, termination, and security properties.
 --

academic/formal-verification/lean4/lakefile.lean

@@ -1,5 +1,5 @@
 -- SPDX-License-Identifier: MPL-2.0
--- SPDX-License-Identifier: CC-BY-SA-4.0
+-- SPDX-License-Identifier: MPL-2.0
 -- Minimal Lake build for the Phronesis Lean 4 metatheory.
 -- No external dependencies (no Mathlib): builds on core Lean only, so CI
 -- needs nothing but the toolchain pinned in `lean-toolchain`.