diff --git a/.github/actionlint.yaml b/.github/actionlint.yaml
new file mode 100644
index 000000000..4287f0f9e
--- /dev/null
+++ b/.github/actionlint.yaml
@@ -0,0 +1,6 @@
+# Custom labels for the self-hosted runners; actionlint cannot discover them.
+self-hosted-runner:
+  labels:
+    - normal
+    - fast
+    - MacM1
diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml
index e1065e562..286091200 100644
--- a/.github/actions/with-docker/action.yml
+++ b/.github/actions/with-docker/action.yml
@@ -3,37 +3,18 @@ description: 'Run a given stage with Docker Image'
 inputs:
   container-name:
     description: 'Docker container name to use'
-    type: string
     required: true
   tag-name:
     description: 'Docker image tag to use'
-    type: string
     required: false
     default: runtimeverificationinc/kontrol
-  subdir:
-    description: 'Subdirectory where code is cloned.'
-    required: false
-    type: string
-    default: './'
-  os:
-    description: 'OS to setup Docker for.'
-    required: false
-    type: string
-    default: 'ubuntu'
-  distro:
-    description: 'Distribution to setup Docker for.'
-    required: false
-    type: string
-    default: 'jammy'
   llvm:
     description: 'LLVM version to use.'
     required: false
-    type: number
     default: 14
   dockerfile:
     description: 'Hardcode the path of the dockerfile to use.'
     required: false
-    type: string
     default: '.github/workflows/Dockerfile'
 runs:
   using: 'composite'
@@ -45,24 +26,21 @@ runs:
   # of falling back to anonymous. Log in with a fresh token so the credential
   # is always valid (a valid GITHUB_TOKEN can pull public images from any org).
   - name: 'Log in to ghcr.io'
-    uses: docker/login-action@v3
+    uses: docker/login-action@c94ce9fb468520275223c153574b00df6fe4bcc9  # v3.7.0
     with:
       registry: ghcr.io
       username: ${{ github.actor }}
       password: ${{ github.token }}
   - name: 'Set up Docker'
+    env:
+      CONTAINER_NAME: ${{ inputs.container-name }}
+      DOCKERFILE: ${{ inputs.dockerfile }}
+      LLVM_VERSION: ${{ inputs.llvm }}
+      TAG_NAME: ${{ inputs.tag-name }}
     shell: bash {0}
     run: |
       set -euxo pipefail
 
-      CONTAINER_NAME=${{ inputs.container-name }}
-      SUBDIR=${{ inputs.subdir }}
-      BASE_OS=${{ inputs.os }}
-      BASE_DISTRO=${{ inputs.distro }}
-      DOCKERFILE=${{ inputs.dockerfile }}
-      LLVM_VERSION=${{ inputs.llvm }}
-      TAG_NAME=${{ inputs.tag-name }}
-
       USER=github-user
       GROUP=${USER}
       Z3_VERSION=$(cat deps/z3)
@@ -71,27 +49,26 @@ runs:
       USER_ID=1000
       GROUP_ID=${USER_ID}
 
-      docker build . --file ${DOCKERFILE}        \
-        --tag ${TAG_NAME}                        \
-        --build-arg USER_ID=${USER_ID}           \
-        --build-arg GROUP_ID=${GROUP_ID}         \
-        --build-arg USER=${USER}                 \
-        --build-arg GROUP=${GROUP}               \
-        --build-arg BASE_DISTRO=${BASE_DISTRO}   \
-        --build-arg K_VERSION=${K_VERSION}       \
-        --build-arg Z3_VERSION=${Z3_VERSION}     \
-        --build-arg LLVM_VERSION=${LLVM_VERSION} \
-        --build-arg UV_VERSION=${UV_VERSION}
+      docker build . --file "${DOCKERFILE}"         \
+        --tag "${TAG_NAME}"                         \
+        --build-arg USER_ID="${USER_ID}"            \
+        --build-arg GROUP_ID="${GROUP_ID}"          \
+        --build-arg USER="${USER}"                  \
+        --build-arg GROUP="${GROUP}"                \
+        --build-arg K_VERSION="${K_VERSION}"        \
+        --build-arg Z3_VERSION="${Z3_VERSION}"      \
+        --build-arg LLVM_VERSION="${LLVM_VERSION}"  \
+        --build-arg UV_VERSION="${UV_VERSION}"
 
-      docker run                          \
-        --name ${CONTAINER_NAME}          \
-        --rm                              \
-        --interactive                     \
-        --tty                             \
-        --detach                          \
-        --user root                       \
-        --workdir /home/${USER}/workspace \
-        ${TAG_NAME}
+      docker run                            \
+        --name "${CONTAINER_NAME}"          \
+        --rm                                \
+        --interactive                       \
+        --tty                               \
+        --detach                            \
+        --user root                         \
+        --workdir "/home/${USER}/workspace" \
+        "${TAG_NAME}"
 
-      docker cp . ${CONTAINER_NAME}:/home/${USER}/workspace
-      docker exec ${CONTAINER_NAME} chown -R ${USER}:${GROUP} /home/${USER}
+      docker cp . "${CONTAINER_NAME}":"/home/${USER}/workspace"
+      docker exec "${CONTAINER_NAME}" chown -R "${USER}:${GROUP}" "/home/${USER}"
diff --git a/.github/scripts/check-cachix-pin.sh b/.github/scripts/check-cachix-pin.sh
deleted file mode 100755
index 92d057ea5..000000000
--- a/.github/scripts/check-cachix-pin.sh
+++ /dev/null
@@ -1,99 +0,0 @@
-#!/usr/bin/env bash
-set -euo pipefail
-
-# Kup relies on cachix registry k-framework-binary.
-CACHE="k-framework-binary"
-OWNER_REPO="${OWNER_REPO:-$(git remote get-url origin | sed -E 's#(git@github.com:|https://github.com/)##; s#\.git$##')}"
-REV="${REV:-${GITHUB_SHA:-$(git rev-parse HEAD)}}"
-UNAME_S="$(uname -s)"
-UNAME_M="$(uname -m)"
-case "${UNAME_S}-${UNAME_M}" in
-  Linux-x86_64) SYSTEM="x86_64-linux" ;;
-  Linux-aarch64 | Linux-arm64) SYSTEM="aarch64-linux" ;;
-  Darwin-x86_64) SYSTEM="x86_64-darwin" ;;
-  Darwin-arm64) SYSTEM="aarch64-darwin" ;;
-  *)
-    echo "Unsupported platform: ${UNAME_S}-${UNAME_M}" >&2
-    exit 1
-    ;;
-esac
-PIN_API_URL="https://app.cachix.org/api/v1/cache/${CACHE}/pin"
-CHECK_PACKAGES=(kontrol kontrol.solc_0_8_13 kontrol.solc_0_8_15)
-
-SUMMARY="${GITHUB_STEP_SUMMARY:-/dev/stdout}"
-
-# Append to the GitHub step summary when set; always print to stdout for live job logs.
-summary_and_log() {
-  if [[ "${SUMMARY}" == "/dev/stdout" ]]; then
-    cat
-  else
-    tee -a "${SUMMARY}"
-  fi
-}
-
-{
-  echo "## Cachix Publish Summary"
-  echo "CACHE: $CACHE"
-  echo "OWNER_REPO: $OWNER_REPO"
-  echo "REV: $REV"
-  echo "SYSTEM: $SYSTEM"
-  echo "PACKAGES: ${CHECK_PACKAGES[*]}"
-} >> "$SUMMARY"
-
-# Verify push + pin together for each package. Both can become visible with delay.
-PIN_VISIBILITY_TIMEOUT_SECONDS=120 # 2 minutes
-PIN_VISIBILITY_INTERVAL_SECONDS=5  # 5 seconds
-PIN_VISIBILITY_ATTEMPTS=$((PIN_VISIBILITY_TIMEOUT_SECONDS / PIN_VISIBILITY_INTERVAL_SECONDS))
-for i in $(seq 1 "$PIN_VISIBILITY_ATTEMPTS"); do
-  PIN_JSON="$(curl -fsSL "${PIN_API_URL}?q=${REV}")"
-  ALL_OK=1
-
-  for PKG in "${CHECK_PACKAGES[@]}"; do
-    KEY="github:${OWNER_REPO}/${REV}#packages.${SYSTEM}.${PKG}"
-    STORE_PATH="$(
-      echo "$PIN_JSON" \
-        | jq -r --arg k "$KEY" 'map(select(.name == $k)) | first | (.lastRevision.storePath // .storePath // .store_path // .path // "")'
-    )"
-    if [ -z "$STORE_PATH" ]; then
-      PIN_STATUS="pin-missing"
-      PUSH_STATUS="000"
-      ALL_OK=0
-      {
-        echo "key-${PKG}: ${KEY}"
-        echo "pin-status-${PKG}: ${PIN_STATUS}"
-        echo "push-http-${PKG}: ${PUSH_STATUS}"
-      } | summary_and_log
-      continue
-    fi
-
-    PIN_STATUS="pin-ok"
-    HASH="$(basename "$STORE_PATH" | cut -d- -f1)"
-    PUSH_NARINFO_URL="https://${CACHE}.cachix.org/${HASH}.narinfo"
-    PUSH_STATUS="$(curl -sS -o /dev/null -w '%{http_code}' "$PUSH_NARINFO_URL")" || PUSH_STATUS="000"
-    if [ "$PUSH_STATUS" != "200" ]; then
-      ALL_OK=0
-    fi
-
-    {
-      echo "key-${PKG}: ${KEY}"
-      echo "store-path-${PKG}: ${STORE_PATH}"
-      echo "pin-status-${PKG}: ${PIN_STATUS}"
-      echo "push-http-${PKG}: ${PUSH_STATUS}"
-    } | summary_and_log
-  done
-
-  if [ "$ALL_OK" = "1" ]; then
-    echo "cachix-status: push-and-pin-ok-for-all-packages" >> "$SUMMARY"
-    exit 0
-  fi
-
-  RETRY_MSG="cachix-check-attempt-${i}: not-ready, retrying in ${PIN_VISIBILITY_INTERVAL_SECONDS}s"
-  printf '%s\n' "$RETRY_MSG" | summary_and_log
-  sleep "$PIN_VISIBILITY_INTERVAL_SECONDS"
-done
-
-echo "cachix-status: push-or-pin-missing-after-${PIN_VISIBILITY_TIMEOUT_SECONDS}s-for-at-least-one-package" >> "$SUMMARY"
-# Pin API bulk JSON goes to job logs only (step summary stays readable); helps if the response shape changes.
-echo "check-cachix-pin: raw Cachix pin API response (last fetch):" >&2
-echo "$PIN_JSON" >&2
-exit 1
diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile
index af30107f7..375ffb314 100644
--- a/.github/workflows/Dockerfile
+++ b/.github/workflows/Dockerfile
@@ -1,6 +1,5 @@
 ARG Z3_VERSION
 ARG K_VERSION
-ARG BASE_DISTRO
 ARG LLVM_VERSION
 
 FROM ghcr.io/foundry-rs/foundry:rc-1 as FOUNDRY
diff --git a/.github/workflows/kontrol-push-fixed-deps.yml b/.github/workflows/kontrol-push-fixed-deps.yml
deleted file mode 100644
index cc2537a9b..000000000
--- a/.github/workflows/kontrol-push-fixed-deps.yml
+++ /dev/null
@@ -1,80 +0,0 @@
----
-name: 'Push Kontrol w/ FIXED Dependencies'
-on:
-  workflow_dispatch:
-
-    inputs:
-      kontrol_branch:
-        description: "Branch of Kontrol to use to build the Docker image"
-        required: true
-
-jobs:
-  dockerhub:
-    name: 'Build and Publish Docker Image'
-    runs-on: [self-hosted, linux, normal]
-    steps:
-      - name: 'Check out code'
-        uses: actions/checkout@v4
-        with:
-          ref: ${{ github.event.inputs.kontrol_branch}}
-          fetch-depth: 0
-
-      - name: 'Set environment'
-        run: |
-          KONTROL_VERSION=$(cat package/version)
-          echo "CONTAINER_NAME=kontrol-ci-docker-${GITHUB_SHA}" >> ${GITHUB_ENV}
-          BRANCH_NAME="${{ github.event.inputs.kontrol_branch }}"
-          SANITIZED_BRANCH_NAME=$(echo "${BRANCH_NAME}" | tr '/' '-' | tr -cd '[:alnum:]-_.')
-          GHCR_TAG=ghcr.io/runtimeverification/kontrol/kontrol-custom:ubuntu-jammy-${SANITIZED_BRANCH_NAME}
-          echo "GHCR_TAG=${GHCR_TAG}" >> ${GITHUB_ENV}
-          echo "DOCKER_USER=user" >> ${GITHUB_ENV}
-          echo "DOCKER_GROUP=user" >> ${GITHUB_ENV}
-          echo "FOUNDRY_ROOT=/home/user/foundry" >> ${GITHUB_ENV}
-
-      - name: 'Build Docker image'
-        run: |
-          K_VERSION=$(cat deps/k_release)
-          Z3_VERSION=$(cat deps/z3)
-          docker build . --no-cache --tag ${GHCR_TAG} --build-arg K_VERSION=${K_VERSION} --build-arg Z3_VERSION=${Z3_VERSION}
-
-      - name: 'Run Docker image'
-        run: |
-          docker run                        \
-          --name ${CONTAINER_NAME}          \
-          --rm                              \
-          --interactive                     \
-          --tty                             \
-          --detach                          \
-          --user root                       \
-          ${GHCR_TAG}
-
-          docker cp src/tests/integration/test-data/foundry ${CONTAINER_NAME}:${FOUNDRY_ROOT}
-          docker exec ${CONTAINER_NAME} chown -R ${DOCKER_USER}:${DOCKER_GROUP} ${FOUNDRY_ROOT}
-
-      - name: 'Run forge build'
-        run: |
-          docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} forge install --no-git foundry-rs/forge-std@75f1746
-          docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} forge install --no-git runtimeverification/kontrol-cheatcodes@a5dd4b0
-          docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} forge build
-  
-      - name: 'Run kontrol build'
-        run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol build -O2
-  
-      - name: 'Run kontrol prove'
-        run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol prove --match-test 'AssertTest.test_assert_true()'
-  
-      - name: 'Run kontrol show'
-        run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol show 'AssertTest.test_assert_true()'
-  
-      - name: 'Tear Down Docker'
-        if: always()
-        run: |
-          docker stop --time=0 ${CONTAINER_NAME}
-
-      - name: 'Push Docker Image to GitHub Packages'
-        run: |
-          echo ${{ secrets.DOCKERHUB_PASSWORD }} | docker login -u ${{ vars.DOCKERHUB_USERNAME }} --password-stdin
-          echo ${{ secrets.GITHUB_TOKEN }} | docker login ghcr.io -u ${{ github.repository_owner }} --password-stdin
-          docker push ${GHCR_TAG}
-
-
diff --git a/.github/workflows/kontrol-push-unfixed-deps.yml b/.github/workflows/kontrol-push-unfixed-deps.yml
deleted file mode 100644
index 51eeee52b..000000000
--- a/.github/workflows/kontrol-push-unfixed-deps.yml
+++ /dev/null
@@ -1,74 +0,0 @@
----
-name: 'Push Kontrol w/ Dependencies'
-on:
-  workflow_dispatch:
-    inputs:
-      kontrol-version: 
-        description: 'Branch/Tag to use for Kontrol'
-        required: false
-        default: ''
-      kevm-version: 
-        description: 'SHA to use for KEVM'
-        required: false
-        default: ''
-      k-version: 
-        description: 'SHA to use for K'
-        required: false
-        default: ''
-      llvm-version: 
-        description: 'SHA to use for LLVM Backend'
-        required: false
-        default: ''
-      haskell-version: 
-        description: 'SHA to use for Haskell Backend'
-        required: false
-        default: ''
-permissions:
-  packages: write
-
-jobs:
-  build-kontrol:
-    runs-on: [self-hosted, normal]
-    steps:
-      - name: 'Login to GitHub Container Registry'
-        uses: docker/login-action@v2
-        with:
-          registry: ghcr.io
-          username: ${{ github.actor }}
-          password: ${{ secrets.GITHUB_TOKEN }}
-      - name: 'Build Kontrol'
-        shell: bash
-        run: |
-          set -o pipefail
-          docker run --env GH_TOKEN=${{ secrets.GITHUB_TOKEN }} --rm -it --detach --name kontrol-build-with-kup-${{ github.run_id }} ghcr.io/runtimeverification/kup:latest
-          if [ -n "${{ inputs.kontrol-version }}" ]; then
-              KONTROL_OVERRIDE="--version ${{ inputs.kontrol-version }}"
-          fi
-          if [ -n "${{ inputs.kevm-version }}" ]; then
-              KEVM_OVERRIDE="--override kevm ${{ inputs.kevm-version }}"
-          fi
-          if [ -n "${{ inputs.k-version }}" ]; then
-              K_OVERRIDE="--override kevm/k-framework ${{ inputs.k-version }}"
-          fi
-          if [ -n "${{ inputs.llvm-version }}" ]; then
-              LLVM_OVERRIDE="--override kevm/k-framework/llvm-backend ${{ inputs.llvm-version }}"
-          fi
-          if [ -n "${{ inputs.haskell-version }}" ]; then
-              HASKELL_OVERRIDE="--override kevm/k-framework/haskell-backend ${{ inputs.haskell-version }}"
-          fi
-          docker exec kontrol-build-with-kup-${{ github.run_id }} /bin/bash --login -c "kup install kontrol ${KONTROL_OVERRIDE} ${KEVM_OVERRIDE} ${K_OVERRIDE} ${LLVM_OVERRIDE} ${HASKELL_OVERRIDE}"
-          docker exec kontrol-build-with-kup-${{ github.run_id }} /bin/bash --login -c "kup list kontrol --inputs" >> versions.out
-          docker commit kontrol-build-with-kup-${{ github.run_id }} ghcr.io/runtimeverification/kontrol-custom:${{ github.run_id }}
-          docker push ghcr.io/runtimeverification/kontrol-custom:${{ github.run_id }}
-      - name: 'Publish Versions to Artifacts'
-        uses: actions/upload-artifact@v4
-        with:
-          name: Versions
-          path: versions.out
-      - name: 'Publish Image Name to Workflow Summary'
-        run: |
-          echo "Image Name: ghcr.io/runtimeverification/kontrol-custom:${{ github.run_id }}" >> $GITHUB_STEP_SUMMARY
-      - name: 'Tear down Docker'
-        if: always()
-        run: |
-          docker stop --time=0 kontrol-build-with-kup-${{ github.run_id }}
diff --git a/.github/workflows/lint-workflows.yml b/.github/workflows/lint-workflows.yml
new file mode 100644
index 000000000..63daf23bf
--- /dev/null
+++ b/.github/workflows/lint-workflows.yml
@@ -0,0 +1,53 @@
+---
+name: 'Lint Workflows'
+on:
+  pull_request:
+    branches:
+      - 'master'
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  actionlint:
+    name: 'actionlint'
+    runs-on: ubuntu-latest
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
+        with:
+          persist-credentials: false
+      - name: 'Install actionlint'
+        env:
+          # Pin the release and verify it, both values should be updated together.
+          ACTIONLINT_VERSION: '1.7.12'
+          ACTIONLINT_SHA256: '8aca8db96f1b94770f1b0d72b6dddcb1ebb8123cb3712530b08cc387b349a3d8'
+        run: |
+          set -euxo pipefail
+          curl --fail --silent --show-error --location --output actionlint.tar.gz \
+            "https://github.com/rhysd/actionlint/releases/download/v${ACTIONLINT_VERSION}/actionlint_${ACTIONLINT_VERSION}_linux_amd64.tar.gz"
+          echo "${ACTIONLINT_SHA256}  actionlint.tar.gz" | sha256sum --check --strict
+          tar --extract --gzip --file actionlint.tar.gz actionlint
+      - name: 'Run actionlint'
+        run: ./actionlint -color
+
+  zizmor:
+    name: 'zizmor'
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      security-events: write  # upload SARIF, so findings annotate the diff
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
+        with:
+          persist-credentials: false
+      - name: 'Run zizmor'
+        uses: zizmorcore/zizmor-action@3dc1ecc9bcb9e94e9b2c709687979e1298497054  # v0.6.2
+        with:
+          version: '1.29.0'
+          online-audits: false
+          advanced-security: true
diff --git a/.github/workflows/master-push.yml b/.github/workflows/master-push.yml
deleted file mode 100644
index 4e7d89ab9..000000000
--- a/.github/workflows/master-push.yml
+++ /dev/null
@@ -1,56 +0,0 @@
----
-name: 'Bump Release'
-on:
-  push:
-    branches:
-      - 'master'
-concurrency:
-  group: ${{ github.workflow }}-${{ github.ref }}
-  cancel-in-progress: true
-
-jobs:
-  version-bump:
-    name: 'Version Bump and Start Release'
-    runs-on: ubuntu-latest
-    steps:
-      - name: 'Check out code'
-        uses: actions/checkout@v4
-        with:
-          token: ${{ secrets.JENKINS_GITHUB_PAT }}
-          # fetch-depth 0 means deep clone the repo
-          fetch-depth: 0
-      - name: 'Configure GitHub user'
-        run: |
-          git config user.name rv-jenkins
-          git config user.email devops@runtimeverification.com
-      - name: 'Update version'
-        run: |
-          # Check out the release branch and create it if it doesn't exist
-          git checkout -B release origin/release
-          
-          # Get the common ancestor commit between master and release branches
-          old_master="$(git merge-base origin/master origin/release)"
-          
-          # Get the latest commit hash on the master branch
-          new_master="$(git rev-parse origin/master)"
-
-          # Check if there are changes in the package/version file between the common ancestor and the latest master commit
-          if git diff --exit-code ${old_master} ${new_master} -- package/version; then
-            # If there are no changes, bump the version based on the current version in master
-            git merge --no-edit origin/master
-            ./package/version.sh bump
-          else
-            # If there are changes, merge master into release with 'theirs' strategy to resolve conflicts
-            git merge --no-edit --strategy-option=theirs origin/master
-          fi
-          
-          # Substitute the version in the package/version file
-          ./package/version.sh sub
-          
-          # Add changes to the staging area and commit them if there are any changes
-          if git add --update && git commit --no-edit --allow-empty --message "Set Version: $(cat package/version)"; then
-            # Push the changes to the release branch -- Trigger the Release Process and Testing
-            git push origin release
-            git tag "release-$(cat package/version)" origin/master
-            git push origin "release-$(cat package/version)"
-          fi
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
deleted file mode 100644
index 4ffc1b5ca..000000000
--- a/.github/workflows/release.yml
+++ /dev/null
@@ -1,165 +0,0 @@
----
-name: 'Release'
-on:
-  push:
-    branches:
-      - 'release'
-jobs:
-
-  draft-release:
-    name: 'Draft Release'
-    runs-on: ubuntu-latest
-    outputs:
-      version: ${{ steps.make-release.outputs.version }}
-    steps:
-      - name: 'Check out code'
-        uses: actions/checkout@v4
-      - name: 'Make release'
-        id: 'make-release'
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-        run: |
-          set -x
-          VERSION=v$(cat package/version)
-          gh release create "${VERSION}"                  \
-            --repo runtimeverification/kontrol  \
-            --draft                                     \
-            --title ${VERSION}                          \
-            --target ${{ github.sha }}
-          echo "version=${VERSION}" >> "$GITHUB_OUTPUT"
-
-  nix-cache:
-    name: 'Populate Nix Caches'
-    strategy:
-      matrix:
-        runner: [normal, ARM64]
-    runs-on: ${{ matrix.runner }}
-    needs: draft-release
-    steps:
-      - name: 'Check out code'
-        uses: actions/checkout@v4
-        with:
-          ref: ${{ github.event.push.head.sha }}
-          fetch-depth: 0
-
-      # Build the Kontrol derivation once, then push it to both the public
-      # k-framework cache (full build closure, via `cachix push`) and the
-      # private k-framework-binary cache (the kup-installable binary, via
-      # `kup publish`). Both pushes reuse the build output already present in
-      # this runner's Nix store, so the derivation is never built twice.
-      - name: 'Build and publish Kontrol to both Nix caches'
-        uses: workflow/nix-shell-action@v3
-        env:
-          GC_DONT_GC: '1'
-          CACHIX_PUBLIC_TOKEN: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
-          CACHIX_PRIVATE_KFB_TOKEN: '${{ secrets.CACHIX_PRIVATE_KFB_TOKEN }}'
-          OWNER_REPO: '${{ github.repository }}'
-          REV: '${{ github.sha }}'
-        with:
-          packages: jq
-          script: |
-            KONTROL=$(nix build --extra-experimental-features 'nix-command flakes' .#kontrol --json | jq -r '.[].outputs | to_entries[].value')
-            DRV=$(nix-store --query --deriver ${KONTROL})
-
-            # Push the full build closure to the public k-framework cache.
-            export CACHIX_AUTH_TOKEN="${CACHIX_PUBLIC_TOKEN}"
-            nix-store --query --requisites --include-outputs ${DRV} | cachix push k-framework
-
-            # Publish the binaries to the private k-framework-binary cache. kup
-            # reuses the store paths built above and only builds the additional
-            # solc variants.
-            export CACHIX_AUTH_TOKEN="${CACHIX_PRIVATE_KFB_TOKEN}"
-            export PATH="$(nix build github:runtimeverification/kup --no-link --json | jq -r '.[].outputs | to_entries[].value')/bin:$PATH"
-            kup publish k-framework-binary .#kontrol --keep-days 180
-            kup publish k-framework-binary .#kontrol.solc_0_8_13 --keep-days 180
-            kup publish k-framework-binary .#kontrol.solc_0_8_15 --keep-days 180
-            # Cachix has not been responding to 'cachix pin' requests made under the hood by kup. Verify the push and pin manually.
-            .github/scripts/check-cachix-pin.sh
-
-      - name: 'On failure, delete drafted release'
-        if: failure()
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-        run: |
-          set -x
-          VERSION=v$(cat package/version)
-          gh release delete ${VERSION}                  \
-            --repo runtimeverification/kontrol  \
-            --yes                                       \
-            --cleanup-tag
-
-  dockerhub:
-    name: 'Build and Publish Docker Image'
-    runs-on: [self-hosted, linux, normal]
-    needs: draft-release
-    steps:
-      - name: 'Check out code'
-        uses: actions/checkout@v4
-        with:
-          ref: ${{ github.event.push.head.sha }}
-          fetch-depth: 0
-
-      - name: 'Set environment'
-        run: |
-          KONTROL_VERSION=$(cat package/version)
-          TAG=runtimeverificationinc/kontrol:ubuntu-jammy-${KONTROL_VERSION}
-          echo "TAG=${TAG}" >> ${GITHUB_ENV}
-
-      - name: 'Build Docker image'
-        run: |
-          K_VERSION=$(cat deps/k_release)
-          Z3_VERSION=$(cat deps/z3)
-          docker build . --no-cache --tag ${TAG} --build-arg K_VERSION=${K_VERSION} --build-arg Z3_VERSION=${Z3_VERSION}
-
-      - name: 'Run Docker image'
-        run: docker run --rm ${TAG} kontrol --help
-
-      - name: 'Push Docker image to Docker Hub'
-        run: |
-          echo "${{ secrets.DOCKERHUB_PASSWORD }}" | docker login --username rvdockerhub --password-stdin
-          docker image push ${TAG}
-
-      - name: 'On failure, delete drafted release'
-        if: failure()
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-        run: |
-          set -x
-          VERSION=v$(cat package/version)
-          gh release delete ${VERSION}                  \
-            --repo runtimeverification/kontrol  \
-            --yes                                       \
-            --cleanup-tag          
-
-  cut-release:
-    name: 'Cut Release'
-    runs-on: ubuntu-latest
-    needs: [dockerhub, nix-cache]
-    steps:
-      - name: 'Check out code'
-        uses: actions/checkout@v4
-        with:
-          ref: ${{ github.event.push.head.sha }}
-          fetch-depth: 0
-
-      - name: 'Finalize Release'
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-        run: |
-          set -x
-          VERSION=v$(cat package/version)
-          gh release edit ${VERSION}                    \
-            --repo runtimeverification/kontrol  \
-            --draft=false
-
-      - name: 'Update dependents'
-        run: |
-          set -x
-          VERSION=$(cat package/version)
-          curl --fail                                                          \
-            -X POST                                                            \
-            -H "Accept: application/vnd.github+json"                           \
-            -H "Authorization: Bearer ${{ secrets.JENKINS_GITHUB_PAT }}"       \
-            -H "X-GitHub-Api-Version: 2022-11-28"                              \
-            https://api.github.com/repos/runtimeverification/devops/dispatches \
-            -d '{"event_type":"on-demand-test","client_payload":{"repo":"runtimeverification/kontrol","version":"'${VERSION}'"}}'
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index 2a74d3d6d..a19e14fe2 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -8,19 +8,27 @@ concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
+# No job here writes to the repository, so the token stays read-only regardless of
+# the repository default. Jobs that build the CI image additionally need
+# `packages: read` to pull `ghcr.io/foundry-rs/foundry`.
+permissions:
+  contents: read
+
 jobs:
   code-quality-checks:
     name: 'Code Quality Checks'
     runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v4
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
+        with:
+          persist-credentials: false
       - name: 'Get uv release'
         id: uv_release
         run: |
-          echo uv_version=$(cat deps/uv_release) >> "${GITHUB_OUTPUT}"
+          echo "uv_version=$(cat deps/uv_release)" >> "${GITHUB_OUTPUT}"
       - name: 'Install uv'
-        uses: astral-sh/setup-uv@v6
+        uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9  # v9.0.0
         with:
           version: ${{ steps.uv_release.outputs.uv_version }}
       - name: 'Run code quality checks'
@@ -34,13 +42,15 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v4
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
+        with:
+          persist-credentials: false
       - name: 'Get uv release'
         id: uv_release
         run: |
-          echo uv_version=$(cat deps/uv_release) >> "${GITHUB_OUTPUT}"
+          echo "uv_version=$(cat deps/uv_release)" >> "${GITHUB_OUTPUT}"
       - name: 'Install uv'
-        uses: astral-sh/setup-uv@v6
+        uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9  # v9.0.0
         with:
           version: ${{ steps.uv_release.outputs.uv_version }}
       - name: 'Run unit tests'
@@ -50,105 +60,129 @@ jobs:
     needs: code-quality-checks
     name: 'Profiling'
     runs-on: [self-hosted, linux, normal]
+    permissions:
+      contents: read
+      packages: read
     timeout-minutes: 30
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v4
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
         with:
           fetch-depth: 0
+          persist-credentials: false
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
           container-name: kontrol-ci-profile-${{ github.sha }}
       - name: 'Build Kontrol'
         run: |
-            docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
+            docker exec -u github-user "kontrol-ci-profile-${GITHUB_SHA}" /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
       - name: 'Run profiling'
         run: |
           PROF_ARGS='--numprocesses=8'
-          docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} make profile PROF_ARGS="${PROF_ARGS}"
+          docker exec -u github-user "kontrol-ci-profile-${GITHUB_SHA}" make profile PROF_ARGS="${PROF_ARGS}"
       - name: 'Tear down Docker'
         if: always()
         run: |
-          docker stop --time=0 kontrol-ci-profile-${GITHUB_SHA}
+          # Best effort: the container does not exist if 'Set up Docker' failed, and a
+          # non-zero exit here would mask the step that actually failed.
+          docker stop --timeout=0 "kontrol-ci-profile-${GITHUB_SHA}" || true
 
   integration-tests:
     needs: code-quality-checks
     name: 'Integration Tests'
     runs-on: [self-hosted, linux, normal, fast]
+    permissions:
+      contents: read
+      packages: read
     timeout-minutes: 120
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v4
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
         with:
           fetch-depth: 0
+          persist-credentials: false
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
           container-name: kontrol-ci-integration-${{ github.sha }}
       - name: 'Build Kontrol'
         run: |
-            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
+            docker exec -u github-user "kontrol-ci-integration-${GITHUB_SHA}" /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
       - name: 'Run integration tests'
         run: |
           TEST_ARGS='-vv --force-sequential -k "not (test_kontrol_cse or test_foundry_minimize_proof or test_kontrol_end_to_end or test_kontrol_setup_storage or test_kontrol_counterexample_generation)" --numprocesses=3'
-          docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS="${TEST_ARGS}"
+          docker exec --user github-user "kontrol-ci-integration-${GITHUB_SHA}" make cov-integration TEST_ARGS="${TEST_ARGS}"
       - name: 'Tear down Docker'
         if: always()
         run: |
-          docker stop --time=0 kontrol-ci-integration-${GITHUB_SHA}
+          # Best effort: the container does not exist if 'Set up Docker' failed, and a
+          # non-zero exit here would mask the step that actually failed.
+          docker stop --timeout=0 "kontrol-ci-integration-${GITHUB_SHA}" || true
 
   cse-tests:
     needs: code-quality-checks
     name: 'CSE Tests'
     runs-on: [self-hosted, linux, normal, fast]
+    permissions:
+      contents: read
+      packages: read
     timeout-minutes: 120
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v4
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
         with:
           fetch-depth: 0
+          persist-credentials: false
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
           container-name: kontrol-ci-integration-${{ github.sha }}
       - name: 'Build Kontrol'
         run: |
-            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
+            docker exec -u github-user "kontrol-ci-integration-${GITHUB_SHA}" /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
       - name: 'Run CSE and Minimize tests'
         run: |
           TEST_ARGS='--numprocesses=5 --force-sequential -vv -k "test_kontrol_cse or test_foundry_minimize_proof"'
-          docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS="${TEST_ARGS}"
+          docker exec --user github-user "kontrol-ci-integration-${GITHUB_SHA}" make cov-integration TEST_ARGS="${TEST_ARGS}"
       - name: 'Tear down Docker'
         if: always()
         run: |
-          docker stop --time=0 kontrol-ci-integration-${GITHUB_SHA}
+          # Best effort: the container does not exist if 'Set up Docker' failed, and a
+          # non-zero exit here would mask the step that actually failed.
+          docker stop --timeout=0 "kontrol-ci-integration-${GITHUB_SHA}" || true
 
   end-to-end-tests:
     needs: code-quality-checks
     name: 'End to End Sanity Tests'
     runs-on: [self-hosted, linux, normal, fast]
+    permissions:
+      contents: read
+      packages: read
     timeout-minutes: 35
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v4
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
         with:
           fetch-depth: 0
+          persist-credentials: false
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
           container-name: kontrol-ci-integration-${{ github.sha }}
       - name: 'Build Kontrol'
         run: |
-            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
+            docker exec -u github-user "kontrol-ci-integration-${GITHUB_SHA}" /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
       - name: 'Run end-to-end tests'
         run: |
           TEST_ARGS='--numprocesses=6 -vv --force-sequential -k "test_kontrol_end_to_end or test_kontrol_setup_storage or test_kontrol_counterexample_generation"'
-          docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS="${TEST_ARGS}"
+          docker exec --user github-user "kontrol-ci-integration-${GITHUB_SHA}" make cov-integration TEST_ARGS="${TEST_ARGS}"
       - name: 'Tear down Docker'
         if: always()
         run: |
-          docker stop --time=0 kontrol-ci-integration-${GITHUB_SHA}
+          # Best effort: the container does not exist if 'Set up Docker' failed, and a
+          # non-zero exit here would mask the step that actually failed.
+          docker stop --timeout=0 "kontrol-ci-integration-${GITHUB_SHA}" || true
 
   docker:
     needs: code-quality-checks
@@ -157,50 +191,55 @@ jobs:
     timeout-minutes: 30
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v4
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
         with:
           fetch-depth: 0
+          persist-credentials: false
 
       - name: 'Set environment'
         run: |
-          echo "IMAGE_TAG=runtimeverificationinc/kontrol-${GITHUB_SHA}" >> ${GITHUB_ENV}
-          echo "CONTAINER_NAME=kontrol-ci-docker-${GITHUB_SHA}" >> ${GITHUB_ENV}
-          echo "DOCKER_USER=user" >> ${GITHUB_ENV}
-          echo "DOCKER_GROUP=user" >> ${GITHUB_ENV}
-          echo "FOUNDRY_ROOT=/home/user/foundry" >> ${GITHUB_ENV}
+          {
+            echo "IMAGE_TAG=runtimeverificationinc/kontrol-${GITHUB_SHA}"
+            echo "CONTAINER_NAME=kontrol-ci-docker-${GITHUB_SHA}"
+            echo "DOCKER_USER=user"
+            echo "DOCKER_GROUP=user"
+            echo "FOUNDRY_ROOT=/home/user/foundry"
+          } >> "${GITHUB_ENV}"
       - name: 'Build Docker image'
         run: |
           K_VERSION=$(cat deps/k_release)
           Z3_VERSION=$(cat deps/z3)
-          docker build . --tag ${IMAGE_TAG} --build-arg K_VERSION=${K_VERSION} --build-arg Z3_VERSION=${Z3_VERSION}
+          docker build . --tag "${IMAGE_TAG}" --build-arg K_VERSION="${K_VERSION}" --build-arg Z3_VERSION="${Z3_VERSION}"
       - name: 'Start Docker container'
         run: |
-          docker run                          \
-            --name ${CONTAINER_NAME}          \
-            --rm                              \
-            --interactive                     \
-            --tty                             \
-            --detach                          \
-            --user root                       \
-            ${IMAGE_TAG}
+          docker run                            \
+            --name "${CONTAINER_NAME}"          \
+            --rm                                \
+            --interactive                       \
+            --tty                               \
+            --detach                            \
+            --user root                         \
+            "${IMAGE_TAG}"
 
-          docker cp src/tests/integration/test-data/foundry ${CONTAINER_NAME}:${FOUNDRY_ROOT}
-          docker exec ${CONTAINER_NAME} chown -R ${DOCKER_USER}:${DOCKER_GROUP} ${FOUNDRY_ROOT}
+          docker cp src/tests/integration/test-data/foundry "${CONTAINER_NAME}":"${FOUNDRY_ROOT}"
+          docker exec "${CONTAINER_NAME}" chown -R "${DOCKER_USER}:${DOCKER_GROUP}" "${FOUNDRY_ROOT}"
       - name: 'Run forge build'
         run: |
-          docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} forge install --no-git foundry-rs/forge-std@75f1746
-          docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} forge install --no-git runtimeverification/kontrol-cheatcodes@a5dd4b0
-          docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} forge build
+          docker exec --user "${DOCKER_USER}" --workdir "${FOUNDRY_ROOT}" "${CONTAINER_NAME}" forge install --no-git foundry-rs/forge-std@75f1746
+          docker exec --user "${DOCKER_USER}" --workdir "${FOUNDRY_ROOT}" "${CONTAINER_NAME}" forge install --no-git runtimeverification/kontrol-cheatcodes@a5dd4b0
+          docker exec --user "${DOCKER_USER}" --workdir "${FOUNDRY_ROOT}" "${CONTAINER_NAME}" forge build
       - name: 'Run kontrol build'
-        run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol build -O2
+        run: docker exec --user "${DOCKER_USER}" --workdir "${FOUNDRY_ROOT}" "${CONTAINER_NAME}" kontrol build -O2
       - name: 'Run kontrol prove'
-        run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol prove --match-test 'AssertTest.test_assert_true()'
+        run: docker exec --user "${DOCKER_USER}" --workdir "${FOUNDRY_ROOT}" "${CONTAINER_NAME}" kontrol prove --match-test 'AssertTest.test_assert_true()'
       - name: 'Run kontrol show'
-        run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol show 'AssertTest.test_assert_true()'
+        run: docker exec --user "${DOCKER_USER}" --workdir "${FOUNDRY_ROOT}" "${CONTAINER_NAME}" kontrol show 'AssertTest.test_assert_true()'
       - name: 'Tear down Docker'
         if: always()
         run: |
-          docker stop --time=0 ${CONTAINER_NAME}
+          # Best effort: the container does not exist if 'Start Docker container' failed,
+          # and a non-zero exit here would mask the step that actually failed.
+          docker stop --timeout=0 "${CONTAINER_NAME}" || true
 
   nix:
     needs: code-quality-checks
@@ -208,29 +247,28 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        runner: [normal, MacM1]  # MacM1 / normal are self-hosted, 
+        runner: [normal, MacM1]  # MacM1 / normal are self-hosted
     runs-on: ${{ matrix.runner }}
     timeout-minutes: 60
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v4
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
         with:
           fetch-depth: 0
+          persist-credentials: false
 
+      # k-framework is a public cache, so it is declared as a substituter directly
+      # rather than through cachix-action. The `cachix` CLI validates whatever auth
+      # token is left in the runner's own config before it will register a cache, and
+      # a revoked token there fails the step even for a cache that needs no auth.
       - name: 'Install Nix'
         if: ${{ matrix.runner != 'MacM1' }}
-        uses: cachix/install-nix-action@v31.2.0
+        uses: cachix/install-nix-action@754537aaedb35f72ab11a60cc162c49ef3016495  # v31.2.0
         with:
           install_url: https://releases.nixos.org/nix/nix-2.31.0/install
           extra_nix_config: |
-            substituters = http://cache.nixos.org https://cache.iog.io
-            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= 
-
-      - name: 'Install Cachix'
-        if: ${{ matrix.runner != 'MacM1' }}
-        uses: cachix/cachix-action@v16
-        with:
-          name: k-framework
+            substituters = https://cache.nixos.org https://k-framework.cachix.org
+            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= k-framework.cachix.org-1:jeyMXB2h28gpNRjuVkehg+zLj62ma1RnyyopA/20yFE=
 
       - name: 'Build Kontrol'
         env:
@@ -240,8 +278,8 @@ jobs:
           set -euxo pipefail
           nix --version
           JQ=$(nix-build '<nixpkgs>' -A jq --no-link)/bin/jq
-          KONTROL_BIN=$(nix build .#kontrol.solc_0_8_13 --print-build-logs --json | $JQ -r '.[].outputs | to_entries[].value')/bin
-          echo $KONTROL_BIN >> $GITHUB_PATH
+          KONTROL_BIN=$(nix build .#kontrol.solc_0_8_13 --print-build-logs --json | "${JQ}" -r '.[].outputs | to_entries[].value')/bin
+          echo "${KONTROL_BIN}" >> "${GITHUB_PATH}"
 
       - name: 'Run smoke test'
         run: cd package && ./test-package.sh
diff --git a/.github/workflows/update-expected-output.yml b/.github/workflows/update-expected-output.yml
index 81d70045f..7a558c8e4 100644
--- a/.github/workflows/update-expected-output.yml
+++ b/.github/workflows/update-expected-output.yml
@@ -6,44 +6,56 @@ on:
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
+
+permissions:
+  contents: read
+
 jobs:
   update-output:
-    if: github.ref != 'refs/heads/master'
     name: 'Update Kontrol expected output'
     runs-on: [self-hosted, linux, normal, fast]
+    permissions:
+      contents: read
+      packages: read
     timeout-minutes: 180
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v4
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
         with:
           fetch-depth: 0
-          token: ${{ secrets.JENKINS_GITHUB_PAT }}
+          persist-credentials: false
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
           container-name: kontrol-ci-integration-${{ github.sha }}
       - name: 'Build Kontrol'
         run: |
-            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
+            docker exec -u github-user "kontrol-ci-integration-${GITHUB_SHA}" /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
       - name: 'Run integration tests'
         run: |
           TEST_ARGS="--maxfail=1000 --numprocesses=2 --update-expected-output --force-sequential -vv"
-          docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"not (test_kontrol_cse or test_foundry_minimize_proof or test_kontrol_end_to_end or test_kontrol_setup_storage or test_kontrol_counterexample_generation)\"' || true"
-          docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"test_kontrol_cse or test_foundry_minimize_proof\"' || true"
-          docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"test_kontrol_end_to_end or test_kontrol_setup_storage or test_kontrol_counterexample_generation\"' || true"
+          docker exec --user github-user "kontrol-ci-integration-${GITHUB_SHA}" bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"not (test_kontrol_cse or test_foundry_minimize_proof or test_kontrol_end_to_end or test_kontrol_setup_storage or test_kontrol_counterexample_generation)\"' || true"
+          docker exec --user github-user "kontrol-ci-integration-${GITHUB_SHA}" bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"test_kontrol_cse or test_foundry_minimize_proof\"' || true"
+          docker exec --user github-user "kontrol-ci-integration-${GITHUB_SHA}" bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"test_kontrol_end_to_end or test_kontrol_setup_storage or test_kontrol_counterexample_generation\"' || true"
       - name: 'Copy updated files to host'
         run: |
-          docker cp kontrol-ci-integration-${GITHUB_SHA}:/home/github-user/workspace/src/tests/integration/test-data/show ./src/tests/integration/test-data/
-      - name: 'Configure GitHub user'
-        run: |
-          git config user.name devops
-          git config user.email devops@runtimeverification.com
-      - name: 'Push golden files to branch'
-        run: |
-          git add ./src/tests/integration/test-data/show
-          git commit -m "Update expected output files"
-          git push
+          docker cp "kontrol-ci-integration-${GITHUB_SHA}":/home/github-user/workspace/src/tests/integration/test-data/show ./src/tests/integration/test-data/
+      # The regenerated files are published as an artifact rather than pushed back to
+      # the branch, so this workflow needs no write credential. Download it and commit
+      # the contents over src/tests/integration/test-data/show; see the README.
+      - name: 'Upload golden files'
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a  # v7.0.1
+        with:
+          name: expected-output
+          path: src/tests/integration/test-data/show
+          # Every test step above ends in `|| true`, so a run that produced nothing at
+          # all would otherwise upload an empty artifact and look like a success.
+          if-no-files-found: error
+          # Long enough for whoever dispatched the run to download and commit it.
+          retention-days: 7
       - name: 'Tear down Docker'
         if: always()
         run: |
-          docker stop --time=0 kontrol-ci-integration-${GITHUB_SHA}
+          # Best effort: the container does not exist if 'Set up Docker' failed, and a
+          # non-zero exit here would mask the step that actually failed.
+          docker stop --timeout=0 "kontrol-ci-integration-${GITHUB_SHA}" || true
diff --git a/.github/workflows/update-version.yml b/.github/workflows/update-version.yml
deleted file mode 100644
index 7f4b4b0ae..000000000
--- a/.github/workflows/update-version.yml
+++ /dev/null
@@ -1,81 +0,0 @@
----
-name: 'Update Version'
-on:
-  push:
-    branches:
-      - '_update-deps/runtimeverification/evm-semantics'
-      - '_update-deps/runtimeverification/rv-nix-tools'
-      - '_update-deps-cron/uv2nix'
-      - '_update-deps-cron/pyproject-build-systems'
-  workflow_dispatch:
-# Stop in progress workflows on the same branch and same workflow to use latest committed code
-concurrency:
-  group: ${{ github.workflow }}-${{ github.ref }}
-  cancel-in-progress: true
-
-jobs:
-  update-versions:
-    name: 'Update Dependency Versions'
-    runs-on: ubuntu-latest
-    steps:
-      - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          submodules: recursive
-          token: ${{ secrets.JENKINS_GITHUB_PAT }}
-          fetch-depth: 0
-      - name: 'Configure GitHub user'
-        run: |
-          git config user.name devops
-          git config user.email devops@runtimeverification.com
-      - name: 'Install Nix'
-        uses: cachix/install-nix-action@v31.2.0
-        with:
-          install_url: https://releases.nixos.org/nix/nix-2.31.0/install
-          extra_nix_config: |
-            substituters = http://cache.nixos.org https://cache.iog.io
-            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= 
-            access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
-      - uses: cachix/cachix-action@v16
-        with:
-          name: k-framework
-          authToken: ${{ secrets.CACHIX_PUBLIC_TOKEN }}
-      # note: we install the same version of `uv` as used by `uv2nix` in order to match the nix derivation
-      - name: 'Update uv release tag'
-        id: uv_release
-        run: |
-          UV2NIX_VERSION=$(cat deps/uv2nix)
-          UV_VERSION=$(curl -s https://raw.githubusercontent.com/pyproject-nix/uv2nix/$(cat deps/uv2nix)/pkgs/uv-bin/srcs.json | jq -r .version)
-          [[ "$UV_VERSION" =~ ^[0-9]+\.[0-9]+\.[0-9]+$ ]]
-          echo $UV_VERSION > deps/uv_release
-          git add deps/uv_release && git commit -m "Sync uv version: uv ${UV_VERSION}" || true
-          echo uv_version=$UV_VERSION >> "${GITHUB_OUTPUT}"
-      - name: 'Install uv'
-        uses: astral-sh/setup-uv@v6
-        with:
-          version: ${{ steps.uv_release.outputs.uv_version }}
-      - name: 'Update kevm-pyk release tag'
-        run: |
-          KEVM_VERSION="$(cat deps/kevm_release)"
-          sed -i 's!    "kevm-pyk@git+https://github.com/runtimeverification/evm-semantics.git@[v0-9\.]*#subdirectory=kevm-pyk"!    "kevm-pyk@git+https://github.com/runtimeverification/evm-semantics.git@v'${KEVM_VERSION}'#subdirectory=kevm-pyk"!' pyproject.toml
-          uv lock --upgrade
-          git add -u && git commit -m "Sync uv files: kevm-pyk version ${KEVM_VERSION}" || true
-      - name: 'Update K release file'
-        run: |
-          K_VERSION=$(uv run python3 -c 'import pyk; print(pyk.__version__)')
-          echo ${K_VERSION} > deps/k_release
-          git add deps/k_release && git commit -m "deps/k_release: sync release file version ${K_VERSION}" || true
-      - name: 'Update Nix flake inputs'
-        run: |
-          KEVM_VERSION=$(cat deps/kevm_release)
-          UV2NIX_VERSION=$(cat deps/uv2nix)
-          PYPROJECT_BUILD_SYSTEMS_VERSION=$(cat deps/pyproject-build-systems)
-          RV_NIX_TOOLS_VERSION=$(cat deps/rv-nix-tools)
-          sed -i 's!    kevm.url = "github:runtimeverification/evm-semantics/[v0-9\.]*"!    kevm.url = "github:runtimeverification/evm-semantics/v'"${KEVM_VERSION}"'"!' flake.nix
-          sed -i 's!    uv2nix.url = "github:pyproject-nix/uv2nix/[a-z0-9\.]*"!    uv2nix.url = "github:pyproject-nix/uv2nix/'"${UV2NIX_VERSION}"'"!' flake.nix
-          sed -i 's!    pyproject-build-systems.url = "github:pyproject-nix/build-system-pkgs/[a-z0-9\.]*"!    pyproject-build-systems.url = "github:pyproject-nix/build-system-pkgs/'"${PYPROJECT_BUILD_SYSTEMS_VERSION}"'"!' flake.nix
-          sed -i 's!    rv-nix-tools.url = "github:runtimeverification/rv-nix-tools/[a-z0-9\.]*"!    rv-nix-tools.url = "github:runtimeverification/rv-nix-tools/'"${RV_NIX_TOOLS_VERSION}"'"!' flake.nix
-          nix flake update
-          git add flake.nix flake.lock && git commit -m 'flake.{nix,lock}: update Nix derivations' || true
-      - name: 'Push updates'
-        run: git push
diff --git a/CLAUDE.md b/CLAUDE.md
index 0d8458a3d..12ee6ed40 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -107,16 +107,18 @@ uv run pytest src/tests/integration/test_foundry_prove.py -v \
 ```
 
 CI (`.github/workflows/test-pr.yml`) partitions integration tests into four self-hosted jobs by `-k` filter to balance load — **Integration** (everything except the named groups), **CSE** (`test_kontrol_cse or test_foundry_minimize_proof`), **End-to-End** (`test_kontrol_end_to_end or test_kontrol_setup_storage or test_kontrol_counterexample_generation`), and **Profiling** — so adding a test to one of those named groups changes which job runs it.
+`.github/workflows/lint-workflows.yml` runs `actionlint` and `zizmor` over `.github/` on every PR; run both locally before touching a workflow.
+`.github/actionlint.yaml` declares the self-hosted runner labels (`normal`, `fast`, `MacM1`) that actionlint cannot discover on its own.
 
 ## Dependencies, versioning, and packaging
 
 `deps/` pins exact upstream versions, each file consumed by the build/CI:
 
 - `deps/k_release` (K framework), `deps/kevm_release` (KEVM/evm-semantics), `deps/z3`, `deps/uv_release` — version strings read by the Dockerfiles, CI workflows, and Nix inputs.
-- `deps/kevm_release` must match the `kevm-pyk@…@vX.Y.Z` git ref in `pyproject.toml`; the `_update-deps/*` automation (`.github/workflows/update-version.yml`) keeps `deps/*`, `pyproject.toml`, `flake.nix`, and `uv.lock` in sync and runs `uv lock --upgrade` + `nix flake update`.
+- `deps/kevm_release` must match the `kevm-pyk@…@vX.Y.Z` git ref in `pyproject.toml`; keeping `deps/*`, `pyproject.toml`, `flake.nix`, and `uv.lock` in sync (`uv lock --upgrade` + `nix flake update`) is currently a manual step — the `_update-deps/*` automation was removed along with the rest of the secret-using CD.
 
 The Kontrol version is `package/version` (plain text), mirrored in `src/kontrol/__init__.py` (`VERSION`) and `pyproject.toml`; `package/version.sh bump`/`sub` increments and propagates it.
-Pushing the `release` branch triggers `.github/workflows/release.yml`: draft GitHub release → build `.#kontrol` and publish to the `k-framework` (public) and `k-framework-binary` (private) Cachix caches via `kup publish` → build+push the Docker image → finalize.
+There is no release automation in this repo at the moment: version bumping, the GitHub release, the Cachix pushes, and the Docker Hub image are all done outside CI until the release workflow is reinstated.
 
 Nix: `flake.nix` exports `.#kontrol` (default) built through a uv2nix layering (`nix/kontrol-pyk-pyproject` → `nix/kontrol-pyk` → `nix/kontrol`).
 solc-pinned variants are exposed as passthru attributes — `.#kontrol.solc_0_8_13`, `.#kontrol.solc_0_8_15`, `.#kontrol.solc_0_8_22` (defined in `nix/kontrol/default.nix`); CI's Nix job builds `solc_0_8_13`.
diff --git a/README.md b/README.md
index 887d4d357..de06c2c8f 100644
--- a/README.md
+++ b/README.md
@@ -75,19 +75,17 @@ To update the expected output of the tests, use the `--update-expected-output` f
 make cov-integration TEST_ARGS="--numprocesses=8 --update-expected-output"
 ```
 
-### Build Development Kontrol Image with Fixed Upstream Dependencies
---------------------------------
-Relevant to this workflow [kontrol-push-fixed-deps.yml](.github/workflows/kontrol-push-fixed-deps.yml)
->This is relevant for internal development to publish development images of Kontrol with modified Kontrol changes and retain fixed upstream dependencies.
-The use case for this workflow is intended to facilitate testing changes to Kontrol needed for use in testing CI or in other downstream workflows without needing to publish changes or PRs first.
-
-The intent is to reduce the friction of needing custom builds and avoiding lengthy upstream changes and PRs.
+The full run takes hours, so the `Update Expected Output` workflow can do it on a CI runner instead.
+Dispatch it against your branch, then apply the result:
+```sh
+gh run download <run-id> --name expected-output --dir src/tests/integration/test-data/show
+git add src/tests/integration/test-data/show && git commit -m 'Update expected output files'
+```
+The artifact expires after 7 days.
 
 ### Build Kontrol with Kup and Specific Dependency Overrides
 --------------------------------
-Relevant to this workflow [kup-build-kontrol.yml](.github/workflows/kontrol-push-unfixed-deps.yml)
-> This is relevant for internal development to publish development images of Kontrol for use in KaaS or a dockerized test environment.
-Use the workflow [Kup Build Kontrol](.github/workflows/kup-build-kontrol.yml) to publish a custom version of Kontrol for use in CI and [KaaS](https://kaas.runtimeverification.com/).
+> This is relevant for internal development to build a custom version of Kontrol against unreleased upstream dependencies.
 [See KUP docs for more information](https://github.com/runtimeverification/kup/blob/master/src/kup/install-help.md#kup-install----override)
 
 #### Using Kup 
@@ -126,25 +124,6 @@ Now run a build using kup and specific dependency overrides:
 
 > **Note**: It's important that you use the short-rev hash or the long for specific revisions of the dependencies to modify. 
 
-#### Using the workflow to publish to ghcr.io/runtimeverification
---------------------------------
-
-#### Running the workflow
-- Go to repo [Kontrol Actions Page](https://github.com/runtimeverification/kontrol/actions) 
-- Click on "Push Kontrol w/ Dependencies" from the left hand list 
-- Click on "Run Workflow" on the top right corner of the list of workflow runs is an option "Run Workflow".
-- Use the 'master' branch unless you're doing something special.
-- Input the override hash strings for specific dependencies to override in kontrol. See below on how to find the hash for the dependency.
-- Then click "Run Workflow" and a job will start.
-- The workflow summary shows the name of the image that was built and pushed e.g. ghcr.io/runtimeverification/kontrol-custom:tag 
-
-> **Note**: The tag will be a randomly generated string.
-
-[The workflow](.github/workflows/kontrol-push-unfixed-deps.yml) takes multiple inputs to override the various components of kontrol. Those overrides are listed above in the example output of 'kup list kontrol --inputs' 
-
-To set the desired revisions of the dependencies. Find the associated hash on the branch and commit made to be used for the dependnecy override. 
-If an input is left blank, the workflow will workout the default hash to use based on kontrols latest release. 
-
 Example to fetch the desired hash to insert a different dependency version into the kontrol build.
 Substitude the k-framework revision used to build kontrol.
 ```