diff --git a/.github/workflows/coq-alpine.yml b/.github/workflows/coq-alpine.yml
index 6ab7f719ae4..8775e5b2f5b 100644
--- a/.github/workflows/coq-alpine.yml
+++ b/.github/workflows/coq-alpine.yml
@@ -6,6 +6,8 @@ on:
   pull_request:
   merge_group:
   workflow_dispatch:
+  release:
+    types: [published]
   schedule:
     - cron: '0 0 1 * *'
 
@@ -91,12 +93,115 @@ jobs:
     - name: display per-line timing info
       run: etc/ci/github-actions-display-per-line-timing.sh
 
+  test-standalone:
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+        - alpine: 'edge'
+#        - alpine: 'latest-stable'
+    runs-on: ubuntu-latest
+    name: test-standalone-${{ matrix.alpine }}
+    needs: build
+    steps:
+    - uses: actions/checkout@v4
+    - name: Download standalone ${{ matrix.alpine }}
+      uses: actions/download-artifact@v3
+      with:
+        name: standalone-${{ matrix.alpine }}
+        path: dist-${{ matrix.alpine }}/
+    - name: List files
+      run: find dist-edge
+    - name: Rename files
+      run: |
+        mkdir dist
+        mv dist-${{ matrix.alpine }}/standalone.tar.gz dist/fiat-crypto-alpine-${{ matrix.alpine }}.tar.gz
+        find dist
+        tar -tvf dist/fiat-crypto-alpine-${{ matrix.alpine }}.tar.gz
+    - name: Unpack files
+      run: |
+        cd dist
+        tar -xzvf fiat-crypto-alpine-${{ matrix.alpine }}.tar.gz
+        ls -la .
+    - name: Test files (host)
+      run: |
+        cd dist
+        for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do
+          echo "::group::file $prog"
+          file $prog
+          echo "::endgroup::"
+          echo "::group::ldd $prog"
+          ldd $prog
+          echo "::endgroup::"
+          echo "::group::$prog"
+          ./$prog -h || echo "::error::$prog does not run on host" # does not work yet
+          echo "::endgroup::"
+        done
+    - uses: jirutka/setup-alpine@v1
+      with:
+        branch: ${{ matrix.alpine }}
+        extra-repositories: https://dl-cdn.alpinelinux.org/alpine/edge/testing
+    - name: Test files (container)
+      shell: alpine.sh {0}
+      run: |
+        cd dist
+        for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do
+          echo "::group::file $prog"
+          file $prog
+          echo "::endgroup::"
+          echo "::group::ldd $prog"
+          ldd $prog
+          echo "::endgroup::"
+          echo "::group::$prog"
+          ./$prog -h
+          echo "::endgroup::"
+        done
+
+  publish-standalone:
+    runs-on: ubuntu-latest
+    needs: build
+    permissions:
+      contents: write  # IMPORTANT: mandatory for making GitHub Releases
+    steps:
+    - uses: actions/checkout@v4
+    - name: Download standalone edge
+      uses: actions/download-artifact@v3
+      with:
+        name: standalone-edge
+        path: dist-edge/
+    - name: List files
+      run: find dist-edge
+    - name: Unpack files
+      run: |
+        mkdir dist
+        mv dist-edge/standalone.tar.gz dist/fiat-crypto-alpine-edge.tar.gz
+        find dist
+        tar -tvf dist/fiat-crypto-alpine-edge.tar.gz
+    - name: Upload artifacts to GitHub Release
+      env:
+        GITHUB_TOKEN: ${{ github.token }}
+      # Upload to GitHub Release using the `gh` CLI.
+      # `dist/` contains the built packages
+      run: >-
+        gh release upload
+        '${{ github.ref_name }}' dist/**
+        --repo '${{ github.repository }}'
+      if: ${{ startsWith(github.ref, 'refs/tags/') && github.event_name == 'release' }}
+
   alpine-check-all:
     runs-on: ubuntu-latest
-    needs: [build]
+    needs: [build, test-standalone, publish-standalone]
     if: always()
     steps:
     - run: echo 'build passed'
       if: ${{ needs.build.result == 'success' }}
+    - run: echo 'test-standalone passed'
+      if: ${{ needs.test-standalone == 'success' }}
+    - run: echo 'publish-standalone passed'
+      if: ${{ needs.publish-standalone.result == 'success' }}
     - run: echo 'build failed' && false
       if: ${{ needs.build.result != 'success' }}
+    - run: echo 'test-standalone failed' && false
+      if: ${{ needs.test-standalone != 'success' }}
+    - run: echo 'publish-standalone failed' && false
+      if: ${{ needs.publish-standalone.result != 'success' }}
diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml
index 774f3725bd4..fc7d4d19c55 100644
--- a/.github/workflows/coq-debian.yml
+++ b/.github/workflows/coq-debian.yml
@@ -6,6 +6,8 @@ on:
   pull_request:
   merge_group:
   workflow_dispatch:
+  release:
+    types: [published]
   schedule:
     - cron: '0 0 1 * *'
 
@@ -113,16 +115,116 @@ jobs:
       env:
         ALLOW_DIFF: 1
 
+  test-standalone:
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+        - debian: sid
+        #- debian: bookworm # restore once 8.17 lands in Debian stable
+    runs-on: ubuntu-latest
+    needs: build
+    steps:
+    - uses: actions/checkout@v4
+    - name: Download standalone ${{ matrix.debian }}
+      uses: actions/download-artifact@v3
+      with:
+        name: standalone-${{ matrix.debian }}
+        path: dist-${{ matrix.debian }}/
+    - name: List files
+      run: find dist-${{ matrix.debian }}
+    - name: Rename files
+      run: |
+        mkdir dist
+        mv dist-${{ matrix.debian }}/standalone.tar.gz dist/fiat-crypto-${{ matrix.debian }}.tar.gz
+        find dist
+        tar -tvf dist/fiat-crypto-${{ matrix.debian }}.tar.gz
+    - name: Unpack Files
+      run: |
+        cd dist
+        tar -xzvf fiat-crypto-${{ matrix.debian }}.tar.gz
+        ls -la .
+    - name: Test files (host)
+      run: |
+        cd dist
+        for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do
+          echo "::group::file $prog"
+          file $prog
+          echo "::endgroup::"
+          echo "::group::ldd $prog"
+          ldd $prog
+          echo "::endgroup::"
+          echo "::group::$prog"
+          ./$prog -h
+          echo "::endgroup::"
+        done
+    - name: setup Debian chroot
+      run: etc/ci/setup-debian-chroot.sh "${{ matrix.debian }}"
+    - name: Test files (container)
+      shell: in-debian-chroot.sh {0}
+      run: |
+        cd dist
+        for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do
+          echo "::group::file $prog"
+          file $prog
+          echo "::endgroup::"
+          echo "::group::ldd $prog"
+          ldd $prog
+          echo "::endgroup::"
+          echo "::group::$prog"
+          ./$prog -h
+          echo "::endgroup::"
+        done
+
+  publish-standalone:
+    runs-on: ubuntu-latest
+    needs: build
+    permissions:
+      contents: write  # IMPORTANT: mandatory for making GitHub Releases
+    steps:
+    - uses: actions/checkout@v4
+    - name: Download standalone sid
+      uses: actions/download-artifact@v3
+      with:
+        name: standalone-sid
+        path: dist-sid/
+    - name: List files
+      run: find dist-sid
+    - name: Unpack files
+      run: |
+        mkdir dist
+        mv dist-sid/standalone.tar.gz dist/fiat-crypto-sid.tar.gz
+        find dist
+        tar -tvf dist/fiat-crypto-sid.tar.gz
+    - name: Upload artifacts to GitHub Release
+      env:
+        GITHUB_TOKEN: ${{ github.token }}
+      # Upload to GitHub Release using the `gh` CLI.
+      # `dist/` contains the built packages
+      run: >-
+        gh release upload
+        '${{ github.ref_name }}' dist/**
+        --repo '${{ github.repository }}'
+      if: ${{ startsWith(github.ref, 'refs/tags/') && github.event_name == 'release' }}
+
   debian-check-all:
     runs-on: ubuntu-latest
-    needs: [build, test-amd64]
+    needs: [build, test-amd64, test-standalone, publish-standalone]
     if: always()
     steps:
     - run: echo 'build passed'
       if: ${{ needs.build.result == 'success' }}
     - run: echo 'test-amd64 passed'
       if: ${{ needs.test-amd64.result == 'success' }}
+    - run: echo 'test-standalone passed'
+      if: ${{ needs.test-standalone == 'success' }}
+    - run: echo 'publish-standalone passed'
+      if: ${{ needs.publish-standalone.result == 'success' }}
     - run: echo 'build failed' && false
       if: ${{ needs.build.result != 'success' }}
     - run: echo 'test-amd64 failed' && false
       if: ${{ needs.test-amd64.result != 'success' }}
+    - run: echo 'test-standalone failed' && false
+      if: ${{ needs.test-standalone != 'success' }}
+    - run: echo 'publish-standalone failed' && false
+      if: ${{ needs.publish-standalone.result != 'success' }}
diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml
index 9ec9954229b..fd3bf4bd535 100644
--- a/.github/workflows/coq-docker.yml
+++ b/.github/workflows/coq-docker.yml
@@ -6,6 +6,8 @@ on:
   pull_request:
   merge_group:
   workflow_dispatch:
+  release:
+    types: [published]
   schedule:
     - cron: '0 0 1 * *'
 
@@ -132,16 +134,119 @@ jobs:
       env:
         ALLOW_DIFF: 1
 
+  test-standalone:
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+        - coq-version: master
+          docker-coq-version: dev
+          docker-ocaml-version: default
+
+    runs-on: ubuntu-latest
+    needs: build
+    steps:
+    - uses: actions/checkout@v4
+    - name: Download standalone Docker
+      uses: actions/download-artifact@v3
+      with:
+        name: standalone-docker-coq-${{ matrix.docker-coq-version }}
+        path: dist-docker-coq-${{ matrix.docker-coq-version }}/
+    - name: List files
+      run: find dist-docker-coq-${{ matrix.docker-coq-version }}
+    - name: Rename files
+      run: |
+        mkdir dist
+        mv dist-docker-coq-${{ matrix.docker-coq-version }}/standalone.tar.gz dist/fiat-crypto-docker-coq-${{ matrix.docker-coq-version }}.tar.gz
+        find dist
+        tar -tvf dist/fiat-crypto-docker-coq-${{ matrix.docker-coq-version }}.tar.gz
+    - name: Unpack Files
+      run: |
+        cd dist
+        tar -xzvf fiat-crypto-docker-coq-${{ matrix.docker-coq-version }}.tar.gz
+        ls -la .
+    - name: Test files (host)
+      run: |
+        cd dist
+        for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do
+          echo "::group::file $prog"
+          file $prog
+          echo "::endgroup::"
+          echo "::group::ldd $prog"
+          ldd $prog
+          echo "::endgroup::"
+          echo "::group::$prog"
+          ./$prog -h
+          echo "::endgroup::"
+        done
+    - name: Test files (container)
+      uses: coq-community/docker-coq-action@v1
+      with:
+        coq_version: ${{ matrix.docker-coq-version }}
+        ocaml_version: ${{ matrix.docker-ocaml-version }}
+        custom_script: |
+          cd dist
+          for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do
+            echo "::group::file $prog"
+            file $prog
+            echo "::endgroup::"
+            echo "::group::ldd $prog"
+            ldd $prog
+            echo "::endgroup::"
+            echo "::group::$prog"
+            ./$prog -h
+            echo "::endgroup::"
+          done
+
+  publish-standalone:
+    runs-on: ubuntu-latest
+    needs: build
+    permissions:
+      contents: write  # IMPORTANT: mandatory for making GitHub Releases
+    steps:
+    - uses: actions/checkout@v4
+    - name: Download standalone Docker
+      uses: actions/download-artifact@v3
+      with:
+        name: standalone-docker-coq-dev
+        path: dist-docker-coq-dev/
+    - name: List files
+      run: find dist-docker-coq-dev
+    - name: Unpack files
+      run: |
+        mkdir dist
+        mv dist-docker-coq-dev/standalone.tar.gz dist/fiat-crypto-docker-coq-dev.tar.gz
+        find dist
+        tar -tvf dist/fiat-crypto-docker-coq-dev.tar.gz
+    - name: Upload artifacts to GitHub Release
+      env:
+        GITHUB_TOKEN: ${{ github.token }}
+      # Upload to GitHub Release using the `gh` CLI.
+      # `dist/` contains the built packages
+      run: >-
+        gh release upload
+        '${{ github.ref_name }}' dist/**
+        --repo '${{ github.repository }}'
+      if: ${{ startsWith(github.ref, 'refs/tags/') && github.event_name == 'release' }}
+
   docker-check-all:
     runs-on: ubuntu-latest
-    needs: [build, test-amd64]
+    needs: [build, test-amd64, test-standalone, publish-standalone]
     if: always()
     steps:
     - run: echo 'build passed'
       if: ${{ needs.build.result == 'success' }}
     - run: echo 'test-amd64 passed'
       if: ${{ needs.test-amd64.result == 'success' }}
+    - run: echo 'test-standalone passed'
+      if: ${{ needs.test-standalone == 'success' }}
+    - run: echo 'publish-standalone passed'
+      if: ${{ needs.publish-standalone.result == 'success' }}
     - run: echo 'build failed' && false
       if: ${{ needs.build.result != 'success' }}
     - run: echo 'test-amd64 failed' && false
       if: ${{ needs.test-amd64.result != 'success' }}
+    - run: echo 'test-standalone failed' && false
+      if: ${{ needs.test-standalone != 'success' }}
+    - run: echo 'publish-standalone failed' && false
+      if: ${{ needs.publish-standalone.result != 'success' }}
diff --git a/.github/workflows/coq-macos.yml b/.github/workflows/coq-macos.yml
index 48ec0e7136e..7f56cd7cd3a 100644
--- a/.github/workflows/coq-macos.yml
+++ b/.github/workflows/coq-macos.yml
@@ -6,6 +6,8 @@ on:
   pull_request:
   merge_group:
   workflow_dispatch:
+  release:
+    types: [published]
   schedule:
     - cron: '0 0 1 * *'
 
@@ -97,12 +99,89 @@ jobs:
 #        make TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}"
 #      if: github.event_name != 'pull_request'
 
+  test-standalone:
+    runs-on: macos-latest
+    needs: build
+    steps:
+    - uses: actions/checkout@v4
+    - name: Download standalone MacOS
+      uses: actions/download-artifact@v3
+      with:
+        name: standalone-macos
+        path: dist-macos/
+    - name: List files
+      run: find dist-macos
+    - name: Rename files
+      run: |
+        mkdir dist
+        mv dist-macos/standalone.tar.gz dist/fiat-crypto-macos.tar.gz
+        find dist
+        tar -tvf dist/fiat-crypto-macos.tar.gz
+    - name: Unpack Files
+      run: |
+        cd dist
+        tar -xzvf fiat-crypto-macos.tar.gz
+        ls -la .
+    - name: Test files
+    - run: |
+        cd dist
+        for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do
+          echo "::group::file $prog"
+          file $prog
+          echo "::endgroup::"
+          echo "::group::otool -L $prog"
+          otool -L $prog
+          echo "::endgroup::"
+          echo "::group::$prog"
+          ./$prog -h
+          echo "::endgroup::"
+        done
+
+  publish-standalone:
+    runs-on: ubuntu-latest
+    needs: build
+    permissions:
+      contents: write  # IMPORTANT: mandatory for making GitHub Releases
+    steps:
+    - uses: actions/checkout@v4
+    - name: Download standalone MacOS
+      uses: actions/download-artifact@v3
+      with:
+        name: standalone-macos
+        path: dist-macos/
+    - name: List files
+      run: find dist-macos
+    - name: Unpack files
+      run: |
+        mkdir dist
+        mv dist-macos/standalone.tar.gz dist/fiat-crypto-macos.tar.gz
+        find dist
+        tar -tvf dist/fiat-crypto-macos.tar.gz
+    - name: Upload artifacts to GitHub Release
+      env:
+        GITHUB_TOKEN: ${{ github.token }}
+      # Upload to GitHub Release using the `gh` CLI.
+      # `dist/` contains the built packages
+      run: >-
+        gh release upload
+        '${{ github.ref_name }}' dist/**
+        --repo '${{ github.repository }}'
+      if: ${{ startsWith(github.ref, 'refs/tags/') && github.event_name == 'release' }}
+
   macos-check-all:
     runs-on: ubuntu-latest
-    needs: [build]
+    needs: [build, test-standalone, publish-standalone]
     if: always()
     steps:
     - run: echo 'build passed'
       if: ${{ needs.build.result == 'success' }}
+    - run: echo 'test-standalone passed'
+      if: ${{ needs.test-standalone == 'success' }}
+    - run: echo 'publish-standalone passed'
+      if: ${{ needs.publish-standalone.result == 'success' }}
     - run: echo 'build failed' && false
       if: ${{ needs.build.result != 'success' }}
+    - run: echo 'test-standalone failed' && false
+      if: ${{ needs.test-standalone != 'success' }}
+    - run: echo 'publish-standalone failed' && false
+      if: ${{ needs.publish-standalone.result != 'success' }}
diff --git a/.github/workflows/coq-windows.yml b/.github/workflows/coq-windows.yml
index 170dae6a34e..5e9de04b721 100644
--- a/.github/workflows/coq-windows.yml
+++ b/.github/workflows/coq-windows.yml
@@ -9,6 +9,8 @@ on:
   pull_request:
   merge_group:
   workflow_dispatch:
+  release:
+    types: [published]
   schedule:
     - cron: '0 0 1 * *'
 
@@ -118,12 +120,96 @@ jobs:
 #      shell: cmd
 #      if: github.event_name != 'pull_request'
 
+  test-standalone:
+    runs-on: windows-latest
+    needs: build
+    steps:
+    - uses: actions/checkout@v4
+    - name: Download standalone Windows
+      uses: actions/download-artifact@v3
+      with:
+        name: standalone-windows
+        path: dist-windows/
+    - name: List files
+      run: Get-ChildItem dist-windows -Name
+    - name: Rename files
+      run: |
+        New-Item -ItemType Directory -Path dist
+        Move-Item dist-windows/standalone.zip dist/fiat-crypto-windows.zip
+        Get-ChildItem dist -Name
+    - name: Unpack files
+      run: |
+        Expand-Archive -Path dist/fiat-crypto-windows.zip -DestinationPath dist
+        Get-ChildItem dist
+    - name: Check Executable Dependencies
+      run: |
+        $executables = @(
+          ".\dist\word_by_word_montgomery.exe",
+          ".\dist\unsaturated_solinas.exe",
+          ".\dist\saturated_solinas.exe",
+          ".\dist\base_conversion.exe"
+        )
+
+        foreach ($prog in $executables) {
+          Write-Host "::group::File Info - $prog"
+          Get-Item $prog | Format-List
+          dumpbin.exe /headers $prog
+          Write-Host "::endgroup::"
+
+          Write-Host "::group::DLL Dependencies - $prog"
+          dumpbin.exe /dependents $prog
+          Write-Host "::endgroup::"
+        }
+    - run: .\dist\word_by_word_montgomery.exe -h
+    - run: .\dist\unsaturated_solinas.exe -h
+    - run: .\dist\saturated_solinas.exe -h
+    - run: .\dist\base_conversion.exe -h
+
+  publish-standalone:
+    runs-on: ubuntu-latest
+    needs: build
+    permissions:
+      contents: write  # IMPORTANT: mandatory for making GitHub Releases
+    steps:
+    - uses: actions/checkout@v4
+    - name: Download standalone Windows
+      uses: actions/download-artifact@v3
+      with:
+        name: standalone-windows
+        path: dist-windows/
+    - name: List files
+      run: find dist-windows
+    - name: Unpack files
+      run: |
+        mkdir dist
+        mv dist-windows/standalone.zip dist/fiat-crypto-windows.zip
+        find dist
+        unzip -l dist/fiat-crypto-windows.zip
+    - name: Upload artifacts to GitHub Release
+      env:
+        GITHUB_TOKEN: ${{ github.token }}
+      # Upload to GitHub Release using the `gh` CLI.
+      # `dist/` contains the built packages
+      run: >-
+        gh release upload
+        '${{ github.ref_name }}' dist/**
+        --repo '${{ github.repository }}'
+      if: ${{ startsWith(github.ref, 'refs/tags/') && github.event_name == 'release' }}
+
   windows-check-all:
     runs-on: ubuntu-latest
-    needs: [build]
+    needs: [build, test-standalone, publish-standalone]
     if: always()
     steps:
     - run: echo 'build passed'
       if: ${{ needs.build.result == 'success' }}
+    - run: echo 'test-standalone passed'
+      if: ${{ needs.test-standalone == 'success' }}
+    - run: echo 'publish-standalone passed'
+      if: ${{ needs.publish-standalone.result == 'success' }}
     - run: echo 'build failed' && false
       if: ${{ needs.build.result != 'success' }}
+    - run: echo 'test-standalone failed' && false
+      if: ${{ needs.test-standalone != 'success' }}
+    - run: echo 'publish-standalone failed' && false
+      if: ${{ needs.publish-standalone.result != 'success' }}