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"
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"
 
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