diff --git a/.github/workflows/bench-main.yml b/.github/workflows/bench-main.yml
index 957b51b3..f117a815 100644
--- a/.github/workflows/bench-main.yml
+++ b/.github/workflows/bench-main.yml
@@ -28,7 +28,7 @@ jobs:
   build:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
       # Pinned Rust toolchain + cargo cache (~/.cargo + target/, via the action's
       # built-in rust-cache), so `lake build`'s cargo step doesn't recompile the
       # Plonky3/multi-stark deps from scratch on every run.
@@ -54,7 +54,7 @@ jobs:
           lake build bench-typecheck
           cp .lake/build/bin/bench-typecheck ~/.local/bin/bench-typecheck
           chmod +x ~/.local/bin/bench-typecheck
-      - uses: actions/cache/save@v5
+      - uses: actions/cache/save@v6
         with:
           path: ~/.local/bin
           key: aiur-bench-bins-${{ github.sha }}
@@ -78,11 +78,11 @@ jobs:
           #   cache_pkg: formal_conjectures
           #   mathlib: true
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
         with:
           fetch-depth: 0
           fetch-tags: true   # bencher-track reads the bencher-thresholds-reset tag
-      - uses: actions/cache/restore@v5
+      - uses: actions/cache/restore@v6
         with:
           path: ~/.local/bin
           key: aiur-bench-bins-${{ github.sha }}
@@ -102,7 +102,7 @@ jobs:
           use-mathlib-cache: ${{ matrix.mathlib && 'true' || 'false' }}
       # FLT and FC take a few minutes to rebuild, so cache their build artifacts.
       - if: matrix.cache_pkg
-        uses: actions/cache@v5
+        uses: actions/cache@v6
         with:
           path: ${{ env.COMPILE_DIR }}/.lake/packages/${{ matrix.cache_pkg }}/.lake/build
           key: ${{ matrix.cache_pkg }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', env.COMPILE_DIR)) }}-${{ hashFiles(format('{0}/lake-manifest.json', env.COMPILE_DIR)) }}
@@ -118,7 +118,7 @@ jobs:
       # Cache the `.ixe` for the prove job (reused, never recompiled there).
       # Only the matrix jobs the prove job consumes, to stay under the repo cache limit.
       - if: matrix.bench == 'InitStd' || matrix.bench == 'Mathlib'
-        uses: actions/cache/save@v5
+        uses: actions/cache/save@v6
         with:
           path: ${{ matrix.bench }}.ixe
           key: aiur-ixe-${{ github.sha }}-${{ matrix.bench }}
@@ -179,11 +179,11 @@ jobs:
           - bench: Mathlib
             consts: Nat.factorial Nat.Coprime Nat.Prime.two_le
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
         with:
           fetch-depth: 0     # full history for the baseline-anchor lookup
           fetch-tags: true   # bencher-track reads the bencher-thresholds-reset tag
-      - uses: actions/cache/restore@v5
+      - uses: actions/cache/restore@v6
         with:
           path: ~/.local/bin
           key: aiur-bench-bins-${{ github.sha }}
@@ -197,7 +197,7 @@ jobs:
           build: false
           use-github-cache: false
       # Pull the `.ixe` the compile job built — do NOT recompile it here.
-      - uses: actions/cache/restore@v5
+      - uses: actions/cache/restore@v6
         with:
           path: ${{ matrix.bench }}.ixe
           key: aiur-ixe-${{ github.sha }}-${{ matrix.bench }}
diff --git a/.github/workflows/bench-pr.yml b/.github/workflows/bench-pr.yml
index a2a1823c..87c9bcb3 100644
--- a/.github/workflows/bench-pr.yml
+++ b/.github/workflows/bench-pr.yml
@@ -27,7 +27,7 @@ jobs:
       benches: ${{ steps.bench-params.outputs.benches }}
       env-vars: ${{ steps.bench-params.outputs.env-vars }}
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
       - name: Parse PR comment body
         id: bench-params
         run: |
@@ -66,12 +66,12 @@ jobs:
           do
             echo "$var" | tee -a $GITHUB_ENV
           done
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
         # Get base branch of the PR
       - uses: xt0rted/pull-request-comment-branch@v3
         id: comment-branch
       - name: Checkout base branch
-        uses: actions/checkout@v6
+        uses: actions/checkout@v7
         with:
           ref: ${{ steps.comment-branch.outputs.base_sha }}
           path : ${{ github.workspace }}/base
@@ -89,7 +89,7 @@ jobs:
           fi
         working-directory: ${{ github.workspace }}/base
       - name: Checkout PR branch
-        uses: actions/checkout@v6
+        uses: actions/checkout@v7
         with:
           path: ${{ github.workspace }}/pr
           ref: ${{ steps.comment-branch.outputs.head_sha }}
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index b7a4eb34..e104bffc 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -17,7 +17,7 @@ jobs:
   lean-test:
     runs-on: warp-ubuntu-latest-x64-16x
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
       - uses: actions-rust-lang/setup-rust-toolchain@v1
       - uses: leanprover/lean-action@v1
         with:
@@ -37,7 +37,7 @@ jobs:
   rust-test:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
       - uses: actions-rust-lang/setup-rust-toolchain@v1
       - uses: taiki-e/install-action@nextest
       # Install Lean for rust-bindgen step
diff --git a/.github/workflows/ignored.yml b/.github/workflows/ignored.yml
index 5e92186a..50efda6b 100644
--- a/.github/workflows/ignored.yml
+++ b/.github/workflows/ignored.yml
@@ -16,10 +16,10 @@ jobs:
   ignored-test:
     runs-on: warp-ubuntu-latest-x64-32x
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
       - uses: actions-rust-lang/setup-rust-toolchain@v1
       # Only restore the cache, since `ci.yml` will save the test binary to the cache first
-      - uses: actions/cache/restore@v5
+      - uses: actions/cache/restore@v6
         with:
           path: .lake
           key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
@@ -38,10 +38,10 @@ jobs:
   valgrind-ffi:
     runs-on: warp-ubuntu-latest-x64-8x
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
       - uses: actions-rust-lang/setup-rust-toolchain@v1
       # Only restore the cache, since `ci.yml` will save the test binary to the cache first
-      - uses: actions/cache/restore@v5
+      - uses: actions/cache/restore@v6
         with:
           path: .lake
           key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml
index 265380c3..fa0cddbc 100644
--- a/.github/workflows/nix.yml
+++ b/.github/workflows/nix.yml
@@ -19,7 +19,7 @@ jobs:
     name: Nix Tests
     runs-on: warp-ubuntu-latest-x64-8x
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
       - uses: cachix/install-nix-action@v31
         with:
           nix_path: nixpkgs=channel:nixos-unstable
@@ -35,7 +35,7 @@ jobs:
     name: Nix devShell Tests
     runs-on: warp-ubuntu-latest-x64-8x
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
       - uses: cachix/install-nix-action@v31
         with:
           nix_path: nixpkgs=channel:nixos-unstable
diff --git a/.github/workflows/riscv-bench.yml b/.github/workflows/riscv-bench.yml
index d9ec22b7..03b2dbad 100644
--- a/.github/workflows/riscv-bench.yml
+++ b/.github/workflows/riscv-bench.yml
@@ -23,14 +23,14 @@ jobs:
     name: Compile zkVM fixture (minimal.ixe)
     runs-on: warp-ubuntu-latest-x64-16x
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
       - uses: actions-rust-lang/setup-rust-toolchain@v1
       - uses: leanprover/lean-action@v1
         with:
           build-args: "--wfail -v"
       - name: Compile zkVM test fixture (minimal.ixe)
         run: lake exe ix compile Tests/MinimalDefs.lean --out minimal.ixe
-      - uses: actions/upload-artifact@v4
+      - uses: actions/upload-artifact@v7
         with:
           name: minimal-ixe
           path: minimal.ixe
@@ -56,7 +56,7 @@ jobs:
     needs: compile-fixture
     runs-on: warp-ubuntu-latest-x64-16x
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
       - uses: actions-rust-lang/setup-rust-toolchain@v1
         with:
           cache-workspaces: sp1
@@ -69,7 +69,7 @@ jobs:
             libsecp256k1-dev libsodium-dev libpqxx-dev nasm libopenmpi-dev \
             openmpi-bin openmpi-common libclang-dev clang gcc-riscv64-unknown-elf \
             pkg-config libssl-dev
-      - uses: actions/download-artifact@v4
+      - uses: actions/download-artifact@v8
         with:
           name: minimal-ixe
       - name: Install SP1 toolchain (sp1up, latest)
@@ -90,7 +90,7 @@ jobs:
     needs: compile-fixture
     runs-on: warp-ubuntu-latest-x64-16x
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v7
       - uses: actions-rust-lang/setup-rust-toolchain@v1
         with:
           cache-workspaces: zisk
@@ -103,7 +103,7 @@ jobs:
             libsecp256k1-dev libsodium-dev libpqxx-dev nasm libopenmpi-dev \
             openmpi-bin openmpi-common libclang-dev clang gcc-riscv64-unknown-elf \
             pkg-config libssl-dev
-      - uses: actions/download-artifact@v4
+      - uses: actions/download-artifact@v8
         with:
           name: minimal-ixe
       - name: Install Zisk toolchain (ziskup, pinned v0.18.0)