From d862f55df104c33caeb66ed47ed18ec8e22d4fdc Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Wed, 12 Aug 2026 15:42:53 +0300
Subject: [PATCH 1/8] .github/workflows, .github/scripts, README.md, CLAUDE.md:
 remove secret-using CD

Ports the CD half of runtimeverification/evm-semantics#2878.

CD is removed rather than converted: version bumping, release cutting, Cachix
publishing, the Docker Hub and ghcr.io image pushes, and the dependency-bump
automation all read repository secrets. Release automation is reinstated in a
follow-up PR, so until then dependency syncing and releases are manual.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 .github/scripts/check-cachix-pin.sh           |  99 -----------
 .github/workflows/kontrol-push-fixed-deps.yml |  80 ---------
 .../workflows/kontrol-push-unfixed-deps.yml   |  74 --------
 .github/workflows/master-push.yml             |  56 ------
 .github/workflows/release.yml                 | 165 ------------------
 .github/workflows/update-version.yml          |  81 ---------
 CLAUDE.md                                     |   5 +-
 README.md                                     |  31 +---
 8 files changed, 3 insertions(+), 588 deletions(-)
 delete mode 100755 .github/scripts/check-cachix-pin.sh
 delete mode 100644 .github/workflows/kontrol-push-fixed-deps.yml
 delete mode 100644 .github/workflows/kontrol-push-unfixed-deps.yml
 delete mode 100644 .github/workflows/master-push.yml
 delete mode 100644 .github/workflows/release.yml
 delete mode 100644 .github/workflows/update-version.yml

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/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/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/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..49de83201 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -107,16 +107,15 @@ 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.
-
 ## 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..3b3ea2fe4 100644
--- a/README.md
+++ b/README.md
@@ -75,19 +75,9 @@ 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.
-
 ### 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 +116,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.
 ```

From 6fce218283f5bc45f4f77e0f01867094e13b5bf3 Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Wed, 12 Aug 2026 15:43:06 +0300
Subject: [PATCH 2/8] .github/actions/with-docker,
 .github/workflows/Dockerfile: pass inputs via env

Composite action inputs were interpolated straight into the shell script, which
is a template-injection surface on self-hosted runners; they now arrive as env
vars and every expansion is quoted. Drops the subdir/os/distro inputs and the
BASE_DISTRO build arg, which nothing read, and the `type:` keys, which are not
valid on composite action inputs.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 .github/actions/with-docker/action.yml | 77 +++++++++-----------------
 .github/workflows/Dockerfile           |  1 -
 2 files changed, 27 insertions(+), 51 deletions(-)

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

From 93b55cb9db8725202e95d74c087a0247bf5d70b7 Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Wed, 12 Aug 2026 15:43:12 +0300
Subject: [PATCH 3/8] .github/workflows/test-pr.yml: pin actions to SHAs,
 restrict token permissions

Pins every action to a commit SHA with a version comment, sets a read-only
workflow token (plus packages:read on the jobs that pull ghcr.io/foundry-rs/
foundry), and stops persisting credentials in the checkout.

Docker teardown becomes `docker stop --timeout=0 ... || true` so a container
that was never created cannot mask the step that actually failed.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 .github/workflows/test-pr.yml | 147 ++++++++++++++++++++++------------
 1 file changed, 94 insertions(+), 53 deletions(-)

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index 2a74d3d6d..0b249c32e 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}" makeprofile 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}" makecov-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}" makecov-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}" makecov-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,27 +247,29 @@ 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
 
       - 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= 
+            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
 
+      # Read-only use of the public k-framework cache; no auth token, so no secret.
       - name: 'Install Cachix'
         if: ${{ matrix.runner != 'MacM1' }}
-        uses: cachix/cachix-action@v16
+        uses: cachix/cachix-action@3ba601ff5bbb07c7220846facfa2cd81eeee15a1  # v16
         with:
           name: k-framework
 
@@ -240,8 +281,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

From f1845f7b143ff7f213617f62e958b9eb93f5a42b Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Wed, 12 Aug 2026 15:43:25 +0300
Subject: [PATCH 4/8] .github/workflows/update-expected-output.yml, README.md:
 publish golden files as an artifact

The job pushed the regenerated files straight to the branch, which required a
push-capable PAT. Since it checks out and runs the dispatched branch's own
composite action in the same job, anyone with write access could exfiltrate
that PAT; it was also the last secret left in the repository.

The files now go up via actions/upload-artifact with a 7-day retention, and the
README documents the download-and-commit step. `if-no-files-found: error` guards
against a silently empty upload, since every test step here ends in `|| true`.

Drops the `github.ref != master` guard along with the push it protected.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 .github/workflows/update-expected-output.yml | 48 ++++++++++++--------
 README.md                                    |  8 ++++
 2 files changed, 38 insertions(+), 18 deletions(-)

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/README.md b/README.md
index 3b3ea2fe4..de06c2c8f 100644
--- a/README.md
+++ b/README.md
@@ -75,6 +75,14 @@ To update the expected output of the tests, use the `--update-expected-output` f
 make cov-integration TEST_ARGS="--numprocesses=8 --update-expected-output"
 ```
 
+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
 --------------------------------
 > This is relevant for internal development to build a custom version of Kontrol against unreleased upstream dependencies.

From b9fa5ce042289f5b4faf005ed24e5e9be30a31fa Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Wed, 12 Aug 2026 15:43:33 +0300
Subject: [PATCH 5/8] .github/actionlint.yaml,
 .github/workflows/lint-workflows.yml, CLAUDE.md: add workflow linting

Runs actionlint and zizmor over .github/ on every PR, so the SHA pinning and
permission scoping added in this branch stay enforced. The actionlint release is
pinned by version and verified by checksum; actionlint.yaml declares the
self-hosted runner labels it cannot discover on its own.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 .github/actionlint.yaml              |  6 ++++
 .github/workflows/lint-workflows.yml | 53 ++++++++++++++++++++++++++++
 CLAUDE.md                            |  3 ++
 3 files changed, 62 insertions(+)
 create mode 100644 .github/actionlint.yaml
 create mode 100644 .github/workflows/lint-workflows.yml

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/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/CLAUDE.md b/CLAUDE.md
index 49de83201..12ee6ed40 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -107,6 +107,9 @@ 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:

From d7d8b2a8e2c9c6bd34e9f31a18844ec07a3fdf5f Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Wed, 12 Aug 2026 16:13:28 +0300
Subject: [PATCH 6/8] test-pr.yml: fix typo

---
 .github/workflows/test-pr.yml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index 0b249c32e..0ba3e0194 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -112,7 +112,7 @@ jobs:
       - 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}" makecov-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: |
@@ -144,7 +144,7 @@ jobs:
       - 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}" makecov-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: |
@@ -176,7 +176,7 @@ jobs:
       - 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}" makecov-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: |

From 2a539a26ba359f1a15502140ab656469e5c23490 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andrei=20V=C4=83caru?=
 <16517508+anvacaru@users.noreply.github.com>
Date: Wed, 12 Aug 2026 16:19:26 +0300
Subject: [PATCH 7/8] Update .github/workflows/test-pr.yml
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
---
 .github/workflows/test-pr.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index 0ba3e0194..29e4a1271 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -80,7 +80,7 @@ jobs:
       - name: 'Run profiling'
         run: |
           PROF_ARGS='--numprocesses=8'
-          docker exec -u github-user "kontrol-ci-profile-${GITHUB_SHA}" makeprofile 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: |

From ec4a1e8df1fb45ec7473b9b10729f82ba476f5b1 Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Wed, 12 Aug 2026 16:37:02 +0300
Subject: [PATCH 8/8] .github/workflows/test-pr.yml: declare k-framework cache
 as a substituter

cachix-action failed on the self-hosted runner with "Cachix Auth token
CACHIX_WEB_PRIVATE_TOKEN has been revoked": the cachix CLI validates whatever
token is left in the runner's own config before registering a cache, so leftover
state from the removed CD workflows broke a step that passes no token at all.

k-framework is public, so the cache is declared directly in extra_nix_config and
the CLI drops out of the path. Also drops cache.iog.io, which could never be used
because its public key was not in trusted-public-keys, and switches cache.nixos.org
to https.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 .github/workflows/test-pr.yml | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index 29e4a1271..a19e14fe2 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -257,21 +257,18 @@ jobs:
           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@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=
-
-      # Read-only use of the public k-framework cache; no auth token, so no secret.
-      - name: 'Install Cachix'
-        if: ${{ matrix.runner != 'MacM1' }}
-        uses: cachix/cachix-action@3ba601ff5bbb07c7220846facfa2cd81eeee15a1  # 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: