diff --git a/.github/workflows/all.yml b/.github/workflows/all.yml
index 458e4c8aa2..3a341d7632 100644
--- a/.github/workflows/all.yml
+++ b/.github/workflows/all.yml
@@ -13,100 +13,31 @@ on:
     types: [ "opened", "synchronize" ]
 
 jobs:
-  base:
-    name: Base
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    uses: ./.github/workflows/base.yml
-    secrets: inherit
-  lint-markdown:
-    name: Lint Markdown
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    uses: ./.github/workflows/lint_markdown.yml
-  nix:
-    name: Nix
-    permissions:
-      actions: 'write'
-      contents: 'read'
-      id-token: 'write'
-    uses: ./.github/workflows/nix.yml
-    secrets: inherit
+  # base:
+  #   name: Base
+  #   permissions:
+  #     contents: 'read'
+  #     id-token: 'write'
+  #   uses: ./.github/workflows/base.yml
+  #   secrets: inherit
+  # lint-markdown:
+  #   name: Lint Markdown
+  #   permissions:
+  #     contents: 'read'
+  #     id-token: 'write'
+  #   uses: ./.github/workflows/lint_markdown.yml
+  # nix:
+  #   name: Nix
+  #   permissions:
+  #     actions: 'write'
+  #     contents: 'read'
+  #     id-token: 'write'
+  #   uses: ./.github/workflows/nix.yml
+  #   secrets: inherit
   ci:
     name: Extended
     permissions:
       contents: 'read'
       id-token: 'write'
-    needs: [ base, nix ]
     uses: ./.github/workflows/ci.yml
     secrets: inherit
-  cbmc:
-    name: CBMC
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    needs: [ base, nix ]
-    uses: ./.github/workflows/cbmc.yml
-    secrets: inherit
-  oqs_integration:
-    name: libOQS
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    needs: [ base ]
-    uses: ./.github/workflows/integration-liboqs.yml
-    secrets: inherit
-  opentitan_integration:
-    name: OpenTitan
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    needs: [ base ]
-    uses: ./.github/workflows/integration-opentitan.yml
-    secrets: inherit
-  awslc_integration_fixed:
-    name: AWS-LC (v1.64.0)
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    needs: [ base ]
-    uses: ./.github/workflows/integration-awslc.yml
-    with:
-      commit: 7187ab572ddcdae4fa408e932d3e878c9941137b # v1.64.0
-    secrets: inherit
-  awslc_integration_head:
-    name: AWS-LC (HEAD)
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    needs: [ base ]
-    uses: ./.github/workflows/integration-awslc.yml
-    with:
-      commit: main
-    secrets: inherit
-  ct-test:
-    name: Constant-time
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    needs: [ base, nix ]
-    uses: ./.github/workflows/ct-tests.yml
-    secrets: inherit
-  slothy:
-    name: SLOTHY
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    needs: [ base, nix ]
-    uses: ./.github/workflows/slothy.yml
-    secrets: inherit
-  baremetal:
-    name: Baremetal
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    needs: [ base ]
-    uses: ./.github/workflows/baremetal.yml
-    secrets: inherit
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 0a22bd2ce3..df3c3f835e 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -9,695 +9,725 @@ on:
   workflow_dispatch:
 
 jobs:
-  build_kat:
-    strategy:
-      fail-fast: false
-      matrix:
-        external:
-         - ${{ github.repository_owner != 'pq-code-package' }}
-        target:
-         - runner: macos-latest
-           name: 'MacOS (aarch64)'
-           arch: mac
-           mode: native
-           nix_shell: ci
-         - runner: macos-15-intel
-           name: 'MacOS (x86_64)'
-           arch: mac
-           mode: native
-           nix_shell: ci
-         - runner: pqcp-arm64
-           name: 'ubuntu-latest (aarch64)'
-           arch: aarch64
-           mode: native
-           nix_shell: ci
-         - runner: pqcp-arm64
-           name: 'ubuntu-latest (aarch64)'
-           arch: x86_64
-           mode: cross-x86_64
-           nix_shell: ci-cross-x86_64
-         - runner: pqcp-arm64
-           name: 'ubuntu-latest (aarch64)'
-           arch: riscv64
-           mode: cross-riscv64
-           nix_shell: ci-cross-riscv64
-         - runner: pqcp-arm64
-           name: 'ubuntu-latest (aarch64)'
-           arch: riscv32
-           mode: cross-riscv32
-           nix_shell: ci-cross-riscv32
-         - runner: pqcp-arm64
-           name: 'ubuntu-latest (ppc64le)'
-           arch: ppc64le
-           mode: cross-ppc64le
-           nix_shell: ci-cross-ppc64le
-         - runner: pqcp-x64
-           name: 'ubuntu-latest (x86_64)'
-           arch: x86_64
-           mode: native
-           nix_shell: ci
-         - runner: pqcp-x64
-           name: 'ubuntu-latest (x86_64)'
-           arch: aarch64
-           mode: cross-aarch64
-           nix_shell: ci-cross-aarch64
-         - runner: pqcp-x64
-           name: 'ubuntu-latest (x86_64)'
-           arch: aarch64_be
-           mode: cross-aarch64_be
-           nix_shell: ci-cross-aarch64_be
-        exclude:
-          - {external: true,
-             target: {
-               runner: pqcp-arm64,
-               name: 'ubuntu-latest (aarch64)',
-               arch: aarch64,
-               mode: native,
-               nix_shell: ci
-             }}
-          - {external: true,
-             target: {
-               runner: pqcp-arm64,
-               name: 'ubuntu-latest (aarch64)',
-               arch: x86_64,
-               mode: cross-x86_64,
-               nix_shell: ci-cross-x86_64
-             }}
-          - {external: true,
-             target: {
-               runner: pqcp-arm64,
-               name: 'ubuntu-latest (aarch64)',
-               arch: riscv64,
-               mode: cross-riscv64,
-               nix_shell: ci-cross-riscv64
-             }}
-          - {external: true,
-             target: {
-               runner: pqcp-arm64,
-               name: 'ubuntu-latest (aarch64)',
-               arch: riscv32,
-               mode: cross-riscv32,
-               nix_shell: ci-cross-riscv32
-             }}
-          - {external: true,
-             target: {
-               runner: pqcp-arm64,
-               name: 'ubuntu-latest (ppc64le)',
-               arch: ppc64le,
-               mode: cross-ppc64le,
-               nix_shell: ci-cross-ppc64le
-             }}
-          - {external: true,
-             target: {
-               runner: pqcp-x64,
-               name: 'ubuntu-latest (x86_64)',
-               arch: x86_64,
-               mode: native,
-               nix_shell: ci
-             }}
-          - {external: true,
-             target: {
-               runner: pqcp-x64,
-               name: 'ubuntu-latest (x86_64)',
-               arch: aarch64,
-               mode: cross-aarch64,
-               nix_shell: ci-cross-aarch64
-             }}
-          - {external: true,
-             target: {
-               runner: pqcp-x64,
-               name: 'ubuntu-latest (x86_64)',
-               arch: aarch64_be,
-               mode: cross-aarch64_be,
-               nix_shell: ci-cross-aarch64_be
-             }}
-    name: Functional tests (${{ matrix.target.arch }}${{ matrix.target.mode != 'native' && ', cross' || ''}})
-    runs-on: ${{ matrix.target.runner }}
-    steps:
-      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
-      - name: build + test (no-opt)
-        uses: ./.github/actions/multi-functest
-        with:
-          nix-shell: ${{ matrix.target.nix_shell }}
-          nix-cache: ${{ matrix.target.mode == 'native' && 'false' || 'true' }}
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          compile_mode: ${{ matrix.target.mode }}
-          opt: 'no_opt'
-      - name: build + test (+debug+memsan+ubsan, native)
-        uses: ./.github/actions/multi-functest
-        if: ${{ matrix.target.mode == 'native' }}
-        with:
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          compile_mode: native
-          cflags: "-DMLKEM_DEBUG -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all"
-          ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all"
-          check_namespace: 'false'
-      - name: build + test (cross, opt)
-        uses: ./.github/actions/multi-functest
-        # There is no native code yet on PPC64LE, riscv32 or AArch64_be, so no point running opt tests
-        if: ${{ matrix.target.mode != 'native' && (matrix.target.arch != 'ppc64le' && matrix.target.arch != 'riscv32' && matrix.target.arch != 'aarch64_be') }}
-        with:
-          nix-shell: ${{ matrix.target.nix_shell }}
-          nix-cache: ${{ matrix.target.mode == 'native' && 'false' || 'true' }}
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          compile_mode: ${{ matrix.target.mode }}
-          opt: 'opt'
-      - name: build + test (cross, opt, +debug)
-        uses: ./.github/actions/multi-functest
-        # There is no native code yet on PPC64LE, riscv32 or AArch64_be, so no point running opt tests
-        if: ${{ matrix.target.mode != 'native' && (matrix.target.arch != 'ppc64le' && matrix.target.arch != 'riscv32' && matrix.target.arch != 'aarch64_be') }}
-        with:
-          nix-shell: ${{ matrix.target.nix_shell }}
-          nix-cache: ${{ matrix.target.mode == 'native' && 'false' || 'true' }}
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          compile_mode: ${{ matrix.target.mode }}
-          cflags: "-DMLKEM_DEBUG"
-          opt: 'opt'
-  backend_tests:
-    name: AArch64 FIPS202 backends (${{ matrix.backend }})
-    strategy:
-      fail-fast: false
-      matrix:
-        backend: [x1_scalar, x1_v84a, x2_v84a, x4_v8a_scalar, x4_v8a_v84a_scalar]
-    runs-on: macos-latest
-    steps:
-      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
-      - name: build + test
-        uses: ./.github/actions/multi-functest
-        with:
-          nix-shell: 'ci'
-          nix-cache: 'false'
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          compile_mode: 'native'
-          opt: 'opt'
-          examples: 'false'
-          cflags: "-DMLKEM_DEBUG -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all"
-          ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all"
-          check_namespace: 'false'
-          extra_args: "--fips202-aarch64-backend ${{ matrix.backend }}"
-  compiler_tests:
-    name: Compiler tests  (${{ matrix.compiler.name }}, ${{ matrix.target.name }}, ${{ matrix.cflags }})
-    strategy:
-      fail-fast: false
-      matrix:
-        cflags: [ "-O0", "-Os", "-O3" ]
-        target:
-         - runner: pqcp-arm64
-           name: 'aarch64'
-         - runner: ubuntu-latest
-           name: 'x86_64'
-         - runner: macos-latest
-           name: 'macos'
-        compiler:
-         - name: gcc-4.8
-           shell: ci_gcc48
-           darwin: False
-           c17: False
-           c23: False
-           opt: all
-           examples: true
-         - name: gcc-4.9
-           shell: ci_gcc49
-           darwin: False
-           c17: False
-           c23: False
-           opt: all
-           examples: true
-         - name: gcc-7
-           shell: ci_gcc7
-           darwin: False
-           c17: False
-           c23: False
-           opt: all
-           examples: true
-         - name: gcc-11
-           shell: ci_gcc11
-           darwin: True
-           c17: True
-           c23: False
-           opt: all
-           examples: true
-         - name: gcc-13
-           shell: ci_gcc13
-           darwin: True
-           c17: True
-           c23: False
-           opt: all
-           examples: true
-         - name: gcc-14
-           shell: ci_gcc14
-           darwin: True
-           c17: True
-           c23: True
-           opt: all
-           examples: true
-         - name: gcc-15
-           shell: ci_gcc15
-           # TODO: Add this once gcc15 is supported in nix on aarch64-Darwin
-           darwin: False
-           c17: True
-           c23: True
-           opt: all
-           examples: true
-         - name: clang-18
-           shell: ci_clang18
-           darwin: True
-           c17: True
-           c23: True
-           opt: all
-           examples: true
-         - name: clang-19
-           shell: ci_clang19
-           darwin: True
-           c17: True
-           c23: True
-           opt: all
-           examples: true
-         - name: clang-20
-           shell: ci_clang20
-           darwin: True
-           c17: True
-           c23: True
-           opt: all
-           examples: true
-         - name: clang-21
-           shell: ci_clang21
-           darwin: True
-           c17: True
-           c23: True
-           opt: all
-           examples: true
-         # CPU flags are not correctly passed to the zig assembler
-         # https://github.com/ziglang/zig/issues/23576
-         # We therefore only test the C backend
-         #
-         # We omit all examples since there is currently no way to run
-         # only those examples not involving native code.
-         - name: zig-0.12
-           shell: ci_zig0_12
-           darwin: True
-           c17: True
-           c23: False
-           examples: False
-           opt: no_opt
-         - name: zig-0.13
-           shell: ci_zig0_13
-           darwin: True
-           c17: True
-           c23: False
-           examples: False
-           opt: no_opt
-         - name: zig-0.14
-           shell: ci_zig0_14
-           darwin: True
-           c17: True
-           c23: True
-           examples: False
-           opt: no_opt
-         - name: zig-0.15
-           shell: ci_zig0_15
-           darwin: True
-           c17: True
-           c23: True
-           examples: False
-           opt: no_opt
-    runs-on: ${{ matrix.target.runner }}
-    steps:
-      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
-      - name: native build+functest (default)
-        if: ${{ matrix.compiler.darwin || matrix.target.runner != 'macos-latest' }}
-        uses: ./.github/actions/multi-functest
-        with:
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          compile_mode: native
-          func: true
-          kat: false
-          acvp: false
-          examples: ${{ matrix.compiler.examples }}
-          opt: ${{ matrix.compiler.opt }}
-          nix-shell: ${{ matrix.compiler.shell }}
-          cflags: "${{ matrix.cflags }}"
-      - name: native build+functest (C90)
-        if: ${{ matrix.compiler.darwin || matrix.target.runner != 'macos-latest' }}
-        uses: ./.github/actions/multi-functest
-        with:
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          compile_mode: native
-          func: true
-          kat: false
-          acvp: false
-          examples: ${{ matrix.compiler.examples }}
-          opt: ${{ matrix.compiler.opt }}
-          nix-shell: ${{ matrix.compiler.shell }}
-          cflags: "-std=c90 ${{ matrix.cflags }}"
-      - name: native build+functest (C99)
-        if: ${{ matrix.compiler.darwin || matrix.target.runner != 'macos-latest' }}
-        uses: ./.github/actions/multi-functest
-        with:
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          compile_mode: native
-          func: true
-          kat: false
-          acvp: false
-          examples: ${{ matrix.compiler.examples }}
-          opt: ${{ matrix.compiler.opt }}
-          nix-shell: ${{ matrix.compiler.shell }}
-          cflags: "-std=c99 ${{ matrix.cflags }}"
-      - name: native build+functest (C11)
-        if: ${{ matrix.compiler.darwin || matrix.target.runner != 'macos-latest' }}
-        uses: ./.github/actions/multi-functest
-        with:
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          compile_mode: native
-          func: true
-          kat: false
-          acvp: false
-          examples: ${{ matrix.compiler.examples }}
-          opt: ${{ matrix.compiler.opt }}
-          nix-shell: ${{ matrix.compiler.shell }}
-          cflags: "-std=c11 ${{ matrix.cflags }}"
-      - name: native build+functest (C17)
-        if: ${{ (matrix.compiler.darwin || matrix.target.runner != 'macos-latest') &&
-                matrix.compiler.c17 }}
-        uses: ./.github/actions/multi-functest
-        with:
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          compile_mode: native
-          func: true
-          kat: false
-          acvp: false
-          examples: ${{ matrix.compiler.examples }}
-          opt: ${{ matrix.compiler.opt }}
-          nix-shell: ${{ matrix.compiler.shell }}
-          cflags: "-std=c17 ${{ matrix.cflags }}"
-      - name: native build+functest (C23)
-        if: ${{ (matrix.compiler.darwin || matrix.target.runner != 'macos-latest') &&
-                matrix.compiler.c23 }}
-        uses: ./.github/actions/multi-functest
-        with:
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          compile_mode: native
-          func: true
-          kat: false
-          acvp: false
-          examples: ${{ matrix.compiler.examples }}
-          opt: ${{ matrix.compiler.opt }}
-          nix-shell: ${{ matrix.compiler.shell }}
-          cflags: "-std=c23 ${{ matrix.cflags }}"
-  stack_analysis:
-    name: Stack analysis (${{ matrix.target.name }}, ${{ matrix.cflags }})
-    strategy:
-      fail-fast: false
-      matrix:
-        external:
-         - ${{ github.repository_owner != 'pq-code-package' }}
-        target:
-          - runner: pqcp-x64
-            name: x86_64
-          - runner: pqcp-arm64
-            name: aarch64
-        cflags: ['-O3', '-Os']
-        exclude:
-          - external: true
-    runs-on: ${{ matrix.target.runner }}
-    steps:
-      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
-      - name: Stack analysis
-        uses: ./.github/actions/multi-functest
-        with:
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          compile_mode: native
-          nix-shell: ci_valgrind-varlat_gcc15
-          nix-cache: false
-          opt: all
-          cflags: "${{ matrix.cflags }}"
-          func: false
-          kat: false
-          acvp: false
-          examples: false
-          stack: true
-          check_namespace: false
-  config_variations:
-    name: Non-standard configurations
-    strategy:
-      fail-fast: false
-      matrix:
-        external:
-         - ${{ github.repository_owner != 'pq-code-package' }}
-        target:
-         - runner: pqcp-arm64
-           name: 'ubuntu-latest (aarch64)'
-         - runner: pqcp-x64
-           name: 'ubuntu-latest (x86_64)'
-        exclude:
-          - {external: true,
-             target: {
-               runner: pqcp-arm64,
-               name: 'ubuntu-latest (aarch64)',
-             }}
-          - {external: true,
-             target: {
-               runner: pqcp-x64,
-               name: 'ubuntu-latest (x86_64)',
-             }}
-    runs-on: ${{ matrix.target.runner }}
-    steps:
-      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
-      - name: "Config Variations"
-        uses: ./.github/actions/config-variations
-        with:
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-  check-cf-protections:
-    name: Test control-flow protections  (${{ matrix.compiler.name }}, x86_64)
-    strategy:
-      fail-fast: false
-      matrix:
-        compiler:
-         - name: gcc-14
-           shell: ci_gcc14
-         - name: gcc-15
-           shell: ci_gcc15
-         - name: clang-19
-           shell: ci_clang19
-    # On AArch64 -fcf-protection is not supported anyway
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
-      - name: Test control-flow protections
-        uses: ./.github/actions/multi-functest
-        with:
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          compile_mode: native
-          cflags: "-Wl,-z,cet-report=error -fcf-protection=full"
-          func: true
-          kat: true
-          acvp: true
-          nix-shell: ${{ matrix.compiler.shell }}
-  # ensure that kem.h and mlkem_native.h; api.h and native backends are compatible
-  check-apis:
-    strategy:
-      fail-fast: false
-      matrix:
-        external:
-         - ${{ github.repository_owner != 'pq-code-package' }}
-        target:
-         - runner: pqcp-arm64
-           name: 'aarch64'
-         - runner: ubuntu-latest
-           name: 'x86_64'
-        exclude:
-          - {external: true,
-             target: {
-               runner: pqcp-arm64,
-               name: 'aarch64'
-             }}
-    name: Check API consistency
-    runs-on: ${{ matrix.target.runner }}
-    steps:
-      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
-      - name: make quickcheck
-        run: |
-          OPT=0 CFLAGS="-Imlkem -DMLK_CHECK_APIS -Wno-redundant-decls" make quickcheck
-          make clean >/dev/null
-          OPT=1 CFLAGS="-Imlkem -DMLK_CHECK_APIS -Wno-redundant-decls" make quickcheck
-      - uses: ./.github/actions/setup-apt
-      - name: tests func
-        run: |
-          ./scripts/tests func --cflags="-Imlkem -DMLK_CHECK_APIS -Wno-redundant-decls"
-  ec2_functests:
-    strategy:
-      fail-fast: false
-      matrix:
-        target:
-          - name: AMD EPYC 4th gen (t3a)
-            ec2_instance_type: t3a.small
-            ec2_ami: ubuntu-latest (x86_64)
-            ec2_volume_size: 20
-            compile_mode: native
-            opt: all
-            config_variations: 'native-cap-CPUID_AVX2'
-          - name: Intel Xeon 4th gen (t3)
-            ec2_instance_type: t3.small
-            ec2_ami: ubuntu-latest (x86_64)
-            ec2_volume_size: 20
-            compile_mode: native
-            opt: all
-            config_variations: 'native-cap-CPUID_AVX2'
-          - name: Graviton2 (c6g.medium)
-            ec2_instance_type: c6g.medium
-            ec2_ami: ubuntu-latest (aarch64)
-            ec2_volume_size: 20
-            compile_mode: native
-            opt: all
-            config_variations: 'native-cap-ON native-cap-OFF native-cap-ID_AA64PFR1_EL1'
-          - name: Graviton3 (c7g.medium)
-            ec2_instance_type: c7g.medium
-            ec2_ami: ubuntu-latest (aarch64)
-            ec2_volume_size: 20
-            compile_mode: native
-            opt: all
-            config_variations: 'native-cap-ID_AA64PFR1_EL1'
-    name: Platform tests  (${{ matrix.target.name }})
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
-    uses: ./.github/workflows/ci_ec2_reusable.yml
-    with:
-      name: ${{ matrix.target.name }}
-      ec2_instance_type: ${{ matrix.target.ec2_instance_type }}
-      ec2_ami: ${{ matrix.target.ec2_ami }}
-      ec2_ami_id: ${{ matrix.target.ec2_ami_id }}
-      compile_mode: ${{ matrix.target.compile_mode }}
-      opt: ${{ matrix.target.opt }}
-      config_variations: ${{ matrix.target.config_variations || '' }}
-      functest: true
-      kattest: true
-      acvptest: true
-      lint: false
-      verbose: true
-    secrets: inherit
-  compatibility_tests:
-    strategy:
-      max-parallel: 4
-      fail-fast: false
-      matrix:
-        container:
-          - id: debian:bullseye
-          - id: debian:bookworm
-          - id: nixos/nix:latest
-            nix_shell: 'nix-shell -p python3 gcc gnumake perl'
-    name: Compatibility tests (${{ matrix.container.id }})
-    runs-on: ubuntu-latest
-    container:
-      ${{ matrix.container.id }}
-    steps:
-      # We're not using the checkout action here because on it's not supported
-      # on all containers we want to test. Resort to a manual checkout.
+  # build_kat:
+  #   strategy:
+  #     fail-fast: false
+  #     matrix:
+  #       external:
+  #        - ${{ github.repository_owner != 'pq-code-package' }}
+  #       target:
+  #        - runner: macos-latest
+  #          name: 'MacOS (aarch64)'
+  #          arch: mac
+  #          mode: native
+  #          nix_shell: ci
+  #        - runner: macos-15-intel
+  #          name: 'MacOS (x86_64)'
+  #          arch: mac
+  #          mode: native
+  #          nix_shell: ci
+  #        - runner: pqcp-arm64
+  #          name: 'ubuntu-latest (aarch64)'
+  #          arch: aarch64
+  #          mode: native
+  #          nix_shell: ci
+  #        - runner: pqcp-arm64
+  #          name: 'ubuntu-latest (aarch64)'
+  #          arch: x86_64
+  #          mode: cross-x86_64
+  #          nix_shell: ci-cross-x86_64
+  #        - runner: pqcp-arm64
+  #          name: 'ubuntu-latest (aarch64)'
+  #          arch: riscv64
+  #          mode: cross-riscv64
+  #          nix_shell: ci-cross-riscv64
+  #        - runner: pqcp-arm64
+  #          name: 'ubuntu-latest (aarch64)'
+  #          arch: riscv32
+  #          mode: cross-riscv32
+  #          nix_shell: ci-cross-riscv32
+  #        - runner: pqcp-arm64
+  #          name: 'ubuntu-latest (ppc64le)'
+  #          arch: ppc64le
+  #          mode: cross-ppc64le
+  #          nix_shell: ci-cross-ppc64le
+  #        - runner: pqcp-x64
+  #          name: 'ubuntu-latest (x86_64)'
+  #          arch: x86_64
+  #          mode: native
+  #          nix_shell: ci
+  #        - runner: pqcp-x64
+  #          name: 'ubuntu-latest (x86_64)'
+  #          arch: aarch64
+  #          mode: cross-aarch64
+  #          nix_shell: ci-cross-aarch64
+  #        - runner: pqcp-x64
+  #          name: 'ubuntu-latest (x86_64)'
+  #          arch: aarch64_be
+  #          mode: cross-aarch64_be
+  #          nix_shell: ci-cross-aarch64_be
+  #       exclude:
+  #         - {external: true,
+  #            target: {
+  #              runner: pqcp-arm64,
+  #              name: 'ubuntu-latest (aarch64)',
+  #              arch: aarch64,
+  #              mode: native,
+  #              nix_shell: ci
+  #            }}
+  #         - {external: true,
+  #            target: {
+  #              runner: pqcp-arm64,
+  #              name: 'ubuntu-latest (aarch64)',
+  #              arch: x86_64,
+  #              mode: cross-x86_64,
+  #              nix_shell: ci-cross-x86_64
+  #            }}
+  #         - {external: true,
+  #            target: {
+  #              runner: pqcp-arm64,
+  #              name: 'ubuntu-latest (aarch64)',
+  #              arch: riscv64,
+  #              mode: cross-riscv64,
+  #              nix_shell: ci-cross-riscv64
+  #            }}
+  #         - {external: true,
+  #            target: {
+  #              runner: pqcp-arm64,
+  #              name: 'ubuntu-latest (aarch64)',
+  #              arch: riscv32,
+  #              mode: cross-riscv32,
+  #              nix_shell: ci-cross-riscv32
+  #            }}
+  #         - {external: true,
+  #            target: {
+  #              runner: pqcp-arm64,
+  #              name: 'ubuntu-latest (ppc64le)',
+  #              arch: ppc64le,
+  #              mode: cross-ppc64le,
+  #              nix_shell: ci-cross-ppc64le
+  #            }}
+  #         - {external: true,
+  #            target: {
+  #              runner: pqcp-x64,
+  #              name: 'ubuntu-latest (x86_64)',
+  #              arch: x86_64,
+  #              mode: native,
+  #              nix_shell: ci
+  #            }}
+  #         - {external: true,
+  #            target: {
+  #              runner: pqcp-x64,
+  #              name: 'ubuntu-latest (x86_64)',
+  #              arch: aarch64,
+  #              mode: cross-aarch64,
+  #              nix_shell: ci-cross-aarch64
+  #            }}
+  #         - {external: true,
+  #            target: {
+  #              runner: pqcp-x64,
+  #              name: 'ubuntu-latest (x86_64)',
+  #              arch: aarch64_be,
+  #              mode: cross-aarch64_be,
+  #              nix_shell: ci-cross-aarch64_be
+  #            }}
+  #   name: Functional tests (${{ matrix.target.arch }}${{ matrix.target.mode != 'native' && ', cross' || ''}})
+  #   runs-on: ${{ matrix.target.runner }}
+  #   steps:
+  #     - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+  #     - name: build + test (no-opt)
+  #       uses: ./.github/actions/multi-functest
+  #       with:
+  #         nix-shell: ${{ matrix.target.nix_shell }}
+  #         nix-cache: ${{ matrix.target.mode == 'native' && 'false' || 'true' }}
+  #         gh_token: ${{ secrets.GITHUB_TOKEN }}
+  #         compile_mode: ${{ matrix.target.mode }}
+  #         opt: 'no_opt'
+  #     - name: build + test (+debug+memsan+ubsan, native)
+  #       uses: ./.github/actions/multi-functest
+  #       if: ${{ matrix.target.mode == 'native' }}
+  #       with:
+  #         gh_token: ${{ secrets.GITHUB_TOKEN }}
+  #         compile_mode: native
+  #         cflags: "-DMLKEM_DEBUG -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all"
+  #         ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all"
+  #         check_namespace: 'false'
+  #     - name: build + test (cross, opt)
+  #       uses: ./.github/actions/multi-functest
+  #       # There is no native code yet on PPC64LE, riscv32 or AArch64_be, so no point running opt tests
+  #       if: ${{ matrix.target.mode != 'native' && (matrix.target.arch != 'ppc64le' && matrix.target.arch != 'riscv32' && matrix.target.arch != 'aarch64_be') }}
+  #       with:
+  #         nix-shell: ${{ matrix.target.nix_shell }}
+  #         nix-cache: ${{ matrix.target.mode == 'native' && 'false' || 'true' }}
+  #         gh_token: ${{ secrets.GITHUB_TOKEN }}
+  #         compile_mode: ${{ matrix.target.mode }}
+  #         opt: 'opt'
+  #     - name: build + test (cross, opt, +debug)
+  #       uses: ./.github/actions/multi-functest
+  #       # There is no native code yet on PPC64LE, riscv32 or AArch64_be, so no point running opt tests
+  #       if: ${{ matrix.target.mode != 'native' && (matrix.target.arch != 'ppc64le' && matrix.target.arch != 'riscv32' && matrix.target.arch != 'aarch64_be') }}
+  #       with:
+  #         nix-shell: ${{ matrix.target.nix_shell }}
+  #         nix-cache: ${{ matrix.target.mode == 'native' && 'false' || 'true' }}
+  #         gh_token: ${{ secrets.GITHUB_TOKEN }}
+  #         compile_mode: ${{ matrix.target.mode }}
+  #         cflags: "-DMLKEM_DEBUG"
+  #         opt: 'opt'
+  # backend_tests:
+  #   name: AArch64 FIPS202 backends (${{ matrix.backend }})
+  #   strategy:
+  #     fail-fast: false
+  #     matrix:
+  #       backend: [x1_scalar, x1_v84a, x2_v84a, x4_v8a_scalar, x4_v8a_v84a_scalar]
+  #   runs-on: macos-latest
+  #   steps:
+  #     - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+  #     - name: build + test
+  #       uses: ./.github/actions/multi-functest
+  #       with:
+  #         nix-shell: 'ci'
+  #         nix-cache: 'false'
+  #         gh_token: ${{ secrets.GITHUB_TOKEN }}
+  #         compile_mode: 'native'
+  #         opt: 'opt'
+  #         examples: 'false'
+  #         cflags: "-DMLKEM_DEBUG -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all"
+  #         ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all"
+  #         check_namespace: 'false'
+  #         extra_args: "--fips202-aarch64-backend ${{ matrix.backend }}"
+  # compiler_tests:
+  #   name: Compiler tests  (${{ matrix.compiler.name }}, ${{ matrix.target.name }}, ${{ matrix.cflags }})
+  #   strategy:
+  #     fail-fast: false
+  #     matrix:
+  #       cflags: [ "-O0", "-Os", "-O3" ]
+  #       target:
+  #        - runner: pqcp-arm64
+  #          name: 'aarch64'
+  #        - runner: ubuntu-latest
+  #          name: 'x86_64'
+  #        - runner: macos-latest
+  #          name: 'macos'
+  #       compiler:
+  #        - name: gcc-4.8
+  #          shell: ci_gcc48
+  #          darwin: False
+  #          c17: False
+  #          c23: False
+  #          opt: all
+  #          examples: true
+  #        - name: gcc-4.9
+  #          shell: ci_gcc49
+  #          darwin: False
+  #          c17: False
+  #          c23: False
+  #          opt: all
+  #          examples: true
+  #        - name: gcc-7
+  #          shell: ci_gcc7
+  #          darwin: False
+  #          c17: False
+  #          c23: False
+  #          opt: all
+  #          examples: true
+  #        - name: gcc-11
+  #          shell: ci_gcc11
+  #          darwin: True
+  #          c17: True
+  #          c23: False
+  #          opt: all
+  #          examples: true
+  #        - name: gcc-13
+  #          shell: ci_gcc13
+  #          darwin: True
+  #          c17: True
+  #          c23: False
+  #          opt: all
+  #          examples: true
+  #        - name: gcc-14
+  #          shell: ci_gcc14
+  #          darwin: True
+  #          c17: True
+  #          c23: True
+  #          opt: all
+  #          examples: true
+  #        - name: gcc-15
+  #          shell: ci_gcc15
+  #          # TODO: Add this once gcc15 is supported in nix on aarch64-Darwin
+  #          darwin: False
+  #          c17: True
+  #          c23: True
+  #          opt: all
+  #          examples: true
+  #        - name: clang-18
+  #          shell: ci_clang18
+  #          darwin: True
+  #          c17: True
+  #          c23: True
+  #          opt: all
+  #          examples: true
+  #        - name: clang-19
+  #          shell: ci_clang19
+  #          darwin: True
+  #          c17: True
+  #          c23: True
+  #          opt: all
+  #          examples: true
+  #        - name: clang-20
+  #          shell: ci_clang20
+  #          darwin: True
+  #          c17: True
+  #          c23: True
+  #          opt: all
+  #          examples: true
+  #        - name: clang-21
+  #          shell: ci_clang21
+  #          darwin: True
+  #          c17: True
+  #          c23: True
+  #          opt: all
+  #          examples: true
+  #        # CPU flags are not correctly passed to the zig assembler
+  #        # https://github.com/ziglang/zig/issues/23576
+  #        # We therefore only test the C backend
+  #        #
+  #        # We omit all examples since there is currently no way to run
+  #        # only those examples not involving native code.
+  #        - name: zig-0.12
+  #          shell: ci_zig0_12
+  #          darwin: True
+  #          c17: True
+  #          c23: False
+  #          examples: False
+  #          opt: no_opt
+  #        - name: zig-0.13
+  #          shell: ci_zig0_13
+  #          darwin: True
+  #          c17: True
+  #          c23: False
+  #          examples: False
+  #          opt: no_opt
+  #        - name: zig-0.14
+  #          shell: ci_zig0_14
+  #          darwin: True
+  #          c17: True
+  #          c23: True
+  #          examples: False
+  #          opt: no_opt
+  #        - name: zig-0.15
+  #          shell: ci_zig0_15
+  #          darwin: True
+  #          c17: True
+  #          c23: True
+  #          examples: False
+  #          opt: no_opt
+  #   runs-on: ${{ matrix.target.runner }}
+  #   steps:
+  #     - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+  #     - name: native build+functest (default)
+  #       if: ${{ matrix.compiler.darwin || matrix.target.runner != 'macos-latest' }}
+  #       uses: ./.github/actions/multi-functest
+  #       with:
+  #         gh_token: ${{ secrets.GITHUB_TOKEN }}
+  #         compile_mode: native
+  #         func: true
+  #         kat: false
+  #         acvp: false
+  #         examples: ${{ matrix.compiler.examples }}
+  #         opt: ${{ matrix.compiler.opt }}
+  #         nix-shell: ${{ matrix.compiler.shell }}
+  #         cflags: "${{ matrix.cflags }}"
+  #     - name: native build+functest (C90)
+  #       if: ${{ matrix.compiler.darwin || matrix.target.runner != 'macos-latest' }}
+  #       uses: ./.github/actions/multi-functest
+  #       with:
+  #         gh_token: ${{ secrets.GITHUB_TOKEN }}
+  #         compile_mode: native
+  #         func: true
+  #         kat: false
+  #         acvp: false
+  #         examples: ${{ matrix.compiler.examples }}
+  #         opt: ${{ matrix.compiler.opt }}
+  #         nix-shell: ${{ matrix.compiler.shell }}
+  #         cflags: "-std=c90 ${{ matrix.cflags }}"
+  #     - name: native build+functest (C99)
+  #       if: ${{ matrix.compiler.darwin || matrix.target.runner != 'macos-latest' }}
+  #       uses: ./.github/actions/multi-functest
+  #       with:
+  #         gh_token: ${{ secrets.GITHUB_TOKEN }}
+  #         compile_mode: native
+  #         func: true
+  #         kat: false
+  #         acvp: false
+  #         examples: ${{ matrix.compiler.examples }}
+  #         opt: ${{ matrix.compiler.opt }}
+  #         nix-shell: ${{ matrix.compiler.shell }}
+  #         cflags: "-std=c99 ${{ matrix.cflags }}"
+  #     - name: native build+functest (C11)
+  #       if: ${{ matrix.compiler.darwin || matrix.target.runner != 'macos-latest' }}
+  #       uses: ./.github/actions/multi-functest
+  #       with:
+  #         gh_token: ${{ secrets.GITHUB_TOKEN }}
+  #         compile_mode: native
+  #         func: true
+  #         kat: false
+  #         acvp: false
+  #         examples: ${{ matrix.compiler.examples }}
+  #         opt: ${{ matrix.compiler.opt }}
+  #         nix-shell: ${{ matrix.compiler.shell }}
+  #         cflags: "-std=c11 ${{ matrix.cflags }}"
+  #     - name: native build+functest (C17)
+  #       if: ${{ (matrix.compiler.darwin || matrix.target.runner != 'macos-latest') &&
+  #               matrix.compiler.c17 }}
+  #       uses: ./.github/actions/multi-functest
+  #       with:
+  #         gh_token: ${{ secrets.GITHUB_TOKEN }}
+  #         compile_mode: native
+  #         func: true
+  #         kat: false
+  #         acvp: false
+  #         examples: ${{ matrix.compiler.examples }}
+  #         opt: ${{ matrix.compiler.opt }}
+  #         nix-shell: ${{ matrix.compiler.shell }}
+  #         cflags: "-std=c17 ${{ matrix.cflags }}"
+  #     - name: native build+functest (C23)
+  #       if: ${{ (matrix.compiler.darwin || matrix.target.runner != 'macos-latest') &&
+  #               matrix.compiler.c23 }}
+  #       uses: ./.github/actions/multi-functest
+  #       with:
+  #         gh_token: ${{ secrets.GITHUB_TOKEN }}
+  #         compile_mode: native
+  #         func: true
+  #         kat: false
+  #         acvp: false
+  #         examples: ${{ matrix.compiler.examples }}
+  #         opt: ${{ matrix.compiler.opt }}
+  #         nix-shell: ${{ matrix.compiler.shell }}
+  #         cflags: "-std=c23 ${{ matrix.cflags }}"
+  # stack_analysis:
+  #   name: Stack analysis (${{ matrix.target.name }}, ${{ matrix.cflags }})
+  #   strategy:
+  #     fail-fast: false
+  #     matrix:
+  #       external:
+  #        - ${{ github.repository_owner != 'pq-code-package' }}
+  #       target:
+  #         - runner: pqcp-x64
+  #           name: x86_64
+  #         - runner: pqcp-arm64
+  #           name: aarch64
+  #       cflags: ['-O3', '-Os']
+  #       exclude:
+  #         - external: true
+  #   runs-on: ${{ matrix.target.runner }}
+  #   steps:
+  #     - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+  #     - name: Stack analysis
+  #       uses: ./.github/actions/multi-functest
+  #       with:
+  #         gh_token: ${{ secrets.GITHUB_TOKEN }}
+  #         compile_mode: native
+  #         nix-shell: ci_valgrind-varlat_gcc15
+  #         nix-cache: false
+  #         opt: all
+  #         cflags: "${{ matrix.cflags }}"
+  #         func: false
+  #         kat: false
+  #         acvp: false
+  #         examples: false
+  #         stack: true
+  #         check_namespace: false
+  # config_variations:
+  #   name: Non-standard configurations
+  #   strategy:
+  #     fail-fast: false
+  #     matrix:
+  #       external:
+  #        - ${{ github.repository_owner != 'pq-code-package' }}
+  #       target:
+  #        - runner: pqcp-arm64
+  #          name: 'ubuntu-latest (aarch64)'
+  #        - runner: pqcp-x64
+  #          name: 'ubuntu-latest (x86_64)'
+  #       exclude:
+  #         - {external: true,
+  #            target: {
+  #              runner: pqcp-arm64,
+  #              name: 'ubuntu-latest (aarch64)',
+  #            }}
+  #         - {external: true,
+  #            target: {
+  #              runner: pqcp-x64,
+  #              name: 'ubuntu-latest (x86_64)',
+  #            }}
+  #   runs-on: ${{ matrix.target.runner }}
+  #   steps:
+  #     - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+  #     - name: "Config Variations"
+  #       uses: ./.github/actions/config-variations
+  #       with:
+  #         gh_token: ${{ secrets.GITHUB_TOKEN }}
+  # check-cf-protections:
+  #   name: Test control-flow protections  (${{ matrix.compiler.name }}, x86_64)
+  #   strategy:
+  #     fail-fast: false
+  #     matrix:
+  #       compiler:
+  #        - name: gcc-14
+  #          shell: ci_gcc14
+  #        - name: gcc-15
+  #          shell: ci_gcc15
+  #        - name: clang-19
+  #          shell: ci_clang19
+  #   # On AArch64 -fcf-protection is not supported anyway
+  #   runs-on: ubuntu-latest
+  #   steps:
+  #     - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+  #     - name: Test control-flow protections
+  #       uses: ./.github/actions/multi-functest
+  #       with:
+  #         gh_token: ${{ secrets.GITHUB_TOKEN }}
+  #         compile_mode: native
+  #         cflags: "-Wl,-z,cet-report=error -fcf-protection=full"
+  #         func: true
+  #         kat: true
+  #         acvp: true
+  #         nix-shell: ${{ matrix.compiler.shell }}
+  # # ensure that kem.h and mlkem_native.h; api.h and native backends are compatible
+  # check-apis:
+  #   strategy:
+  #     fail-fast: false
+  #     matrix:
+  #       external:
+  #        - ${{ github.repository_owner != 'pq-code-package' }}
+  #       target:
+  #        - runner: pqcp-arm64
+  #          name: 'aarch64'
+  #        - runner: ubuntu-latest
+  #          name: 'x86_64'
+  #       exclude:
+  #         - {external: true,
+  #            target: {
+  #              runner: pqcp-arm64,
+  #              name: 'aarch64'
+  #            }}
+  #   name: Check API consistency
+  #   runs-on: ${{ matrix.target.runner }}
+  #   steps:
+  #     - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+  #     - name: make quickcheck
+  #       run: |
+  #         OPT=0 CFLAGS="-Imlkem -DMLK_CHECK_APIS -Wno-redundant-decls" make quickcheck
+  #         make clean >/dev/null
+  #         OPT=1 CFLAGS="-Imlkem -DMLK_CHECK_APIS -Wno-redundant-decls" make quickcheck
+  #     - uses: ./.github/actions/setup-apt
+  #     - name: tests func
+  #       run: |
+  #         ./scripts/tests func --cflags="-Imlkem -DMLK_CHECK_APIS -Wno-redundant-decls"
+  # ec2_functests:
+  #   strategy:
+  #     fail-fast: false
+  #     matrix:
+  #       target:
+  #         - name: AMD EPYC 4th gen (t3a)
+  #           ec2_instance_type: t3a.small
+  #           ec2_ami: ubuntu-latest (x86_64)
+  #           ec2_volume_size: 20
+  #           compile_mode: native
+  #           opt: all
+  #           config_variations: 'native-cap-CPUID_AVX2'
+  #         - name: Intel Xeon 4th gen (t3)
+  #           ec2_instance_type: t3.small
+  #           ec2_ami: ubuntu-latest (x86_64)
+  #           ec2_volume_size: 20
+  #           compile_mode: native
+  #           opt: all
+  #           config_variations: 'native-cap-CPUID_AVX2'
+  #         - name: Graviton2 (c6g.medium)
+  #           ec2_instance_type: c6g.medium
+  #           ec2_ami: ubuntu-latest (aarch64)
+  #           ec2_volume_size: 20
+  #           compile_mode: native
+  #           opt: all
+  #           config_variations: 'native-cap-ON native-cap-OFF native-cap-ID_AA64PFR1_EL1'
+  #         - name: Graviton3 (c7g.medium)
+  #           ec2_instance_type: c7g.medium
+  #           ec2_ami: ubuntu-latest (aarch64)
+  #           ec2_volume_size: 20
+  #           compile_mode: native
+  #           opt: all
+  #           config_variations: 'native-cap-ID_AA64PFR1_EL1'
+  #   name: Platform tests  (${{ matrix.target.name }})
+  #   permissions:
+  #     contents: 'read'
+  #     id-token: 'write'
+  #   if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
+  #   uses: ./.github/workflows/ci_ec2_reusable.yml
+  #   with:
+  #     name: ${{ matrix.target.name }}
+  #     ec2_instance_type: ${{ matrix.target.ec2_instance_type }}
+  #     ec2_ami: ${{ matrix.target.ec2_ami }}
+  #     ec2_ami_id: ${{ matrix.target.ec2_ami_id }}
+  #     compile_mode: ${{ matrix.target.compile_mode }}
+  #     opt: ${{ matrix.target.opt }}
+  #     config_variations: ${{ matrix.target.config_variations || '' }}
+  #     functest: true
+  #     kattest: true
+  #     acvptest: true
+  #     lint: false
+  #     verbose: true
+  #   secrets: inherit
+  # compatibility_tests:
+  #   strategy:
+  #     max-parallel: 4
+  #     fail-fast: false
+  #     matrix:
+  #       container:
+  #         - id: debian:bullseye
+  #         - id: debian:bookworm
+  #         - id: nixos/nix:latest
+  #           nix_shell: 'nix-shell -p python3 gcc gnumake perl'
+  #   name: Compatibility tests (${{ matrix.container.id }})
+  #   runs-on: ubuntu-latest
+  #   container:
+  #     ${{ matrix.container.id }}
+  #   steps:
+  #     # We're not using the checkout action here because on it's not supported
+  #     # on all containers we want to test. Resort to a manual checkout.
 
-      # We can't hoist this into an action since calling an action can only
-      # be done after checkout.
-      - name: Manual checkout
-        shell: bash
-        run: |
-          if (which yum > /dev/null); then
-             yum install git -y
-          elif (which apt > /dev/null); then
-             apt update
-             apt install git -y
-          fi
+  #     # We can't hoist this into an action since calling an action can only
+  #     # be done after checkout.
+  #     - name: Manual checkout
+  #       shell: bash
+  #       run: |
+  #         if (which yum > /dev/null); then
+  #            yum install git -y
+  #         elif (which apt > /dev/null); then
+  #            apt update
+  #            apt install git -y
+  #         fi
 
-          git config --global --add safe.directory $GITHUB_WORKSPACE
-          git init
-          git remote add origin $GITHUB_SERVER_URL/$GITHUB_REPOSITORY
-          git fetch origin --depth 1 $GITHUB_SHA
-          git checkout FETCH_HEAD
-      - uses: ./.github/actions/setup-os
-        with:
-          sudo: ""
-      - name: make quickcheck
-        shell: bash
-        run: |
-          if [ -n "${{ matrix.container.nix_shell }}" ]; then
-            ${{ matrix.container.nix_shell }} --run "CC=gcc OPT=0 make quickcheck && make clean >/dev/null && CC=gcc OPT=1 make quickcheck"
-          else
-            CC=gcc OPT=0 make quickcheck
-            make clean >/dev/null
-            CC=gcc OPT=1 make quickcheck
-          fi
-      - name: Functional Tests
-        uses: ./.github/actions/multi-functest
-        with:
-          nix-shell: ""
-          custom_shell: ${{ matrix.container.nix_shell && format('{0} --run \"bash -e {{0}}\"', matrix.container.nix_shell) || 'bash' }}
-          gh_token: ${{ secrets.AWS_GITHUB_TOKEN }}
-  ec2_compatibilitytests:
-    strategy:
-      max-parallel: 8
-      fail-fast: false
-      matrix:
-        container:
-          - id: amazonlinux-2-aarch:base
-          - id: amazonlinux-2-aarch:gcc-7x
-          - id: amazonlinux-2-aarch:clang-7x
-          - id: amazonlinux-2023-aarch:base
-          - id: amazonlinux-2023-aarch:gcc-11x
-          - id: amazonlinux-2023-aarch:clang-15x
-          - id: amazonlinux-2023-aarch:clang-15x-sanitizer
-          # - id: amazonlinux-2023-aarch:cryptofuzz Not yet supported
-          - id: ubuntu-22.04-aarch:gcc-12x
-          - id: ubuntu-22.04-aarch:gcc-11x
-          - id: ubuntu-20.04-aarch:gcc-8x
-          - id: ubuntu-20.04-aarch:gcc-7x
-          - id: ubuntu-20.04-aarch:clang-9x
-          - id: ubuntu-20.04-aarch:clang-8x
-          - id: ubuntu-20.04-aarch:clang-7x-bm-framework
-          - id: ubuntu-20.04-aarch:clang-7x
-          - id: ubuntu-20.04-aarch:clang-10x
-          - id: ubuntu-22.04-aarch:base
-          - id: ubuntu-20.04-aarch:base
-    name: Compatibility tests (${{ matrix.container.id }})
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    uses: ./.github/workflows/ci_ec2_container.yml
-    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
-    with:
-      container: ${{ matrix.container.id }}
-      name: ${{ matrix.container.id }}
-      ec2_instance_type: t4g.small
-      ec2_ami: ubuntu-latest (custom AMI)
-      ec2_ami_id: ami-0c9bc1901ef0d1066 # Has docker images preinstalled
-      compile_mode: native
-      opt: all
-      functest: true
-      kattest: true
-      acvptest: true
-      lint: false
-      verbose: true
-      cflags: "-O0"
-    secrets: inherit
+  #         git config --global --add safe.directory $GITHUB_WORKSPACE
+  #         git init
+  #         git remote add origin $GITHUB_SERVER_URL/$GITHUB_REPOSITORY
+  #         git fetch origin --depth 1 $GITHUB_SHA
+  #         git checkout FETCH_HEAD
+  #     - uses: ./.github/actions/setup-os
+  #       with:
+  #         sudo: ""
+  #     - name: make quickcheck
+  #       shell: bash
+  #       run: |
+  #         if [ -n "${{ matrix.container.nix_shell }}" ]; then
+  #           ${{ matrix.container.nix_shell }} --run "CC=gcc OPT=0 make quickcheck && make clean >/dev/null && CC=gcc OPT=1 make quickcheck"
+  #         else
+  #           CC=gcc OPT=0 make quickcheck
+  #           make clean >/dev/null
+  #           CC=gcc OPT=1 make quickcheck
+  #         fi
+  #     - name: Functional Tests
+  #       uses: ./.github/actions/multi-functest
+  #       with:
+  #         nix-shell: ""
+  #         custom_shell: ${{ matrix.container.nix_shell && format('{0} --run \"bash -e {{0}}\"', matrix.container.nix_shell) || 'bash' }}
+  #         gh_token: ${{ secrets.AWS_GITHUB_TOKEN }}
+  # ec2_compatibilitytests:
+  #   strategy:
+  #     max-parallel: 8
+  #     fail-fast: false
+  #     matrix:
+  #       container:
+  #         - id: amazonlinux-2-aarch:base
+  #         - id: amazonlinux-2-aarch:gcc-7x
+  #         - id: amazonlinux-2-aarch:clang-7x
+  #         - id: amazonlinux-2023-aarch:base
+  #         - id: amazonlinux-2023-aarch:gcc-11x
+  #         - id: amazonlinux-2023-aarch:clang-15x
+  #         - id: amazonlinux-2023-aarch:clang-15x-sanitizer
+  #         # - id: amazonlinux-2023-aarch:cryptofuzz Not yet supported
+  #         - id: ubuntu-22.04-aarch:gcc-12x
+  #         - id: ubuntu-22.04-aarch:gcc-11x
+  #         - id: ubuntu-20.04-aarch:gcc-8x
+  #         - id: ubuntu-20.04-aarch:gcc-7x
+  #         - id: ubuntu-20.04-aarch:clang-9x
+  #         - id: ubuntu-20.04-aarch:clang-8x
+  #         - id: ubuntu-20.04-aarch:clang-7x-bm-framework
+  #         - id: ubuntu-20.04-aarch:clang-7x
+  #         - id: ubuntu-20.04-aarch:clang-10x
+  #         - id: ubuntu-22.04-aarch:base
+  #         - id: ubuntu-20.04-aarch:base
+  #   name: Compatibility tests (${{ matrix.container.id }})
+  #   permissions:
+  #     contents: 'read'
+  #     id-token: 'write'
+  #   uses: ./.github/workflows/ci_ec2_container.yml
+  #   if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
+  #   with:
+  #     container: ${{ matrix.container.id }}
+  #     name: ${{ matrix.container.id }}
+  #     ec2_instance_type: t4g.small
+  #     ec2_ami: ubuntu-latest (custom AMI)
+  #     ec2_ami_id: ami-0c9bc1901ef0d1066 # Has docker images preinstalled
+  #     compile_mode: native
+  #     opt: all
+  #     functest: true
+  #     kattest: true
+  #     acvptest: true
+  #     lint: false
+  #     verbose: true
+  #     cflags: "-O0"
+  #   secrets: inherit
+  # check_hol_light_bytecode:
+  #   strategy:
+  #     fail-fast: false
+  #     matrix:
+  #       target:
+  #         - system: macos-latest
+  #           nix_shell: hol_light
+  #           nix_cache: false
+  #         - system: macos-15-intel
+  #           nix_shell: hol_light
+  #           nix_cache: false
+  #         - system: ubuntu-latest
+  #           nix_shell: hol_light-cross-aarch64
+  #           nix_cache: true
+  #         - system: pqcp-arm64
+  #           nix_shell: hol_light
+  #           nix_cache: false
+  #   runs-on: ${{ matrix.target.system }}
+  #   name: Check HOL-Light bytecode ${{ matrix.target.system }}
+  #   steps:
+  #     - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+  #     - uses: ./.github/actions/setup-shell
+  #       with:
+  #         nix-shell: ${{ matrix.target.nix_shell }}
+  #         nix-cache: ${{ matrix.target.nix_cache }}
+  #         gh_token: ${{ secrets.GITHUB_TOKEN }}
+  #         script: |
+  #           python3 ./scripts/autogen --dry-run --update-hol-light-bytecode
   check_autogenerated_files:
     strategy:
       fail-fast: false
       matrix:
-        system: [ubuntu-latest, pqcp-arm64]
-    runs-on: ${{ matrix.system }}
+        target:
+          - system: macos-latest
+            nix_shell: 'ci'
+          - system: macos-15-intel
+            nix_shell: 'ci'
+          - system: ubuntu-latest
+            nix_shell: 'ci-cross'
+            extra_args: '--force-cross'
+          - system: pqcp-arm64
+            nix_shell: 'ci-cross'
+            extra_args: '--force-cross'
+    runs-on: ${{ matrix.target.system }}
     name: Check autogenerated files
     steps:
       - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
       - uses: ./.github/actions/setup-shell
         with:
-          nix-shell: 'ci-cross' # Need cross-compiler for ASM simplification
+          nix-shell: ${{ matrix.target.nix_shell }}
           nix-cache: 'true'
           gh_token: ${{ secrets.GITHUB_TOKEN }}
           script: |
-            python3 ./scripts/autogen --dry-run --force-cross
-      - uses: ./.github/actions/setup-shell
-        # Building the HOL-Light bytecode currently requires native compilation
-        if: ${{ matrix.system == 'pqcp-arm64' }}
-        with:
-          nix-shell: 'hol_light'
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          script: |
-            python3 ./scripts/autogen --dry-run --update-hol-light-bytecode
+            python3 ./scripts/autogen --dry-run ${{ matrix.target.extra_args }}
diff --git a/dev/fips202/aarch64/src/keccak_f1600_x1_v84a_asm.S b/dev/fips202/aarch64/src/keccak_f1600_x1_v84a_asm.S
index 58be4de5fb..7e5568d169 100644
--- a/dev/fips202/aarch64/src/keccak_f1600_x1_v84a_asm.S
+++ b/dev/fips202/aarch64/src/keccak_f1600_x1_v84a_asm.S
@@ -243,19 +243,19 @@
 
 /* Macros using v8.4-A SHA-3 instructions */
 
-.macro eor3_m0 d s0 s1 s2
+.macro eor3_m0 d, s0, s1, s2
     eor3 \d\().16b, \s0\().16b, \s1\().16b, \s2\().16b
 .endm
 
-.macro rax1_m0 d s0 s1
+.macro rax1_m0 d, s0, s1
     rax1 \d\().2d, \s0\().2d, \s1\().2d
 .endm
 
-.macro xar_m0 d s0 s1 imm
+.macro xar_m0 d, s0, s1, imm
     xar \d\().2d, \s0\().2d, \s1\().2d, #\imm
 .endm
 
-.macro bcax_m0 d s0 s1 s2
+.macro bcax_m0 d, s0, s1, s2
     bcax \d\().16b, \s0\().16b, \s1\().16b, \s2\().16b
 .endm
 
diff --git a/dev/fips202/aarch64/src/keccak_f1600_x2_v84a_asm.S b/dev/fips202/aarch64/src/keccak_f1600_x2_v84a_asm.S
index 4726f99071..be3608108c 100644
--- a/dev/fips202/aarch64/src/keccak_f1600_x2_v84a_asm.S
+++ b/dev/fips202/aarch64/src/keccak_f1600_x2_v84a_asm.S
@@ -225,19 +225,19 @@
 
 /* Macros using v8.4-A SHA-3 instructions */
 
-.macro eor3_m0 d s0 s1 s2
+.macro eor3_m0 d, s0, s1, s2
     eor3 \d\().16b, \s0\().16b, \s1\().16b, \s2\().16b
 .endm
 
-.macro rax1_m0 d s0 s1
+.macro rax1_m0 d, s0, s1
     rax1 \d\().2d, \s0\().2d, \s1\().2d
 .endm
 
-.macro xar_m0 d s0 s1 imm
+.macro xar_m0 d, s0, s1, imm
     xar \d\().2d, \s0\().2d, \s1\().2d, #\imm
 .endm
 
-.macro bcax_m0 d s0 s1 s2
+.macro bcax_m0 d, s0, s1, s2
     bcax \d\().16b, \s0\().16b, \s1\().16b, \s2\().16b
 .endm
 
diff --git a/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_asm.S b/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_asm.S
index 1f4ff90451..104881c0e9 100644
--- a/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_asm.S
+++ b/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_asm.S
@@ -166,24 +166,24 @@
 
 /************************ MACROS ****************************/
 
-.macro eor3_m1 d s0 s1 s2
+.macro eor3_m1 d, s0, s1, s2
    eor \d\().16b, \s0\().16b, \s1\().16b
    eor \d\().16b, \d\().16b,  \s2\().16b
 .endm
 
-.macro rax1_m1 d s0 s1
+.macro rax1_m1 d, s0, s1
    add vtmp.2d, \s1\().2d, \s1\().2d
    sri vtmp.2d, \s1\().2d, #63
    eor \d\().16b, vtmp.16b, \s0\().16b
 .endm
 
-.macro xar_m1 d s0 s1 imm
+.macro xar_m1 d, s0, s1, imm
    eor vtmp.16b, \s0\().16b, \s1\().16b
    shl \d\().2d, vtmp.2d, #(64-\imm)
    sri \d\().2d, vtmp.2d, #(\imm)
 .endm
 
-.macro bcax_m1 d s0 s1 s2
+.macro bcax_m1 d, s0, s1, s2
     bic vtmp.16b, \s1\().16b, \s2\().16b
     eor \d\().16b, vtmp.16b, \s0\().16b
 .endm
diff --git a/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_asm.S b/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_asm.S
index 34b3305fdc..3b6c4298b4 100644
--- a/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_asm.S
+++ b/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_asm.S
@@ -168,40 +168,40 @@
 
 /************************ MACROS ****************************/
 
-.macro eor3_m0 d s0 s1 s2
+.macro eor3_m0 d, s0, s1, s2
     eor3 \d\().16b, \s0\().16b, \s1\().16b, \s2\().16b
 .endm
 
-.macro rax1_m0 d s0 s1
+.macro rax1_m0 d, s0, s1
     rax1 \d\().2d, \s0\().2d, \s1\().2d
 .endm
 
-.macro xar_m0 d s0 s1 imm
+.macro xar_m0 d, s0, s1, imm
     xar \d\().2d, \s0\().2d, \s1\().2d, #\imm
 .endm
 
-.macro bcax_m0 d s0 s1 s2
+.macro bcax_m0 d, s0, s1, s2
     bcax \d\().16b, \s0\().16b, \s1\().16b, \s2\().16b
 .endm
 
-.macro eor3_m1 d s0 s1 s2
+.macro eor3_m1 d, s0, s1, s2
    eor \d\().16b, \s0\().16b, \s1\().16b
    eor \d\().16b, \d\().16b,  \s2\().16b
 .endm
 
-.macro rax1_m1 d s0 s1
+.macro rax1_m1 d, s0, s1
    add vtmp.2d, \s1\().2d, \s1\().2d
    sri vtmp.2d, \s1\().2d, #63
    eor \d\().16b, vtmp.16b, \s0\().16b
 .endm
 
-.macro xar_m1 d s0 s1 imm
+.macro xar_m1 d, s0, s1, imm
    eor vtmp.16b, \s0\().16b, \s1\().16b
    shl \d\().2d, vtmp.2d, #(64-\imm)
    sri \d\().2d, vtmp.2d, #(\imm)
 .endm
 
-.macro bcax_m1 d s0 s1 s2
+.macro bcax_m1 d, s0, s1, s2
     bic vtmp.16b, \s1\().16b, \s2\().16b
     eor \d\().16b, vtmp.16b, \s0\().16b
 .endm
diff --git a/dev/fips202/aarch64_symbolic/keccak_f1600_x4_v8a_scalar_hybrid_clean.S b/dev/fips202/aarch64_symbolic/keccak_f1600_x4_v8a_scalar_hybrid_clean.S
index 2c19bc7dab..4ebc76ad18 100644
--- a/dev/fips202/aarch64_symbolic/keccak_f1600_x4_v8a_scalar_hybrid_clean.S
+++ b/dev/fips202/aarch64_symbolic/keccak_f1600_x4_v8a_scalar_hybrid_clean.S
@@ -166,24 +166,24 @@
 
 /************************ MACROS ****************************/
 
-.macro eor3_m1 d s0 s1 s2
+.macro eor3_m1 d, s0, s1, s2
    eor \d\().16b, \s0\().16b, \s1\().16b
    eor \d\().16b, \d\().16b,  \s2\().16b
 .endm
 
-.macro rax1_m1 d s0 s1
+.macro rax1_m1 d, s0, s1
    add vtmp.2d, \s1\().2d, \s1\().2d
    sri vtmp.2d, \s1\().2d, #63
    eor \d\().16b, vtmp.16b, \s0\().16b
 .endm
 
-.macro xar_m1 d s0 s1 imm
+.macro xar_m1 d, s0, s1, imm
    eor vtmp.16b, \s0\().16b, \s1\().16b
    shl \d\().2d, vtmp.2d, #(64-\imm)
    sri \d\().2d, vtmp.2d, #(\imm)
 .endm
 
-.macro bcax_m1 d s0 s1 s2
+.macro bcax_m1 d, s0, s1, s2
     bic vtmp.16b, \s1\().16b, \s2\().16b
     eor \d\().16b, vtmp.16b, \s0\().16b
 .endm
diff --git a/dev/fips202/aarch64_symbolic/keccak_f1600_x4_v8a_v84a_scalar_hybrid_clean.S b/dev/fips202/aarch64_symbolic/keccak_f1600_x4_v8a_v84a_scalar_hybrid_clean.S
index d02d9503ae..61c7a16a45 100644
--- a/dev/fips202/aarch64_symbolic/keccak_f1600_x4_v8a_v84a_scalar_hybrid_clean.S
+++ b/dev/fips202/aarch64_symbolic/keccak_f1600_x4_v8a_v84a_scalar_hybrid_clean.S
@@ -168,40 +168,40 @@
 
 /************************ MACROS ****************************/
 
-.macro eor3_m0 d s0 s1 s2
+.macro eor3_m0 d, s0, s1, s2
     eor3 \d\().16b, \s0\().16b, \s1\().16b, \s2\().16b
 .endm
 
-.macro rax1_m0 d s0 s1
+.macro rax1_m0 d, s0, s1
     rax1 \d\().2d, \s0\().2d, \s1\().2d
 .endm
 
-.macro xar_m0 d s0 s1 imm
+.macro xar_m0 d, s0, s1, imm
     xar \d\().2d, \s0\().2d, \s1\().2d, #\imm
 .endm
 
-.macro bcax_m0 d s0 s1 s2
+.macro bcax_m0 d, s0, s1, s2
     bcax \d\().16b, \s0\().16b, \s1\().16b, \s2\().16b
 .endm
 
-.macro eor3_m1 d s0 s1 s2
+.macro eor3_m1 d, s0, s1, s2
    eor \d\().16b, \s0\().16b, \s1\().16b
    eor \d\().16b, \d\().16b,  \s2\().16b
 .endm
 
-.macro rax1_m1 d s0 s1
+.macro rax1_m1 d, s0, s1
    add vtmp.2d, \s1\().2d, \s1\().2d
    sri vtmp.2d, \s1\().2d, #63
    eor \d\().16b, vtmp.16b, \s0\().16b
 .endm
 
-.macro xar_m1 d s0 s1 imm
+.macro xar_m1 d, s0, s1, imm
    eor vtmp.16b, \s0\().16b, \s1\().16b
    shl \d\().2d, vtmp.2d, #(64-\imm)
    sri \d\().2d, vtmp.2d, #(\imm)
 .endm
 
-.macro bcax_m1 d s0 s1 s2
+.macro bcax_m1 d, s0, s1, s2
     bic vtmp.16b, \s1\().16b, \s2\().16b
     eor \d\().16b, vtmp.16b, \s0\().16b
 .endm
diff --git a/dev/x86_64/src/fq.inc b/dev/x86_64/src/fq.inc
index 647011e208..86202f5b2c 100644
--- a/dev/x86_64/src/fq.inc
+++ b/dev/x86_64/src/fq.inc
@@ -8,7 +8,7 @@
  * AVX2 Kyber implementation @[REF_AVX2].
  */
 
-.macro red16 r,rs=0,x=12
+.macro red16 r, rs=0, x=12
 vpmulhw         %ymm1,%ymm\r,%ymm\x
 .if \rs
 vpmulhrsw	%ymm\rs,%ymm\x,%ymm\x
@@ -19,14 +19,14 @@ vpmullw         %ymm0,%ymm\x,%ymm\x
 vpsubw          %ymm\x,%ymm\r,%ymm\r
 .endm
 
-.macro csubq r,x=12
+.macro csubq r, x=12
 vpsubw		%ymm0,%ymm\r,%ymm\r
 vpsraw		$15,%ymm\r,%ymm\x
 vpand		%ymm0,%ymm\x,%ymm\x
 vpaddw		%ymm\x,%ymm\r,%ymm\r
 .endm
 
-.macro caddq r,x=12
+.macro caddq r, x=12
 vpsraw		$15,%ymm\r,%ymm\x
 vpand		%ymm0,%ymm\x,%ymm\x
 vpaddw		%ymm\x,%ymm\r,%ymm\r
@@ -34,7 +34,7 @@ vpaddw		%ymm\x,%ymm\r,%ymm\r
 
 /* Montgomery multiplication between b and ah,
  * with Montgomery twist of ah in al. */
-.macro fqmulprecomp al,ah,b,x=12
+.macro fqmulprecomp al, ah, b, x=12
 vpmullw		%ymm\al,%ymm\b,%ymm\x
 vpmulhw		%ymm\ah,%ymm\b,%ymm\b
 vpmulhw		%ymm0,%ymm\x,%ymm\x
diff --git a/dev/x86_64/src/intt.S b/dev/x86_64/src/intt.S
index 649ee424b0..727d0c5b73 100644
--- a/dev/x86_64/src/intt.S
+++ b/dev/x86_64/src/intt.S
@@ -41,7 +41,7 @@
  * Butterflies 0,1 use root zh0 and twisted root zl0, and butterflies
  * 2,3 use root zh1 and twisted root zl1
  * Results are again in rl{0-3} and rh{0-3} */
-.macro butterfly rl0,rl1,rl2,rl3,rh0,rh1,rh2,rh3,zl0=2,zl1=2,zh0=3,zh1=3
+.macro butterfly rl0, rl1, rl2, rl3, rh0, rh1, rh2, rh3, zl0=2, zl1=2, zh0=3, zh1=3
 vpsubw		%ymm\rl0,%ymm\rh0,%ymm12    /* ymm12 = rh0 - rl0 */
 vpaddw		%ymm\rh0,%ymm\rl0,%ymm\rl0  /* rl0   = rh0 + rl0 */
 vpsubw		%ymm\rl1,%ymm\rh1,%ymm13    /* ymm13 = rh1 - rl1 */
@@ -121,7 +121,7 @@ vpshufb		%ymm12,%ymm1,%ymm1
 vpshufb		%ymm12,%ymm2,%ymm2
 vpshufb		%ymm12,%ymm3,%ymm3
 
-butterfly	4,5,8,9,6,7,10,11,15,1,2,3
+butterfly	4, 5, 8, 9, 6, 7, 10, 11, 15, 1, 2, 3
 
 /* Montgmoery multiplication with a signed canonical twiddle
  * always has absolute value < q. This is used henceforth to
@@ -137,7 +137,7 @@ vmovdqa		MLK_AVX2_BACKEND_DATA_OFFSET_REVIDXB*2(%rsi),%ymm1
 vpshufb		%ymm1,%ymm2,%ymm2
 vpshufb		%ymm1,%ymm3,%ymm3
 
-butterfly	4,5,6,7,8,9,10,11,2,2,3,3
+butterfly	4, 5, 6, 7, 8, 9, 10, 11, 2, 2, 3, 3
 
 /* For 8,9,10,11, it is sufficient to use the bound <q (much weaker
  * than what we used above) for the absolute value of the Montgomery
@@ -154,7 +154,7 @@ vmovdqa		MLK_AVX2_BACKEND_DATA_OFFSET_REVIDXD*2(%rsi),%ymm12
 vpermd		(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+(1-\off)*224+112)*2(%rsi),%ymm12,%ymm2
 vpermd		(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+(1-\off)*224+128)*2(%rsi),%ymm12,%ymm10
 
-butterfly	3,4,6,8,5,7,9,11,2,2,10,10
+butterfly	3, 4, 6, 8, 5, 7, 9, 11, 2, 2, 10, 10
 /* 3 abs bound < 8q, 4 abs bound < 4q, 6,8 abs bound < 2q, 5,7,9,11 abs bound < q */
 
 // Broadcast 20159 (0x4ebf) to all elements of ymm1
@@ -173,7 +173,7 @@ shuffle2	9,11,5,11  // 5,11 abs bound < q
 vpermq		$0x1B,(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+(1-\off)*224+80)*2(%rsi),%ymm2
 vpermq		$0x1B,(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+(1-\off)*224+96)*2(%rsi),%ymm9
 
-butterfly	10,3,6,5,4,8,7,11,2,2,9,9
+butterfly	10, 3, 6, 5, 4, 8, 7, 11, 2, 2, 9, 9
 /* 10 abs bound < 8q
  * 3 abs bound < 4q
  * 5,6 abs bound < 2q
@@ -198,7 +198,7 @@ shuffle4	7,11,4,11  /* 4,11 abs bound < q */
 vpermq		$0x4E,(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+(1-\off)*224+48)*2(%rsi),%ymm2
 vpermq		$0x4E,(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+(1-\off)*224+64)*2(%rsi),%ymm7
 
-butterfly	9,10,6,4,3,5,8,11,2,2,7,7
+butterfly	9, 10, 6, 4, 3, 5, 8, 11, 2, 2, 7, 7
 /* 9 abs bound < 8q
  * 10 abs bound < 4q
  * 4,6 abs bound <2q
@@ -217,7 +217,7 @@ shuffle8	8,11,3,11  /* 3,11 abs bound < q */
 vmovdqa		(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+(1-\off)*224+16)*2(%rsi),%ymm2
 vmovdqa		(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+(1-\off)*224+32)*2(%rsi),%ymm8
 
-butterfly	7,9,6,3,10,4,5,11,2,2,8,8
+butterfly	7, 9, 6, 3, 10, 4, 5, 11, 2, 2, 8, 8
 /* 7         abs bound <8q
  * 9         abs bound <4q
  * 6,3       abs bound < 2q
@@ -254,7 +254,7 @@ vmovdqa         (64*\off+ 48)*2(%rdi),%ymm7
 vmovdqa         (64*\off+176)*2(%rdi),%ymm11
 vpbroadcastq	(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+4)*2(%rsi),%ymm3
 
-butterfly	4,5,6,7,8,9,10,11
+butterfly	4, 5, 6, 7, 8, 9, 10, 11
 /* global abs bound < 8q */
 
 /* REF-CHANGE: The official AVX2 implementation has a `red16 4` for `off=0`.
diff --git a/dev/x86_64/src/ntt.S b/dev/x86_64/src/ntt.S
index 4df9f88a4e..89208b30f2 100644
--- a/dev/x86_64/src/ntt.S
+++ b/dev/x86_64/src/ntt.S
@@ -33,7 +33,7 @@
 #include "shuffle.inc"
 
 /* Compute steps 1,2 / 3 of Montgomery multiplication */
-.macro mul rh0,rh1,rh2,rh3,zl0=15,zl1=15,zh0=2,zh1=2
+.macro mul rh0, rh1, rh2, rh3, zl0=15, zl1=15, zh0=2, zh1=2
 vpmullw		%ymm\zl0,%ymm\rh0,%ymm12
 vpmullw		%ymm\zl0,%ymm\rh1,%ymm13
 
@@ -75,7 +75,7 @@ vpmulhw		%ymm0,%ymm15,%ymm15
  * Since the result of the Montgomery multiplication is bounded
  * by q in absolute value, the coefficients overall grow by not
  * more than q in absolute value per layer. */
-.macro update rln,rl0,rl1,rl2,rl3,rh0,rh1,rh2,rh3
+.macro update rln, rl0, rl1, rl2, rl3, rh0, rh1, rh2, rh3
 vpaddw		%ymm\rh0,%ymm\rl0,%ymm\rln /* rln = rl0 + rh0 */
 vpsubw		%ymm\rh0,%ymm\rl0,%ymm\rh0 /* rh0 = rl0 - rh0 */
 vpaddw		%ymm\rh1,%ymm\rl1,%ymm\rl0 /* rl0 = rl1 + rh1 */
@@ -103,7 +103,7 @@ vmovdqa		(64*\off+160)*2(%rdi),%ymm10
 vmovdqa		(64*\off+176)*2(%rdi),%ymm11
 vpbroadcastq	(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+4)*2(%rsi),%ymm2
 
-mul		8,9,10,11
+mul		8, 9, 10, 11
 
 vmovdqa		(64*\off+  0)*2(%rdi),%ymm4
 vmovdqa		(64*\off+ 16)*2(%rdi),%ymm5
@@ -111,7 +111,7 @@ vmovdqa		(64*\off+ 32)*2(%rdi),%ymm6
 vmovdqa		(64*\off+ 48)*2(%rdi),%ymm7
 
 reduce
-update		3,4,5,6,7,8,9,10,11
+update		3, 4, 5, 6, 7, 8, 9, 10, 11
 
 vmovdqa		%ymm3,(64*\off+  0)*2(%rdi)
 vmovdqa		%ymm4,(64*\off+ 16)*2(%rdi)
@@ -132,7 +132,7 @@ vmovdqa		(128*\off+ 96)*2(%rdi),%ymm10
 vmovdqa		(128*\off+112)*2(%rdi),%ymm11
 vmovdqa		(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+224*\off+32)*2(%rsi),%ymm2
 
-mul		8,9,10,11
+mul		8, 9, 10, 11
 
 vmovdqa		(128*\off+  0)*2(%rdi),%ymm4
 vmovdqa	 	(128*\off+ 16)*2(%rdi),%ymm5
@@ -140,7 +140,7 @@ vmovdqa		(128*\off+ 32)*2(%rdi),%ymm6
 vmovdqa		(128*\off+ 48)*2(%rdi),%ymm7
 
 reduce
-update		3,4,5,6,7,8,9,10,11
+update		3, 4, 5, 6, 7, 8, 9, 10, 11
 
 /* level 2 */
 shuffle8	5,10,7,10
@@ -149,13 +149,13 @@ shuffle8	6,11,5,11
 vmovdqa		(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+224*\off+48)*2(%rsi),%ymm15
 vmovdqa		(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+224*\off+64)*2(%rsi),%ymm2
 
-mul		7,10,5,11
+mul		7, 10, 5, 11
 
 shuffle8	3,8,6,8
 shuffle8	4,9,3,9
 
 reduce
-update		4,6,8,3,9,7,10,5,11
+update		4, 6, 8, 3, 9, 7, 10, 5, 11
 
 /* level 3 */
 shuffle4	8,5,9,5
@@ -164,13 +164,13 @@ shuffle4	3,11,8,11
 vmovdqa		(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+224*\off+80)*2(%rsi),%ymm15
 vmovdqa		(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+224*\off+96)*2(%rsi),%ymm2
 
-mul		9,5,8,11
+mul		9, 5, 8, 11
 
 shuffle4	4,7,3,7
 shuffle4	6,10,4,10
 
 reduce
-update		6,3,7,4,10,9,5,8,11
+update		6, 3, 7, 4, 10, 9, 5, 8, 11
 
 /* level 4 */
 shuffle2	7,8,10,8
@@ -179,13 +179,13 @@ shuffle2	4,11,7,11
 vmovdqa		(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+224*\off+112)*2(%rsi),%ymm15
 vmovdqa		(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+224*\off+128)*2(%rsi),%ymm2
 
-mul		10,8,7,11
+mul		10, 8, 7, 11
 
 shuffle2	6,9,4,9
 shuffle2	3,5,6,5
 
 reduce
-update		3,4,9,6,5,10,8,7,11
+update		3, 4, 9, 6, 5, 10, 8, 7, 11
 
 /* level 5 */
 shuffle1	9,7,5,7
@@ -194,13 +194,13 @@ shuffle1	6,11,9,11
 vmovdqa		(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+224*\off+144)*2(%rsi),%ymm15
 vmovdqa		(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+224*\off+160)*2(%rsi),%ymm2
 
-mul		5,7,9,11
+mul		5, 7, 9, 11
 
 shuffle1	3,10,6,10
 shuffle1	4,8,3,8
 
 reduce
-update		4,6,10,3,8,5,7,9,11
+update		4, 6, 10, 3, 8, 5, 7, 9, 11
 
 /* level 6 */
 vmovdqa		(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+224*\off+176)*2(%rsi),%ymm14
@@ -208,10 +208,10 @@ vmovdqa		(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+224*\off+208)*2(%rsi),%ymm15
 vmovdqa		(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+224*\off+192)*2(%rsi),%ymm8
 vmovdqa		(MLK_AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP+224*\off+224)*2(%rsi),%ymm2
 
-mul		10,3,9,11,14,15,8,2
+mul		10, 3, 9, 11, 14, 15, 8, 2
 
 reduce
-update		8,4,6,5,7,10,3,9,11
+update		8, 4, 6, 5, 7, 10, 3, 9, 11
 
 vmovdqa		%ymm8,(128*\off+  0)*2(%rdi)
 vmovdqa		%ymm4,(128*\off+ 16)*2(%rdi)
diff --git a/dev/x86_64/src/nttfrombytes.S b/dev/x86_64/src/nttfrombytes.S
index b4e3696a74..15db0fb3e7 100644
--- a/dev/x86_64/src/nttfrombytes.S
+++ b/dev/x86_64/src/nttfrombytes.S
@@ -27,7 +27,7 @@
 #include "fq.inc"
 #include "shuffle.inc"
 
-.macro nttfrombytes_128_coefficients offset_in offset_out
+.macro nttfrombytes_128_coefficients offset_in, offset_out
 #load
 vmovdqu	(\offset_in +  0)(%rsi), %ymm4
 vmovdqu	(\offset_in + 32)(%rsi), %ymm5
@@ -102,8 +102,8 @@ movl $0x0FFF0FFF, %eax
 vmovd %eax, %xmm0
 vpbroadcastd %xmm0, %ymm0
 
-nttfrombytes_128_coefficients 0 0
-nttfrombytes_128_coefficients 192 256
+nttfrombytes_128_coefficients 0, 0
+nttfrombytes_128_coefficients 192, 256
 
 ret
 
diff --git a/dev/x86_64/src/ntttobytes.S b/dev/x86_64/src/ntttobytes.S
index b93db4569b..af244f9093 100644
--- a/dev/x86_64/src/ntttobytes.S
+++ b/dev/x86_64/src/ntttobytes.S
@@ -27,7 +27,7 @@
 #include "fq.inc"
 #include "shuffle.inc"
 
-.macro ntttobytes_128_coefficients offset_in offset_out
+.macro ntttobytes_128_coefficients offset_in, offset_out
 #load
 vmovdqa (\offset_in +   0)(%rsi), %ymm5
 vmovdqa (\offset_in +  32)(%rsi), %ymm6
@@ -97,8 +97,8 @@ movl $0x0D010D01, %eax
 vmovd %eax, %xmm0
 vpbroadcastd %xmm0, %ymm0
 
-ntttobytes_128_coefficients 0 0
-ntttobytes_128_coefficients 256 192
+ntttobytes_128_coefficients 0, 0
+ntttobytes_128_coefficients 256, 192
 
 ret
 
diff --git a/dev/x86_64/src/poly_basemul.inc b/dev/x86_64/src/poly_basemul.inc
index 2a17f94e8c..832c0d68ef 100644
--- a/dev/x86_64/src/poly_basemul.inc
+++ b/dev/x86_64/src/poly_basemul.inc
@@ -50,7 +50,7 @@
  *    r = ac + bdz = r0 + r1,
  *    s = ad + bc = s0 + s1.
  */
-.macro schoolbook iter k
+.macro schoolbook iter, k
 vmovdqa (256*\k + 32*\iter +  0)*2(%rsi), _a
 vmovdqa (256*\k + 32*\iter + 16)*2(%rsi), _b
 vmovdqa (256*\k + 32*\iter +  0)*2(%rdx), _c
@@ -114,14 +114,14 @@ vmovdqa _s0, (32*\iter + 16)*2(%rdi)
 .endm
 
 .macro poly_basemul k
-schoolbook 0 \k
-schoolbook 1 \k
-schoolbook 2 \k
-schoolbook 3 \k
-schoolbook 4 \k
-schoolbook 5 \k
-schoolbook 6 \k
-schoolbook 7 \k
+schoolbook 0, \k
+schoolbook 1, \k
+schoolbook 2, \k
+schoolbook 3, \k
+schoolbook 4, \k
+schoolbook 5, \k
+schoolbook 6, \k
+schoolbook 7, \k
 .endm
 
 .macro polyvec_basemul k
diff --git a/dev/x86_64/src/shuffle.inc b/dev/x86_64/src/shuffle.inc
index c03a82bdb5..9f732b4a67 100644
--- a/dev/x86_64/src/shuffle.inc
+++ b/dev/x86_64/src/shuffle.inc
@@ -8,12 +8,12 @@
  * AVX2 Kyber implementation @[REF_AVX2].
  */
 
-.macro shuffle8 r0,r1,r2,r3
+.macro shuffle8 r0, r1, r2, r3
 vperm2i128	$0x20,%ymm\r1,%ymm\r0,%ymm\r2
 vperm2i128	$0x31,%ymm\r1,%ymm\r0,%ymm\r3
 .endm
 
-.macro shuffle4 r0,r1,r2,r3
+.macro shuffle4 r0, r1, r2, r3
 vpunpcklqdq	%ymm\r1,%ymm\r0,%ymm\r2
 vpunpckhqdq	%ymm\r1,%ymm\r0,%ymm\r3
 .endm
@@ -21,7 +21,7 @@ vpunpckhqdq	%ymm\r1,%ymm\r0,%ymm\r3
 /* Shuffle r0=(a0,b0,c0,d0,...), r1=(a1,b1,c1,d1,...) into */
 /* r2 = (a0,b0,a1,b1,e0,f0,e1,f1,...) */
 /* r3 = (c0,d0,c1,d1,g0,h0,g1,h1,...) */
-.macro shuffle2 r0,r1,r2,r3
+.macro shuffle2 r0, r1, r2, r3
 /* r2=(a1,b1,a1,b1,e1,f1,e1,f1,...) */
 vmovsldup	%ymm\r1,%ymm\r2
 /* Conditional move */
@@ -34,7 +34,7 @@ vpsrlq		$32,%ymm\r0,%ymm\r0
 vpblendd	$0xAA,%ymm\r1,%ymm\r0,%ymm\r3
 .endm
 
-.macro shuffle1 r0,r1,r2,r3
+.macro shuffle1 r0, r1, r2, r3
 vpslld		$16,%ymm\r1,%ymm\r2
 vpblendw	$0xAA,%ymm\r2,%ymm\r0,%ymm\r2
 vpsrld		$16,%ymm\r0,%ymm\r0
diff --git a/flake.nix b/flake.nix
index f7bb2975f8..2148c91d68 100644
--- a/flake.nix
+++ b/flake.nix
@@ -117,6 +117,15 @@
           devShells.ci-slothy = util.mkShell {
             packages = builtins.attrValues { inherit (config.packages) slothy linters toolchains_native; };
           };
+          devShells.hol_light-cross = util.mkShell {
+            packages = builtins.attrValues { inherit (config.packages) linters toolchains hol_light s2n_bignum; };
+          };
+          devShells.hol_light-cross-aarch64 = util.mkShell {
+            packages = builtins.attrValues { inherit (config.packages) linters toolchain_aarch64 hol_light s2n_bignum; };
+          };
+          devShells.hol_light-cross-x86_64 = util.mkShell {
+            packages = builtins.attrValues { inherit (config.packages) linters toolchain_x86_64 hol_light s2n_bignum; };
+          };
           devShells.ci-cross = util.mkShell {
             packages = builtins.attrValues { inherit (config.packages) linters toolchains; };
           };
diff --git a/mlkem/src/native/x86_64/src/fq.inc b/mlkem/src/native/x86_64/src/fq.inc
index 647011e208..86202f5b2c 100644
--- a/mlkem/src/native/x86_64/src/fq.inc
+++ b/mlkem/src/native/x86_64/src/fq.inc
@@ -8,7 +8,7 @@
  * AVX2 Kyber implementation @[REF_AVX2].
  */
 
-.macro red16 r,rs=0,x=12
+.macro red16 r, rs=0, x=12
 vpmulhw         %ymm1,%ymm\r,%ymm\x
 .if \rs
 vpmulhrsw	%ymm\rs,%ymm\x,%ymm\x
@@ -19,14 +19,14 @@ vpmullw         %ymm0,%ymm\x,%ymm\x
 vpsubw          %ymm\x,%ymm\r,%ymm\r
 .endm
 
-.macro csubq r,x=12
+.macro csubq r, x=12
 vpsubw		%ymm0,%ymm\r,%ymm\r
 vpsraw		$15,%ymm\r,%ymm\x
 vpand		%ymm0,%ymm\x,%ymm\x
 vpaddw		%ymm\x,%ymm\r,%ymm\r
 .endm
 
-.macro caddq r,x=12
+.macro caddq r, x=12
 vpsraw		$15,%ymm\r,%ymm\x
 vpand		%ymm0,%ymm\x,%ymm\x
 vpaddw		%ymm\x,%ymm\r,%ymm\r
@@ -34,7 +34,7 @@ vpaddw		%ymm\x,%ymm\r,%ymm\r
 
 /* Montgomery multiplication between b and ah,
  * with Montgomery twist of ah in al. */
-.macro fqmulprecomp al,ah,b,x=12
+.macro fqmulprecomp al, ah, b, x=12
 vpmullw		%ymm\al,%ymm\b,%ymm\x
 vpmulhw		%ymm\ah,%ymm\b,%ymm\b
 vpmulhw		%ymm0,%ymm\x,%ymm\x
diff --git a/mlkem/src/native/x86_64/src/poly_basemul.inc b/mlkem/src/native/x86_64/src/poly_basemul.inc
index 2a17f94e8c..832c0d68ef 100644
--- a/mlkem/src/native/x86_64/src/poly_basemul.inc
+++ b/mlkem/src/native/x86_64/src/poly_basemul.inc
@@ -50,7 +50,7 @@
  *    r = ac + bdz = r0 + r1,
  *    s = ad + bc = s0 + s1.
  */
-.macro schoolbook iter k
+.macro schoolbook iter, k
 vmovdqa (256*\k + 32*\iter +  0)*2(%rsi), _a
 vmovdqa (256*\k + 32*\iter + 16)*2(%rsi), _b
 vmovdqa (256*\k + 32*\iter +  0)*2(%rdx), _c
@@ -114,14 +114,14 @@ vmovdqa _s0, (32*\iter + 16)*2(%rdi)
 .endm
 
 .macro poly_basemul k
-schoolbook 0 \k
-schoolbook 1 \k
-schoolbook 2 \k
-schoolbook 3 \k
-schoolbook 4 \k
-schoolbook 5 \k
-schoolbook 6 \k
-schoolbook 7 \k
+schoolbook 0, \k
+schoolbook 1, \k
+schoolbook 2, \k
+schoolbook 3, \k
+schoolbook 4, \k
+schoolbook 5, \k
+schoolbook 6, \k
+schoolbook 7, \k
 .endm
 
 .macro polyvec_basemul k
diff --git a/mlkem/src/native/x86_64/src/shuffle.inc b/mlkem/src/native/x86_64/src/shuffle.inc
index c03a82bdb5..9f732b4a67 100644
--- a/mlkem/src/native/x86_64/src/shuffle.inc
+++ b/mlkem/src/native/x86_64/src/shuffle.inc
@@ -8,12 +8,12 @@
  * AVX2 Kyber implementation @[REF_AVX2].
  */
 
-.macro shuffle8 r0,r1,r2,r3
+.macro shuffle8 r0, r1, r2, r3
 vperm2i128	$0x20,%ymm\r1,%ymm\r0,%ymm\r2
 vperm2i128	$0x31,%ymm\r1,%ymm\r0,%ymm\r3
 .endm
 
-.macro shuffle4 r0,r1,r2,r3
+.macro shuffle4 r0, r1, r2, r3
 vpunpcklqdq	%ymm\r1,%ymm\r0,%ymm\r2
 vpunpckhqdq	%ymm\r1,%ymm\r0,%ymm\r3
 .endm
@@ -21,7 +21,7 @@ vpunpckhqdq	%ymm\r1,%ymm\r0,%ymm\r3
 /* Shuffle r0=(a0,b0,c0,d0,...), r1=(a1,b1,c1,d1,...) into */
 /* r2 = (a0,b0,a1,b1,e0,f0,e1,f1,...) */
 /* r3 = (c0,d0,c1,d1,g0,h0,g1,h1,...) */
-.macro shuffle2 r0,r1,r2,r3
+.macro shuffle2 r0, r1, r2, r3
 /* r2=(a1,b1,a1,b1,e1,f1,e1,f1,...) */
 vmovsldup	%ymm\r1,%ymm\r2
 /* Conditional move */
@@ -34,7 +34,7 @@ vpsrlq		$32,%ymm\r0,%ymm\r0
 vpblendd	$0xAA,%ymm\r1,%ymm\r0,%ymm\r3
 .endm
 
-.macro shuffle1 r0,r1,r2,r3
+.macro shuffle1 r0, r1, r2, r3
 vpslld		$16,%ymm\r1,%ymm\r2
 vpblendw	$0xAA,%ymm\r2,%ymm\r0,%ymm\r2
 vpsrld		$16,%ymm\r0,%ymm\r0
diff --git a/proofs/hol_light/arm/Makefile b/proofs/hol_light/arm/Makefile
index e43d435921..4010796209 100644
--- a/proofs/hol_light/arm/Makefile
+++ b/proofs/hol_light/arm/Makefile
@@ -19,6 +19,28 @@ ARCHTYPE_RESULT=$(shell uname -m)
 SRC ?= $(S2N_BIGNUM_DIR)
 SRC_ARM ?= $(SRC)/arm
 
+ARCHFLAGS=-march=armv8.4-a+sha3
+
+# If actually on an AArch64 machine, just use the assembler (as). Otherwise
+# use a cross-assembling version so that the code can still be assembled
+# and the proofs checked against the object files (though you won't be able
+# to run code without additional emulation infrastructure).
+
+ifeq ($(ARCHTYPE_RESULT)-$(OSTYPE_RESULT),x86_64-Darwin)
+ASSEMBLE=as -arch arm64
+OBJDUMP=otool -tvV
+else
+ifeq ($(filter $(ARCHTYPE_RESULT),aarch64 arm64),)
+CROSS_PREFIX=aarch64-unknown-linux-gnu-
+# Check if cross-toolchain exists
+ifeq ($(shell command -v $(ASSEMBLE) >/dev/null 2>&1 && echo yes || echo no),no)
+$(error Cross-toolchain not found. Please run in the 'hol_light' nix shell via: nix develop .#hol_light)
+endif
+endif
+ASSEMBLE=$(CROSS_PREFIX)as $(ARCHFLAGS)
+OBJDUMP=$(CROSS_PREFIX)objdump -d
+endif
+
 # Add explicit language input parameter to cpp, otherwise the use of #n for
 # numeric literals in ARM code is a problem when used inside #define macros
 # since normally that means stringization.
@@ -26,11 +48,10 @@ SRC_ARM ?= $(SRC)/arm
 # Some clang-based preprocessors seem to behave differently, and get confused
 # by single-quote characters in comments, so we eliminate // comments first.
 
-ARCHFLAGS=-march=armv8.4-a+sha3
 ifeq ($(OSTYPE_RESULT),Darwin)
 PREPROCESS=sed -e 's/\/\/.*//' | $(CC) -E -xassembler-with-cpp -
 else
-PREPROCESS=$(CC) $(ARCHFLAGS) -E -xassembler-with-cpp -
+PREPROCESS=$(CC) -E -xassembler-with-cpp -
 endif
 
 # Generally GNU-type assemblers are happy with multiple instructions on
@@ -38,34 +59,6 @@ endif
 
 SPLIT=tr ';' '\n'
 
-# If actually on an ARM8 machine, just use the assembler (as). Otherwise
-# use a cross-assembling version so that the code can still be assembled
-# and the proofs checked against the object files (though you won't be able
-# to run code without additional emulation infrastructure). For the clang
-# version on OS X we just add the "-arch arm64" option. For the Linux/gcc
-# toolchain we assume the presence of the special cross-assembler. This
-# can be installed via something like:
-#
-#  sudo apt-get install binutils-aarch64-linux-gnu
-
-ifeq ($(ARCHTYPE_RESULT),aarch64)
-ASSEMBLE=as $(ARCHFLAGS)
-OBJDUMP=objdump -d
-else
-ifeq ($(ARCHTYPE_RESULT),arm64)
-ASSEMBLE=as $(ARCHFLAGS)
-OBJDUMP=objdump -d
-else
-ifeq ($(OSTYPE_RESULT),Darwin)
-ASSEMBLE=as -arch arm64
-OBJDUMP=otool -tvV
-else
-ASSEMBLE=aarch64-linux-gnu-as $(ARCHFLAGS)
-OBJDUMP=aarch64-linux-gnu-objdump -d
-endif
-endif
-endif
-
 OBJ = mlkem/mlkem_ntt.o                                   \
       mlkem/mlkem_intt.o                                  \
       mlkem/mlkem_poly_tomont.o                           \
diff --git a/scripts/autogen b/scripts/autogen
index 9bccd3f865..a8ca662a9e 100755
--- a/scripts/autogen
+++ b/scripts/autogen
@@ -32,6 +32,10 @@ _RE_LABEL = re.compile(r"^(\w+):")
 _RE_CONFIG_NAME = re.compile(r"\* Name:\s+(\w+)")
 _RE_MACRO_CHECK = re.compile(r"[^_]((?:MLK_|MLKEM_)\w+)(.*)$", re.M)
 _RE_DEFINE = re.compile(r"^\s*#define\s+(\w+)")
+_RE_ARGS_COMMENT = re.compile(r"(.*?)(\s*//.*)?$")
+_RE_MACRO_DEF = re.compile(r"^\s*\.macro\s+(\w+)")
+_RE_MACRO_DEF_ARGS = re.compile(r"^(\s*\.macro\s+\w+)(\s+.*)$")
+_RE_LEADING_SPACE = re.compile(r"^(\s*)")
 
 # File cache: {filename: {"content": str, "original": str, "force_format": bool}}
 # Caches content of files in preparation/modification to avoid repeated
@@ -2050,6 +2054,85 @@ def check_asm_loop_labels():
         results = list(executor.map(check_asm_loop_labels_for_file, files))
 
 
+def normalize_comma_separated_args(args_str):
+    """Convert whitespace-separated args to comma-separated, add spaces after commas"""
+    # Extract and preserve comment
+    match = _RE_ARGS_COMMENT.match(args_str)
+    args_only = match.group(1).rstrip()
+    comment = match.group(2) or ""
+
+    # If already has commas, just normalize spacing
+    if "," in args_only:
+        result = re.sub(r",(?! )", ", ", args_only)
+    else:
+        # Split on whitespace and join with commas
+        args = args_only.split()
+        if not args:
+            return args_str
+        result = ", ".join(args)
+
+    return result + comment
+
+
+def normalize_asm_macro_syntax_for_file(filename):
+    """Normalize macro definitions and invocations to use commas with spaces"""
+    status_update("asm-macro-syntax", filename)
+
+    content = read_file(filename)
+    lines = content.split("\n")
+
+    # First pass: collect macro names
+    macro_names = set()
+    for line in lines:
+        macro_match = _RE_MACRO_DEF.match(line)
+        if macro_match:
+            macro_names.add(macro_match.group(1))
+
+    # Second pass: normalize syntax
+    modified = False
+    new_lines = []
+    for line in lines:
+        # Normalize .macro definitions
+        macro_def_match = _RE_MACRO_DEF_ARGS.match(line)
+        if macro_def_match:
+            prefix = macro_def_match.group(1)
+            args_with_space = macro_def_match.group(2)
+            # Preserve leading whitespace, normalize the rest
+            leading_space = _RE_LEADING_SPACE.match(args_with_space).group(1)
+            args = args_with_space.lstrip()
+            normalized_args = normalize_comma_separated_args(args)
+            line = prefix + leading_space + normalized_args
+        else:
+            # Normalize macro invocations
+            for macro_name in macro_names:
+                # Match: whitespace + macro_name + whitespace + args
+                pattern = r"^(\s*" + re.escape(macro_name) + r")(\s+.*)$"
+                invocation_match = re.match(pattern, line)
+                if not invocation_match:
+                    continue
+                prefix = invocation_match.group(1)
+                args_with_space = invocation_match.group(2)
+                # Preserve leading whitespace, normalize the rest
+                leading_space = _RE_LEADING_SPACE.match(args_with_space).group(1)
+                args = args_with_space.lstrip()
+                normalized_args = normalize_comma_separated_args(args)
+                line = prefix + leading_space + normalized_args
+                break
+
+        new_lines.append(line)
+
+    update_file(filename, "\n".join(new_lines))
+
+
+def normalize_asm_macro_syntax():
+    """Normalize macro syntax in all assembly files"""
+    # Operate on assembly files in dev/ only. The ones in mlkem/ are autogenerated.
+    files = list(filter(lambda s: s.startswith("dev/"), get_asm_source_files()))
+    files += list(filter(lambda s: s.endswith(".inc"), get_files("dev/**/*.inc")))
+    with ThreadPoolExecutor() as executor:
+        results = list(executor.map(normalize_asm_macro_syntax_for_file, files))
+
+
 def update_via_simpasm(
     infile_full,
     outdir,
@@ -2116,17 +2199,19 @@ def update_via_simpasm(
             # Add syntax option for x86_64
             if arch == "x86_64" and x86_64_syntax != "att":
                 cmd += ["--syntax", x86_64_syntax]
+            cmd += ["-v"]
             r = subprocess.run(
                 cmd,
-                stdout=subprocess.DEVNULL,
-                stderr=subprocess.PIPE,
+                stdout=subprocess.PIPE,
+                stderr=subprocess.STDOUT,
                 check=True,
                 text=True,
             )
+            print(r.stdout)
         except subprocess.CalledProcessError as e:
             print(f"Command failed: {' '.join(cmd)}")
             print(f"Exit code: {e.returncode}")
-            print(f"stderr: {e.stderr}")
+            print(f"stdout/stderr: {e.stdout}")
             raise Exception("Failed to run simpasm") from e
         tmp.seek(0)
         new_contents = tmp.read().decode()
@@ -3214,6 +3299,8 @@ def _main():
     high_level_status("Checked assembly register aliases")
     check_asm_loop_labels()
     high_level_status("Checked assembly loop labels")
+    normalize_asm_macro_syntax()
+    high_level_status("Normalize assembly macro syntax")
 
     gen_c_zeta_file()
     gen_aarch64_hol_light_zeta_file()
diff --git a/scripts/simpasm b/scripts/simpasm
index 6ef3e37cb3..1b9bf0dd9b 100755
--- a/scripts/simpasm
+++ b/scripts/simpasm
@@ -246,7 +246,7 @@ def simplify(logger, args, asm_input, asm_output=None):
             logger.debug(f"Using raw global symbol {sym} going forward ...")
 
         cmd = [args.objdump, "--disassemble", tmp_objfile0]
-        if platform.system() == "Darwin":
+        if platform.system() == "Darwin" and args.arch == "aarch64":
             cmd += ["--triple=aarch64"]
 
         # Add syntax option if specified
@@ -256,6 +256,8 @@ def simplify(logger, args, asm_input, asm_output=None):
         logger.debug(f"Disassembling temporary object file {tmp_objfile0} ...")
         disasm = run_cmd(cmd).stdout
 
+        print(disasm)
+
         logger.debug("Patching up disassembly ...")
         simplified = patchup_disasm(disasm, cfify=args.cfify)