diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 98ae8ef..2b15764 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -43,17 +43,13 @@ jobs:
     steps:
       - name: Install the pinned Debian toolchain
         run: |
-          set -euo pipefail
-          curl -fsSL -o "$RUNNER_TEMP/agda.tar.xz" \
-            https://github.com/agda/agda/releases/download/v2.7.0.1/Agda-v2.7.0.1-linux.tar.xz
-          echo "${AGDA_SHA256}  $RUNNER_TEMP/agda.tar.xz" | sha256sum --check
-          tar -xJf "$RUNNER_TEMP/agda.tar.xz" -C "$RUNNER_TEMP"
-          echo "Agda_datadir=$RUNNER_TEMP/Agda-v2.7.0.1/data" >> "$GITHUB_ENV"
-          echo "AGDA_BIN=$RUNNER_TEMP/Agda-v2.7.0.1/bin/agda" >> "$GITHUB_ENV"
-      - name: Type-check and axiom audit
-        run: proofs/bootstrap.sh
-      - name: Gate self-test (the gate must reject planted defects)
-        run: proofs/tests/gate-selftest.sh
+          apt-get update
+          apt-get install --no-install-recommends -y ca-certificates git agda-bin=2.6.4.3-1+b2 agda-stdlib=2.1-4
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
+        with:
+          persist-credentials: false
+      - name: Proof gate (axiom audit, type-check, reject controls, gate self-test)
+        run: proofs/check.sh
   oracle:
     name: R reference oracle (R 4.5.0, Bioconductor 3.22)
     runs-on: ubuntu-24.04
@@ -82,11 +78,20 @@ jobs:
         with:
           version: '1.12'
       - uses: julia-actions/cache@d10a6fd8f31b12404a54613ebad242900567f2b9 # v2
-      - name: Native vs reference agreement
+      # RCall.jl's own CI does the same: libR's directory must be on the loader path.
+      - name: Put libR on the loader path
+        run: echo "LD_LIBRARY_PATH=$(R RHOME)/lib${LD_LIBRARY_PATH:+:$LD_LIBRARY_PATH}" >> "$GITHUB_ENV"
+      - name: R can load ALDEx2
+        run: Rscript -e 'library(ALDEx2); cat(R.version.string, "ALDEx2", as.character(packageVersion("ALDEx2")), "\n")'
+      - name: Julia can start R through RCall
         run: |
           export R_HOME="$(R RHOME)"
-          # Skip Pkg's bulk precompile: it reports a failed extension without its error.
-          # Loading directly below surfaces the real error if there is one.
+          echo "R_HOME=$R_HOME"
           JULIA_PKG_PRECOMPILE_AUTO=0 julia --project=test/oracle -e 'using Pkg; Pkg.develop(path="."); Pkg.instantiate()'
-          julia --project=test/oracle -e 'using CompositionalDA, RCall; @assert Base.get_extension(CompositionalDA, :CompositionalDARCallExt) !== nothing'
+          for l in ~/.julia/scratchspaces/*/*/build.log; do echo "== $l"; cat "$l"; done
+          julia --project=test/oracle -e 'using RCall; println(rcopy(R"R.version.string"))'
+          julia --project=test/oracle -e 'using CompositionalDA, RCall; @assert Base.get_extension(CompositionalDA, :CompositionalDARCallExt) !== nothing; println("extension loaded")'
+      - name: Native vs reference agreement
+        run: |
+          export R_HOME="$(R RHOME)"
           julia --project=test/oracle test/oracle/runoracle.jl