diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index 3b2a1cdc4f..7eae5bcee0 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -309,205 +309,6 @@ jobs:
           path: |
             **/kore-exec.tar.gz
 
-  macos-build:
-    name: 'Build MacOS Package'
-    runs-on: macos-latest
-    timeout-minutes: 120
-    environment: production
-    needs: [set-release-id, source-tarball]
-    continue-on-error: true # Do not fail releases due to MacOS builds at this time. Oct. 6, 2025
-    steps:
-      - name: Check out code
-        uses: actions/checkout@v4
-        with:
-          submodules: recursive
-          path: kframework
-
-      - name: Check out matching homebrew repo branch
-        uses: actions/checkout@v4
-        id: checkout
-        with:
-          repository: runtimeverification/homebrew-k
-          path: homebrew-k
-          ref: staging
-        continue-on-error: true
-
-      - name: Check out homebrew repo master branch
-        uses: actions/checkout@v4
-        if: ${{ steps.checkout.outcome == 'failure' }}
-        with:
-          repository: runtimeverification/homebrew-k
-          path: homebrew-k
-
-      - name: Cache maven
-        uses: actions/cache@v4
-        with:
-          path: ~/.m2/repository
-          key: ${{ runner.os }}-maven-${{ hashFiles('**/pom.xml') }}-
-          restore-keys: |
-            ${{ runner.os }}-maven-
-
-      - name: Mac Dependencies
-        run: |
-          # Via: https://github.com/ledger/ledger/commit/1eec9f86667cad3b0bbafb82a83739a0d30ca09f
-          # Unlink and re-link to prevent errors when github mac runner images
-          # install python outside of brew, for example:
-          # https://github.com/orgs/Homebrew/discussions/3895
-          # https://github.com/actions/setup-python/issues/577
-          # https://github.com/actions/runner-images/issues/6459
-          # https://github.com/actions/runner-images/issues/6507
-          # https://github.com/actions/runner-images/issues/2322
-
-          # shellcheck disable=SC2162
-          brew list -1 | grep python | while read formula; do brew unlink "$formula"; brew link --overwrite "$formula"; done
-
-          # uninstall pre-installed cmake
-          brew uninstall cmake
-
-      - name: Build brew bottle
-        id: build
-        env:
-          HOMEBREW_NO_INSTALLED_DEPENDENTS_CHECK: 1
-          MAVEN_OPTS: >-
-              -Dhttp.keepAlive=false
-              -Dmaven.wagon.http.pool=false
-              -Dmaven.wagon.httpconnectionManager.ttlSeconds=30
-        run: |
-          PACKAGE=kframework
-          VERSION=$(cat kframework/package/version)
-          ROOT_URL='https://github.com/runtimeverification/k/releases/download'
-          wget "$ROOT_URL/v${VERSION}/kframework-${VERSION}-src.tar.gz"
-          cd homebrew-k
-          ../kframework/package/macos/brew-update-to-local "${PACKAGE}" "${VERSION}"
-          git commit "Formula/$PACKAGE.rb" -m "Update ${PACKAGE} to ${VERSION}: part 1"
-          ../kframework/package/macos/brew-build-and-update-to-local-bottle "${PACKAGE}" "${VERSION}" "${ROOT_URL}"
-          git reset HEAD^
-          LOCAL_BOTTLE_NAME=$(basename "$(find . -name "kframework--${VERSION}.arm64_sonoma.bottle*.tar.gz")")
-          # shellcheck disable=2001
-          BOTTLE_NAME=$(echo "${LOCAL_BOTTLE_NAME#./}" | sed 's!kframework--!kframework-!')
-          ../kframework/package/macos/brew-update-to-final "${PACKAGE}" "${VERSION}" "${ROOT_URL}"
-          echo "path=${LOCAL_BOTTLE_NAME}" >> "${GITHUB_OUTPUT}"
-          echo "path_remote=${BOTTLE_NAME}" >> "${GITHUB_OUTPUT}"
-
-      - name: Upload bottle
-        uses: actions/upload-artifact@v4
-        with:
-          name: homebrew
-          path: homebrew-k
-
-    outputs:
-      bottle_path: ${{ steps.build.outputs.path }}
-      bottle_path_remote: ${{ steps.build.outputs.path_remote }}
-
-  macos-test:
-    name: 'Test MacOS Package'
-    runs-on: macos-latest
-    timeout-minutes: 60
-    environment: production
-    needs: [macos-build, set-release-id]
-    continue-on-error: true # Do not fail releases due to MacOS tests at this time. Oct. 6, 2025
-    steps:
-      - name: 'Check out matching homebrew repo branch'
-        uses: actions/checkout@v4
-        id: checkout
-        with:
-          repository: runtimeverification/homebrew-k
-          token: ${{ secrets.JENKINS_GITHUB_PAT }}
-          path: homebrew-k
-          ref: staging
-        continue-on-error: true
-
-      - name: 'Check out homebrew repo master branch'
-        uses: actions/checkout@v4
-        if: ${{ steps.checkout.outcome == 'failure' }}
-        with:
-          repository: runtimeverification/homebrew-k
-          token: ${{ secrets.JENKINS_GITHUB_PAT }}
-          path: homebrew-k
-
-      - name: 'Download bottle'
-        uses: actions/download-artifact@v4
-        with:
-          name: homebrew
-          path: homebrew-k-old
-
-      - name: Mac Dependencies
-        run: |
-          # Via: https://github.com/ledger/ledger/commit/1eec9f86667cad3b0bbafb82a83739a0d30ca09f
-          # Unlink and re-link to prevent errors when github mac runner images
-          # install python outside of brew, for example:
-          # https://github.com/orgs/Homebrew/discussions/3895
-          # https://github.com/actions/setup-python/issues/577
-          # https://github.com/actions/runner-images/issues/6459
-          # https://github.com/actions/runner-images/issues/6507
-          # https://github.com/actions/runner-images/issues/2322
-
-          # shellcheck disable=SC2162
-          brew list -1 | grep python | while read formula; do brew unlink "$formula"; brew link --overwrite "$formula"; done
-
-      - name: 'Test brew bottle'
-        id: test
-        env:
-          # github actions sets the JAVA_HOME variable to Java 8 explicitly for
-          # some reason. There doesn't seem to be a way to tell it to unset the
-          # variable, so instead we just have to tell it to use Java 17
-          # explicitly instead.
-          JAVA_HOME: ${{ env.JAVA_HOME_17_X64 }}
-          HOMEBREW_NO_INSTALLED_DEPENDENTS_CHECK: 1
-        run: |
-          # The macOS public runners are prone to flakiness when running this
-          # test suite, so the PL-tutorial is disabled for now.
-          #   - https://github.com/runtimeverification/k/issues/3705
-          cd homebrew-k-old
-          # brew tap expects a git repository, so we initialise the current folder as a dummy repo
-          git init
-          brew tap runtimeverification/k "file:///$(pwd)"
-          # Install the formula using the local bottle file
-          # First, check what files are available
-          ls -la
-          # Try to install using the bottle file pattern like the original script
-          brew install kframework--*.bottle*.tar.gz -v
-          # cp -R /usr/local/share/kframework/pl-tutorial ~
-          # WD=`pwd`
-          # cd
-          # echo 'Starting kserver...'
-          # spawn-kserver $WD/kserver.log
-          # cd pl-tutorial
-          # echo 'Testing tutorial in user environment...'
-          # make -j`sysctl -n hw.ncpu` ${MAKE_EXTRA_ARGS}
-          # cd ~
-          echo 'module TEST imports BOOL endmodule' > test.k
-          kompile test.k --backend llvm
-          kompile test.k --backend haskell
-
-      - name: 'Check out code'
-        uses: actions/checkout@v4
-        with:
-          path: k-homebrew-checkout
-          token: ${{ secrets.JENKINS_GITHUB_PAT }}
-
-      - name: 'Upload Package to Release'
-        env:
-          GITHUB_TOKEN: ${{ secrets.JENKINS_GITHUB_PAT }}
-          BOTTLE_NAME: ${{ needs.macos-build.outputs.bottle_path }}
-          REMOTE_BOTTLE_NAME: ${{ needs.macos-build.outputs.bottle_path_remote }}
-        run: |
-          set -x
-          version=$(cat k-homebrew-checkout/package/version)
-          mv "homebrew-k-old/${BOTTLE_NAME}" "homebrew-k-old/${REMOTE_BOTTLE_NAME}"
-          gh release upload --repo runtimeverification/k --clobber "v${version}" "homebrew-k-old/${REMOTE_BOTTLE_NAME}"
-
-      - run: |
-          git config --global user.name rv-jenkins
-          git config --global user.email devops@runtimeverification.com
-
-      - name: 'Commit changes'
-        run: |
-          cp homebrew-k-old/Formula/kframework.rb homebrew-k/Formula/kframework.rb
-          cd homebrew-k
-          git commit -m 'Update brew package version' Formula/kframework.rb
-          git push origin master
-
   release:
     name: 'Publish Release'
     runs-on: [self-hosted, linux, normal]
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index c6885a201b..031ba5ac84 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -337,128 +337,4 @@ jobs:
           docker stop --time=0 k-pyk-regression-${{ github.sha }}
 
 
-  test-macos-build:
-    name: 'K: macOS Build & Test'
-    runs-on: macos-15
-    timeout-minutes: 60
-    needs: code-quality
-    continue-on-error: true # Do not fail PRs due to MacOS builds at this time. Oct. 6, 2025
-    steps:
-      - name: 'Set up Java 17'
-        uses: actions/setup-java@v4
-        with:
-          distribution: 'zulu'
-          java-version: 17
-
-      - name: 'Check out code'
-        uses: actions/checkout@v4
-        with:
-          submodules: recursive
-          path: kframework
-
-      - name: 'Check out homebrew repo'
-        uses: actions/checkout@v4
-        with:
-          repository: runtimeverification/homebrew-k
-          path: homebrew-k
-          ref: master
-
-      - name: 'Mac Dependencies'
-        run: |
-          # Via: https://github.com/ledger/ledger/commit/1eec9f86667cad3b0bbafb82a83739a0d30ca09f
-          # Unlink and re-link to prevent errors when github mac runner images
-          # install python outside of brew, for example:
-          # https://github.com/orgs/Homebrew/discussions/3895
-          # https://github.com/actions/setup-python/issues/577
-          # https://github.com/actions/runner-images/issues/6459
-          # https://github.com/actions/runner-images/issues/6507
-          # https://github.com/actions/runner-images/issues/2322
-
-          # shellcheck disable=SC2162
-          brew list -1 | grep python | while read formula; do brew unlink "$formula"; brew link --overwrite "$formula"; done
-
-          # uninstall pre-installed cmake
-          brew uninstall cmake
-
-      - name: 'Build brew bottle'
-        id: build
-        env:
-          HOMEBREW_NO_INSTALLED_DEPENDENTS_CHECK: 1
-          MAVEN_OPTS: >-
-              -Dhttp.keepAlive=false
-              -Dmaven.wagon.http.pool=false
-              -Dmaven.wagon.httpconnectionManager.ttlSeconds=30
-        run: |
-          PACKAGE=kframework
-          VERSION=$(cat kframework/package/version)
-          ROOT_URL='https://github.com/runtimeverification/k/releases/download'
-          
-          # For PR testing, we'll use the latest available source tarball
-          # or create a test tarball from the current code
-          if [ -f "$ROOT_URL/v${VERSION}/kframework-${VERSION}-src.tar.gz" ]; then
-            wget "$ROOT_URL/v${VERSION}/kframework-${VERSION}-src.tar.gz"
-          else
-            # Create a test tarball from current code for PR testing
-            echo "Creating test tarball for PR testing..."
-            tar czf "kframework-${VERSION}-src.tar.gz" --exclude='.git' --exclude='homebrew-k' .
-          fi
-          
-          cd homebrew-k
-          ../kframework/package/macos/brew-update-to-local "${PACKAGE}" "${VERSION}"
-          git commit "Formula/$PACKAGE.rb" -m "Update ${PACKAGE} to ${VERSION}: part 1"
-          ../kframework/package/macos/brew-build-and-update-to-local-bottle "${PACKAGE}" "${VERSION}" "${ROOT_URL}"
-          git reset HEAD^
-          LOCAL_BOTTLE_NAME=$(basename "$(find . -name "kframework--${VERSION}.arm64_sonoma.bottle*.tar.gz")")
-          # shellcheck disable=2001
-          BOTTLE_NAME=$(echo "${LOCAL_BOTTLE_NAME#./}" | sed 's!kframework--!kframework-!')
-          ../kframework/package/macos/brew-update-to-final "${PACKAGE}" "${VERSION}" "${ROOT_URL}"
-          echo "path=${LOCAL_BOTTLE_NAME}" >> "${GITHUB_OUTPUT}"
-          echo "path_remote=${BOTTLE_NAME}" >> "${GITHUB_OUTPUT}"
-
-      - name: 'Upload bottle'
-        uses: actions/upload-artifact@v4
-        with:
-          name: homebrew-bottle
-          path: homebrew-k
-          retention-days: 1
-
-      - name: 'Test Homebrew formula validation'
-        id: test
-        env:
-          # github actions sets the JAVA_HOME variable to Java 8 explicitly for
-          # some reason. There doesn't seem to be a way to tell it to unset the
-          # variable, so instead we just have to tell it to use Java 17
-          # explicitly instead.
-          JAVA_HOME: ${{ env.JAVA_HOME_17_X64 }}
-          HOMEBREW_NO_INSTALLED_DEPENDENTS_CHECK: 1
-          MAVEN_OPTS: >-
-            -Dhttp.keepAlive=false
-            -Dmaven.wagon.http.pool=false
-            -Dmaven.wagon.httpconnectionManager.ttlSeconds=30
-        run: |
-          # Test the Homebrew formula validation and basic functionality
-          cd homebrew-k
-          
-          # Remove any existing tap to avoid remote mismatch errors
-          brew untap runtimeverification/k 2>/dev/null || true
-          
-          # Validate the formula syntax by installing it as a local tap
-          brew tap runtimeverification/k "file://$(pwd)"
-          
-          # Test formula installation from source
-          brew install --build-from-source kframework -v
-          
-          # Basic functionality test
-          echo 'module TEST imports BOOL endmodule' > test.k
-          kompile test.k --backend llvm
-          kompile test.k --backend haskell
-          echo "✅ macOS build and test completed successfully"
-
-      - name: 'Upload formula for debugging'
-        if: always()
-        uses: actions/upload-artifact@v4
-        with:
-          name: macos-formula-test
-          path: homebrew-k/Formula/kframework.rb
-          retention-days: 1
 
diff --git a/CODEOWNERS b/CODEOWNERS
index 6491746213..34e72ee235 100644
--- a/CODEOWNERS
+++ b/CODEOWNERS
@@ -1,3 +1,3 @@
-/k-distribution/include/kframework/builtin/* @palinatolmach @tothtamas28
+/k-distribution/include/kframework/builtin/* @palinatolmach @tothtamas28 @ehildenb
 /.github/workflows/* @runtimeverification/admin
-/package/version @palinatolmach @rv-jenkins @F-WRunTime @tothtamas28
+/package/version @palinatolmach @rv-jenkins @tothtamas28
diff --git a/package/macos/brew-build-and-update-to-local-bottle b/package/macos/brew-build-and-update-to-local-bottle
deleted file mode 100755
index d1aaccd285..0000000000
--- a/package/macos/brew-build-and-update-to-local-bottle
+++ /dev/null
@@ -1,11 +0,0 @@
-#!/bin/sh -exu
-package="$1"  ; shift
-version="$1"  ; shift
-root_url="$1" ; shift
-brew update
-brew tap runtimeverification/k "file://$(pwd)"
-brew install $package --build-bottle -v
-brew bottle --json $package --root-url="$root_url/v$version/"
-cat *.bottle.json
-brew bottle --merge --write --no-commit *.bottle.json
-cp $(brew formula $package) Formula/$package.rb
diff --git a/package/macos/brew-install-bottle b/package/macos/brew-install-bottle
deleted file mode 100755
index 9e6b213b34..0000000000
--- a/package/macos/brew-install-bottle
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/bin/sh -ex
-package="$1" ; shift
-version="$1" ; shift
-brew tap runtimeverification/k "file:///$(pwd)"
-brew install $package--$version.*.bottle*.tar.gz -v
diff --git a/package/macos/brew-install-deps b/package/macos/brew-install-deps
deleted file mode 100755
index 45fd5904d5..0000000000
--- a/package/macos/brew-install-deps
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/bin/bash -ex
-
-brew update
-brew install maven cmake boost libyaml jemalloc llvm@17 gmp mpfr z3 pkg-config flex bison haskell-stack
diff --git a/package/macos/brew-update-to-final b/package/macos/brew-update-to-final
deleted file mode 100755
index b2fe3b042c..0000000000
--- a/package/macos/brew-update-to-final
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/sh -exu
-package="$1"  ; shift
-version="$1"  ; shift
-root_url="$1" ; shift
-sed -i "" -e 's!^  url ".*"$!  url "'$root_url/v$version/$package-$version-src'.tar.gz"!' Formula/$package.rb
-cat Formula/$package.rb
diff --git a/package/macos/brew-update-to-local b/package/macos/brew-update-to-local
deleted file mode 100755
index c6b27729cd..0000000000
--- a/package/macos/brew-update-to-local
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/sh -exu
-package="$1" ; shift
-version="$1" ; shift
-sed -i "" -e 's!^  url ".*"$!  url "file:///'$(pwd)/../$package-$version'-src.tar.gz"!' \
-       -e 's!^  sha256 ".*"$!  sha256 "'$(shasum -a 256 ../$package-$version-src.tar.gz | awk '{print $1}')'"!' \
-    Formula/$package.rb