Standardise license setup: MPL-2.0 + PMPL-1.0-or-later (REUSE)

- LICENSE: pure MPL-2.0 text for machine detection (GitHub, registries)
- LICENSES/MPL-2.0.txt: standard MPL-2.0 text
- LICENSES/PMPL-1.0-or-later.txt: Palimpsest License text
- NOTICE: explains the dual-license relationship
- Source SPDX headers remain PMPL-1.0-or-later

This ensures OSI compliance checks pass while preserving PMPL as
the governing license for source code.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: hyperpolymath

.bot_directives/echidnabot.scm

@@ -1,7 +1,24 @@
 ;; SPDX-License-Identifier: PMPL-1.0-or-later
 (bot-directive
   (bot "echidnabot")
-  (scope "formal verification and fuzzing")
-  (allow ("analysis" "fuzzing" "proof checks"))
-  (deny ("write to core modules" "write to bindings"))
-  (notes "May open findings; code changes require explicit approval"))
+  (scope "formal verification, proof correspondence, and property-based testing")
+  (languages ("Rust" "Lean4" "Coq" "Agda" "Isabelle" "Mizar"))
+  (targets
+    ("impl/rust-cli/src/" "Rust shell implementation")
+    ("proofs/" "Multi-prover formal proofs")
+    ("impl/rust-cli/tests/" "Correspondence and property tests"))
+  (allow ("analysis" "fuzzing" "proof checks" "property testing" "proof-hole auditing"))
+  (deny ("write to core modules" "write to bindings" "modify proof axioms"))
+  (scanning-rules
+    (rust
+      (ban ("unsafe" "transmute") (unless "// SAFETY: comment present"))
+      (flag ("unwrap" "expect") (severity "medium")))
+    (lean4
+      (ban ("sorry") (severity "critical") (notes "proof holes must be closed"))
+      (flag ("axiom") (severity "high")))
+    (coq
+      (ban ("Admitted") (severity "critical"))
+      (flag ("Axiom") (severity "high")))
+    (agda
+      (ban ("postulate") (severity "critical"))))
+  (notes "May open findings; code changes require explicit approval. Proof hole count must not increase."))

.github/workflows/echidna-validation.yml

@@ -13,6 +13,8 @@ on:
     paths:
       - 'proofs/**'
       - 'impl/rust-cli/**'
+  schedule:
+    - cron: '0 6 * * 1'  # Weekly on Monday at 06:00 UTC
 
 permissions: read-all
 
@@ -22,7 +24,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5  # v4
 
       - name: Install Rust toolchain
         uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7  # stable
@@ -54,7 +56,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5  # v4
 
       - name: Install Rust toolchain
         uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7  # stable

.github/workflows/hypatia-scan.yml

@@ -20,7 +20,7 @@ jobs:
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
         with:
           fetch-depth: 0  # Full history for better pattern analysis