From 3b81c7e79874809a9d2f6ac7bb07d183f36d34e7 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:03:30 +0000
Subject: [PATCH 1/3] proofs(agda): enforce full safe/cubical-compatible mode
 in Justfile

---
 Justfile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Justfile b/Justfile
index 6b82224c..7e05062e 100644
--- a/Justfile
+++ b/Justfile
@@ -275,8 +275,8 @@ proofs-agda:
     export LC_ALL="${LC_ALL:-C.UTF-8}"
     cd proofs/agda
     for f in $(find . -name '*.agda' -not -path './_build/*' -not -path './dist-newstyle/*' | sort); do
-        echo "agda $f"
-        agda "$f"
+        echo "agda --safe --without-K --cubical-compatible $f"
+        agda --safe --without-K --cubical-compatible "$f"
     done
     echo "Agda corpus: all files type-check"
 

From 7814ebd20094cc41a2e9062f56c853328ea72cc9 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:03:33 +0000
Subject: [PATCH 2/3] proofs(agda): enforce full safe/cubical-compatible mode
 in scripts/test-proofs.sh

---
 scripts/test-proofs.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/test-proofs.sh b/scripts/test-proofs.sh
index 28b2bc36..d7c1c2f4 100755
--- a/scripts/test-proofs.sh
+++ b/scripts/test-proofs.sh
@@ -84,7 +84,7 @@ test_agda() {
         local filename=$(basename "$file")
         log_info "Testing $filename..."
 
-        if agda --safe "$file" &> /dev/null; then
+        if agda --safe --without-K --cubical-compatible "$file" &> /dev/null; then
             log_success "$filename"
             PASSED_TESTS=$((PASSED_TESTS + 1))
         else

From 59d124d92bf72724a5cd57329c887dc6796fe149 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:03:36 +0000
Subject: [PATCH 3/3] proofs(agda): enforce full safe/cubical-compatible mode
 in .github/workflows/agda-meta-checker.yml

---
 .github/workflows/agda-meta-checker.yml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/agda-meta-checker.yml b/.github/workflows/agda-meta-checker.yml
index 8ecd16d3..68c1ebc8 100644
--- a/.github/workflows/agda-meta-checker.yml
+++ b/.github/workflows/agda-meta-checker.yml
@@ -47,7 +47,7 @@ jobs:
           GH_TOKEN: ${{ github.token }}
         run: |
           set -euo pipefail
-          PATTERN='^meta-checker/'
+          PATTERN='^(meta-checker/|\.github/workflows/agda-meta-checker\.yml$)'
           if [ "${{ github.event_name }}" = "pull_request" ]; then
             FILES=$(gh api "repos/${{ github.repository }}/pulls/${{ github.event.pull_request.number }}/files" \
                       --paginate --jq '.[].filename')
@@ -103,5 +103,5 @@ jobs:
         run: |
           cd meta-checker
           echo "$PWD/echidna-meta.agda-lib" >> ~/.agda/libraries
-          agda src/Echidna/MetaChecker.agda
-          echo "✓ All 30+ properties machine-verified"
+          agda --safe --without-K --cubical-compatible src/Echidna/MetaChecker.agda
+          echo "✓ Meta-checker passed with safe / without-K / cubical-compatible; proof assumptions require a separate audit"