diff --git a/.github/dependabot.yaml b/.github/dependabot.yaml
index 9c1fe0a..60356ee 100644
--- a/.github/dependabot.yaml
+++ b/.github/dependabot.yaml
@@ -7,4 +7,10 @@ updates:
     directory: "/"
     schedule:
       # Check for updates to GitHub Actions every week
-      interval: "weekly"
\ No newline at end of file
+      interval: "weekly"
+    cooldown:
+      default-days: 7
+    groups:
+      actions-dependencies:
+        patterns:
+          - "*"
diff --git a/.github/pinact.yaml b/.github/pinact.yaml
new file mode 100644
index 0000000..ffc05eb
--- /dev/null
+++ b/.github/pinact.yaml
@@ -0,0 +1,7 @@
+version: 3
+rules:
+  # Branch refs that must keep tracking their branch: there is no stable tag
+  # to pin to. The shared ci-workflows actions are consumed from `main`.
+  - ignore: true
+    conditions:
+      - expr: ActionName matches "^argumentcomputer/ci-workflows/"
diff --git a/.github/workflows/e2e_test.yml b/.github/workflows/e2e_test.yml
index 61c1c24..fdbf2d1 100644
--- a/.github/workflows/e2e_test.yml
+++ b/.github/workflows/e2e_test.yml
@@ -26,7 +26,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
 
       - name: Update Lean package
         id: update
@@ -44,7 +46,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
 
       - name: Update Lean package with mathlib dependency
         id: update
@@ -66,7 +70,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
 
       - name: Update Lean package with nightly
         id: update
@@ -82,9 +88,11 @@ jobs:
         run: exit 1
 
       - name: The latest Lean release should be nightly
+        env:
+          LATEST_LEAN: ${{ steps.update.outputs.latest_lean }}
         run: |
-          echo "Latest Lean version: ${{ steps.update.outputs.latest_lean }}"
-          if [[ ! "${{ steps.update.outputs.latest_lean }}" =~ ^nightly- ]]; then
+          echo "Latest Lean version: $LATEST_LEAN"
+          if [[ ! "$LATEST_LEAN" =~ ^nightly- ]]; then
             echo "Error: The latest_lean output should start with 'nightly-'"
             exit 1
           fi
@@ -100,7 +108,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
 
       - name: Update Lean package
         id: update
@@ -117,7 +127,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
 
       - name: Update Lean package
         id: update
@@ -138,7 +150,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
 
       - name: Update Lean package
         id: update
@@ -171,7 +185,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
 
       - name: Bump the pinned tag and the toolchain
         id: update
@@ -231,7 +247,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
 
       - name: Bump a package whose dependency is commit-pinned
         id: update
@@ -269,7 +287,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
 
       - name: Bump the toolchain of a dependency-free package
         id: update
@@ -299,7 +319,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
 
       - name: Bump two packages at once
         id: update
@@ -325,10 +347,12 @@ jobs:
           fi
 
       - name: The release must be reported as an output
+        env:
+          LATEST_LEAN: ${{ steps.update.outputs.latest_lean }}
         run: |
-          echo "latest_lean=${{ steps.update.outputs.latest_lean }}"
+          echo "latest_lean=$LATEST_LEAN"
           expected=$(cut -d: -f2 Fixtures/PinnedTags/lean-toolchain)
-          if [ "${{ steps.update.outputs.latest_lean }}" != "$expected" ]; then
+          if [ "$LATEST_LEAN" != "$expected" ]; then
             echo "Error: expected $expected"
             exit 1
           fi
@@ -343,7 +367,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
 
       - name: Bump two packages, excluding one of them
         id: update
diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
index e1cc14c..b9399c5 100644
--- a/.github/workflows/lean_action_ci.yml
+++ b/.github/workflows/lean_action_ci.yml
@@ -26,7 +26,20 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v7
-      - uses: leanprover/lean-action@v1
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
+      - uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
         env:
           GH_TOKEN: ${{ github.token }}
+
+  lints:
+    name: Lint workflows
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
+      # actionlint, shellcheck over composite action scripts, pinact (actions
+      # must be SHA-pinned with a matching version comment) and zizmor
+      - uses: argumentcomputer/ci-workflows/.github/actions/lint-workflows@main
diff --git a/.github/workflows/test.yaml b/.github/workflows/test.yaml
index bdc4d45..1a6bf6a 100644
--- a/.github/workflows/test.yaml
+++ b/.github/workflows/test.yaml
@@ -26,7 +26,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
 
       - name: Update Lean package
         id: update
@@ -44,7 +46,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
       - name: Update Lean package
         id: update
         uses: ./
@@ -60,7 +64,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
 
       - name: Update Lean package
         id: update
@@ -71,18 +77,22 @@ jobs:
           lake_package_directory: "./Fixtures/SmokeSuccess"
 
       - name: output assertion of latest_lean
+        env:
+          LATEST_LEAN: ${{ steps.update.outputs.latest_lean }}
         run: |
-          echo "Latest Lean version: ${{ steps.update.outputs.latest_lean }}"
-          if [[ ! "${{ steps.update.outputs.latest_lean }}" =~ ^v ]]; then
+          echo "Latest Lean version: $LATEST_LEAN"
+          if [[ ! "$LATEST_LEAN" =~ ^v ]]; then
             echo "Error: The latest_lean output should start with 'v'"
             exit 1
           fi
           echo "latest_lean output test passed"
 
       - name: output assertion of notify
+        env:
+          NOTIFY: ${{ steps.update.outputs.notify }}
         run: |
-          echo "Notify status: ${{ steps.update.outputs.notify }}"
-          if [[ "${{ steps.update.outputs.notify }}" != "true" ]]; then
+          echo "Notify status: $NOTIFY"
+          if [[ "$NOTIFY" != "true" ]]; then
             echo "Error: The notify output should be 'true' for this test case"
             echo "This test should have updates available with a successful build"
             exit 1
@@ -93,7 +103,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
 
       - name: Update Lean package
         id: update
@@ -104,9 +116,11 @@ jobs:
           lake_package_directory: "./Fixtures/HasDep"
 
       - name: output assertion of latest_lean
+        env:
+          LATEST_LEAN: ${{ steps.update.outputs.latest_lean }}
         run: |
-          echo "Latest Lean version: ${{ steps.update.outputs.latest_lean }}"
-          if [[ ! "${{ steps.update.outputs.latest_lean }}" =~ ^v ]]; then
+          echo "Latest Lean version: $LATEST_LEAN"
+          if [[ ! "$LATEST_LEAN" =~ ^v ]]; then
             echo "Error: The latest_lean output should start with 'v' even when dependencies are present"
             exit 1
           fi
@@ -116,7 +130,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
 
       - name: Record original lean-toolchain
         id: original-toolchain
@@ -132,18 +148,21 @@ jobs:
           update_lean_toolchain: "never"
 
       - name: output assertion of latest_lean
+        env:
+          LATEST_LEAN: ${{ steps.update.outputs.latest_lean }}
         run: |
-          echo "Latest Lean version: ${{ steps.update.outputs.latest_lean }}"
-          if [[ ! "${{ steps.update.outputs.latest_lean }}" =~ ^v ]]; then
+          echo "Latest Lean version: $LATEST_LEAN"
+          if [[ ! "$LATEST_LEAN" =~ ^v ]]; then
             echo "Error: The latest_lean output should start with 'v' even when update_lean_toolchain is never"
             exit 1
           fi
           echo "latest_lean output test with update_lean_toolchain=never passed"
 
       - name: lean-toolchain should not be updated
+        env:
+          ORIGINAL_TOOLCHAIN: ${{ steps.original-toolchain.outputs.content }}
         run: |
           CURRENT_TOOLCHAIN=$(cat Fixtures/SmokeSuccess/lean-toolchain)
-          ORIGINAL_TOOLCHAIN="${{ steps.original-toolchain.outputs.content }}"
           echo "Original lean-toolchain: $ORIGINAL_TOOLCHAIN"
           echo "Current lean-toolchain: $CURRENT_TOOLCHAIN"
           if [[ "$CURRENT_TOOLCHAIN" != "$ORIGINAL_TOOLCHAIN" ]]; then
diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml
index c685428..5843e3d 100644
--- a/.github/workflows/update.yml
+++ b/.github/workflows/update.yml
@@ -15,9 +15,11 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
 
-      - uses: cachix/install-nix-action@v31
+      - uses: cachix/install-nix-action@13d8dd58da0234aa297dedd986986ccb8e7f3e24 # v31.11.1
         with:
           github_access_token: ${{ github.token }}
 
diff --git a/.github/zizmor.yml b/.github/zizmor.yml
new file mode 100644
index 0000000..89b0279
--- /dev/null
+++ b/.github/zizmor.yml
@@ -0,0 +1,15 @@
+rules:
+  unpinned-uses:
+    config:
+      policies:
+        # Branch-tracking ref allowed by .github/pinact.yaml
+        "argumentcomputer/ci-workflows/*": ref-pin
+        "*": hash-pin
+  # The test workflows exercise this repository's own action through
+  # `uses: ./`, the form upstream uses; keeping it avoids a diff on every
+  # upstream sync.
+  self-repository:
+    ignore:
+      - e2e_test.yml
+      - test.yaml
+      - update.yml
diff --git a/Fixtures/HasDep/.github/workflows/lean_action_ci.yml b/Fixtures/HasDep/.github/workflows/lean_action_ci.yml
deleted file mode 100644
index c48bd68..0000000
--- a/Fixtures/HasDep/.github/workflows/lean_action_ci.yml
+++ /dev/null
@@ -1,14 +0,0 @@
-name: Lean Action CI
-
-on:
-  push:
-  pull_request:
-  workflow_dispatch:
-
-jobs:
-  build:
-    runs-on: ubuntu-latest
-
-    steps:
-      - uses: actions/checkout@v5
-      - uses: leanprover/lean-action@v1
diff --git a/Fixtures/TwoDeps/.github/workflows/lean_action_ci.yml b/Fixtures/TwoDeps/.github/workflows/lean_action_ci.yml
deleted file mode 100644
index c48bd68..0000000
--- a/Fixtures/TwoDeps/.github/workflows/lean_action_ci.yml
+++ /dev/null
@@ -1,14 +0,0 @@
-name: Lean Action CI
-
-on:
-  push:
-  pull_request:
-  workflow_dispatch:
-
-jobs:
-  build:
-    runs-on: ubuntu-latest
-
-    steps:
-      - uses: actions/checkout@v5
-      - uses: leanprover/lean-action@v1
diff --git a/action.yml b/action.yml
index 0294649..61a52fb 100644
--- a/action.yml
+++ b/action.yml
@@ -246,8 +246,8 @@ runs:
         succ="$ON_SUCCESS"
         fail="$ON_FAILURE"
         if [ "$PR" = "true" ]; then
-          succ=pr
-          fail=pr
+          succ="pr"
+          fail="pr"
         fi
         echo "on-success=$succ" | tee -a "$GITHUB_OUTPUT"
         echo "on-failure=$fail" | tee -a "$GITHUB_OUTPUT"
@@ -258,10 +258,11 @@ runs:
         ON_FAILURE: ${{ inputs.on_update_fails }}
 
     - name: Install elan
-      run: |
+      # The appended path is the runner's own home directory, not event data.
+      run: | # zizmor: ignore[github-env]
         : Install elan
         curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y
-        echo "$HOME/.elan/bin" >> $GITHUB_PATH
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
       shell: bash
 
     - name: read lake-manifest.json and find dependencies
@@ -382,48 +383,54 @@ runs:
     # -------------------------------- #
     - name: Record the outcome
       id: record-result
+      env:
+        LEAN4_NIX_READY: ${{ steps.update-lean4-nix.outputs.ready }}
+        VALIDATE_OUTCOME: ${{ steps.validate-update.outcome }}
       run: |
         : Record the outcome
-        if [ "${{ steps.update-lean4-nix.outputs.ready }}" == "false" ]; then
+        if [ "$LEAN4_NIX_READY" == "false" ]; then
           echo "Update is waiting for lean4-nix"
-          echo "outcome=update-deferred" >> $GITHUB_OUTPUT
-        elif [ "${{ env.LEAN_UPDATE_FILES_CHANGED }}" == "false" ]; then
+          echo "outcome=update-deferred" >> "$GITHUB_OUTPUT"
+        elif [ "$LEAN_UPDATE_FILES_CHANGED" == "false" ]; then
           echo "No update available"
-          echo "outcome=no-update" >> $GITHUB_OUTPUT
-        elif [ "${{ steps.validate-update.outcome }}" == "success" ]; then
+          echo "outcome=no-update" >> "$GITHUB_OUTPUT"
+        elif [ "$VALIDATE_OUTCOME" == "success" ]; then
           echo "Update available and validation successful"
-          echo "outcome=update-success" >> $GITHUB_OUTPUT
-        elif [ "${{ steps.validate-update.outcome }}" == "failure" ]; then
+          echo "outcome=update-success" >> "$GITHUB_OUTPUT"
+        elif [ "$VALIDATE_OUTCOME" == "failure" ]; then
           echo "Update available but validation fails"
-          echo "outcome=update-fail" >> $GITHUB_OUTPUT
-        elif [ "${{ steps.validate-update.outcome }}" == "skipped" ]; then
+          echo "outcome=update-fail" >> "$GITHUB_OUTPUT"
+        elif [ "$VALIDATE_OUTCOME" == "skipped" ]; then
           echo "Update available; validation skipped"
-          echo "outcome=update-unvalidated" >> $GITHUB_OUTPUT
+          echo "outcome=update-unvalidated" >> "$GITHUB_OUTPUT"
         fi
       shell: bash
 
     - name: Record the notify status
       id: record-notify
+      env:
+        LEAN4_NIX_READY: ${{ steps.update-lean4-nix.outputs.ready }}
+        VALIDATE_OUTCOME: ${{ steps.validate-update.outcome }}
       run: |
         : Record the notify status
-        if [ "${{ steps.update-lean4-nix.outputs.ready }}" == "false" ]; then
+        if [ "$LEAN4_NIX_READY" == "false" ]; then
           echo "Update deferred until lean4-nix is ready"
-          echo "notify=false" >> $GITHUB_OUTPUT
-        elif [ "${{ env.LEAN_UPDATE_FILES_CHANGED }}" == "false" ]; then
+          echo "notify=false" >> "$GITHUB_OUTPUT"
+        elif [ "$LEAN_UPDATE_FILES_CHANGED" == "false" ]; then
           echo "No updates available, no need to notify"
-          echo "notify=false" >> $GITHUB_OUTPUT
-        elif [ "${{ steps.validate-update.outcome }}" == "success" ] && [ "${{ env.LEAN_UPDATE_DO_UPDATE }}" == "true" ]; then
+          echo "notify=false" >> "$GITHUB_OUTPUT"
+        elif [ "$VALIDATE_OUTCOME" == "success" ] && [ "$LEAN_UPDATE_DO_UPDATE" == "true" ]; then
           echo "Updates available and validation successful - should notify"
-          echo "notify=true" >> $GITHUB_OUTPUT
-        elif [ "${{ steps.validate-update.outcome }}" == "failure" ]; then
+          echo "notify=true" >> "$GITHUB_OUTPUT"
+        elif [ "$VALIDATE_OUTCOME" == "failure" ]; then
           echo "Updates available but validation failed - should notify"
-          echo "notify=true" >> $GITHUB_OUTPUT
-        elif [ "${{ steps.validate-update.outcome }}" == "skipped" ] && [ "${{ env.LEAN_UPDATE_DO_UPDATE }}" == "true" ]; then
+          echo "notify=true" >> "$GITHUB_OUTPUT"
+        elif [ "$VALIDATE_OUTCOME" == "skipped" ] && [ "$LEAN_UPDATE_DO_UPDATE" == "true" ]; then
           echo "Updates available with validation skipped - should notify"
-          echo "notify=true" >> $GITHUB_OUTPUT
+          echo "notify=true" >> "$GITHUB_OUTPUT"
         else
           echo "No need to notify in this case"
-          echo "notify=false" >> $GITHUB_OUTPUT
+          echo "notify=false" >> "$GITHUB_OUTPUT"
         fi
       shell: bash
 
@@ -456,7 +463,7 @@ runs:
           steps.outcomes.outputs.on-success == 'pr' &&
           steps.outcomes.outputs.on-failure == 'pr' &&
           env.LEAN_UPDATE_DO_UPDATE == 'true'))
-      uses: peter-evans/create-pull-request@v8
+      uses: peter-evans/create-pull-request@5f6978faf089d4d20b00c7766989d076bb2fc7f1 # v8.1.1
       with:
         token: ${{ inputs.token }}
         title: "chore: Update Lean to ${{ env.LEAN_UPDATE_LATEST_LEAN }}"
@@ -486,7 +493,7 @@ runs:
 
     - name: Commit update if post-update validation was successful
       if: steps.validate-update.outcome == 'success' && steps.outcomes.outputs.on-success == 'commit' && env.LEAN_UPDATE_DO_UPDATE == 'true'
-      uses: EndBug/add-and-commit@v10
+      uses: EndBug/add-and-commit@cc9c08ba6c8df3b93a8f2db63e89b98368ae2ae8 # v11.1.1
       with:
         default_author: github_actions
       env: