diff --git a/.github/workflows/base.yml b/.github/workflows/base.yml
new file mode 100644
index 000000000..caf1ee04f
--- /dev/null
+++ b/.github/workflows/base.yml
@@ -0,0 +1,236 @@
+# SPDX-License-Identifier: Apache-2.0
+
+name: Base tests
+permissions:
+  contents: read
+on:
+  workflow_dispatch:
+  push:
+    branches: ["main"]
+  pull_request:
+    branches: ["main"]
+    types: [ "opened", "synchronize" ]
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  lint:
+    strategy:
+      fail-fast: false
+      matrix:
+        system: [ubuntu-latest, pqcp-arm64]
+    name: Linting
+    runs-on: ${{ matrix.system }}
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      - uses: ./.github/actions/lint
+        with:
+          nix-shell: ci-linter
+          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          cross-prefix: "aarch64-unknown-linux-gnu-"
+  lint-markdown-link:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+    - uses: gaurav-nelson/github-action-markdown-link-check@1b916f2cf6c36510a6059943104e3c42ce6c16bc # v1.0.16
+  quickcheck:
+    strategy:
+      fail-fast: false
+      matrix:
+        external:
+         - ${{ github.repository_owner != 'pq-code-package' }}
+        target:
+         - runner: pqcp-arm64
+           name: 'aarch64'
+         - runner: ubuntu-latest
+           name: 'x86_64'
+         - runner: macos-latest
+           name: 'macos (aarch64)'
+         - runner: macos-13
+           name: 'macos (x86_64)'
+        exclude:
+          - {external: true,
+             target: {
+               runner: pqcp-arm64,
+               name: 'aarch64'
+             }}
+    name: Quickcheck (${{ matrix.target.name }})
+    runs-on: ${{ matrix.target.runner }}
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      - name: make quickcheck
+        run: |
+          OPT=0 make quickcheck
+          make clean >/dev/null
+          OPT=1 make quickcheck
+      - uses: ./.github/actions/setup-os
+      - name: tests func
+        run: |
+          ./scripts/tests func
+      - name: tests bench
+        run: |
+          ./scripts/tests bench -c NO
+      - name: tests bench components
+        run: |
+          ./scripts/tests bench --components -c NO
+      - name: check namespacing
+        run: |
+          ./scripts/check-namespace
+  quickcheck-c90:
+    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: Quickcheck C90 (${{ matrix.target.name }})
+    runs-on: ${{ matrix.target.runner }}
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      - name: make quickcheck
+        run: |
+          OPT=0 CFLAGS=-std=c90 make quickcheck
+          make clean >/dev/null
+          OPT=1 CFLAGS=-std=c90 make quickcheck
+      - uses: ./.github/actions/setup-apt
+      - name: tests func
+        run: |
+          ./scripts/tests func --cflags="-std=c90"
+      - name: tests bench
+        run: |
+          ./scripts/tests bench -c NO --cflags="-std=c90"
+      - name: tests bench components
+        run: |
+          ./scripts/tests bench --components -c NO --cflags="-std=c90"
+      - name: check namespacing
+        run: |
+          ./scripts/check-namespace
+  quickcheck-windows:
+    strategy:
+      fail-fast: false
+      matrix:
+        system: [windows-latest, windows-2022, windows-2019]
+    name: Quickcheck ${{ matrix.system }}
+    runs-on: ${{ matrix.system }}
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      - uses: ilammy/msvc-dev-cmd@0b201ec74fa43914dc39ae48a89fd1d8cb592756 # v1.13.0
+      - name: Build test
+        shell: powershell
+        run: |
+          # print compiler version
+          cl
+          nmake /f ./Makefile.Microsoft_nmake quickcheck
+  quickcheck-windows-mingw-w64:
+    strategy:
+      fail-fast: false
+      matrix:
+        mingw-version: [5.4.0, 11.2.0, 12.2.0, 13.2.0]
+    name: Quickcheck (Mingw-w64 ${{ matrix.mingw-version }})
+    runs-on: windows-latest
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      - name: Install MinGW-w64
+        run: choco install mingw --version=${{ matrix.mingw-version }} -y
+        shell: cmd
+      - name: make quickcheck
+        shell: bash
+        run: |
+          CC=gcc OPT=0 make quickcheck
+          CC=gcc make clean >/dev/null
+          CC=gcc OPT=1 make quickcheck
+  quickcheck-lib:
+    name: Quickcheck lib
+    strategy:
+      matrix:
+        system: [macos-latest, macos-13, ubuntu-latest, pqcp-arm64]
+    runs-on: ${{ matrix.system }}
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      - name: make lib
+        run: |
+          make lib
+  examples:
+    name: Examples
+    strategy:
+      matrix:
+        system: [macos-latest, macos-13, ubuntu-latest, pqcp-arm64]
+    runs-on: ${{ matrix.system }}
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      - name: mlkem_native_as_code_package
+        run: |
+          CFLAGS="-O0" make run -C examples/mlkem_native_as_code_package
+      - name: bring_your_own_fips202
+        run: |
+          CFLAGS="-O0" make run -C examples/bring_your_own_fips202
+      - name: custom_backend
+        run: |
+          CFLAGS="-O0" make run -C examples/custom_backend
+      - name: monolithic_build
+        run: |
+          CFLAGS="-O0" make run -C examples/monolithic_build
+      - name: monolithic_build_multilevel
+        run: |
+          CFLAGS="-O0" make run -C examples/monolithic_build_multilevel
+      - name: multilevel_build
+        run: |
+          CFLAGS="-O0" make run -C examples/multilevel_build
+      - name: multilevel_build_native
+        run: |
+          CFLAGS="-O0" make run -C examples/multilevel_build_native
+  check_autogenerated_files:
+    strategy:
+      fail-fast: false
+      matrix:
+        system: [ubuntu-latest, pqcp-arm64]
+    runs-on: ${{ matrix.system }}
+    name: Check autogenerated files
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      - uses: ./.github/actions/setup-shell
+        with:
+          nix-shell: 'ci-cross' # Need cross-compiler for ASM simplification
+          nix-cache: 'true'
+          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          script: |
+            python3 ./scripts/autogen --dry-run --force-cross
+  simpasm:
+    strategy:
+      fail-fast: false
+      matrix:
+        backend:
+           - arg: '--aarch64-clean'
+             name: Clean
+           - arg: ''
+             name: Optimized
+        simplify:
+           - arg: ''
+             name: Simplified
+           - arg: '--no-simplify'
+             name: Unmodified
+    runs-on: pqcp-arm64
+    name: AArch64 dev backend (${{ matrix.backend.name }}, ${{ matrix.simplify.name }})
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      - name: Reinstate and test backend
+        uses: ./.github/actions/setup-shell
+        with:
+          nix-shell: 'ci'
+          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          script: |
+            ./scripts/autogen ${{ matrix.backend.arg }} ${{ matrix.simplify.arg }}
+            make clean
+            OPT=1 make quickcheck
diff --git a/.github/workflows/cbmc.yml b/.github/workflows/cbmc.yml
new file mode 100644
index 000000000..4d40b9dd8
--- /dev/null
+++ b/.github/workflows/cbmc.yml
@@ -0,0 +1,87 @@
+# SPDX-License-Identifier: Apache-2.0
+
+name: CBMC
+permissions:
+  contents: read
+on:
+  workflow_dispatch:
+  push:
+    branches: ["main"]
+  pull_request:
+    branches: ["main"]
+    types: [ "opened", "synchronize" ]
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  cbmc_k2:
+    name: CBMC (ML-KEM-512)
+    if: ${{ github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork }}
+    permissions:
+      contents: 'read'
+      id-token: 'write'
+    uses: ./.github/workflows/ci_ec2_reusable.yml
+    with:
+      name: CBMC (MLKEM-512)
+      ec2_instance_type: c7g.2xlarge
+      ec2_ami: ubuntu-latest (custom AMI)
+      ec2_ami_id: ami-08ddb0acd99dc3d33 # aarch64, ubuntu-latest, 64g
+      compile_mode: native
+      opt: no_opt
+      lint: false
+      verbose: true
+      functest: true
+      kattest: false
+      nistkattest: false
+      acvptest: false
+      cbmc: true
+      cbmc_mlkem_k: 2
+    secrets: inherit
+  cbmc_k3:
+    name: CBMC (ML-KEM-768)
+    if: ${{ github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork }}
+    permissions:
+      contents: 'read'
+      id-token: 'write'
+    uses: ./.github/workflows/ci_ec2_reusable.yml
+    with:
+      name: CBMC (MLKEM-768)
+      ec2_instance_type: c7g.2xlarge
+      ec2_ami: ubuntu-latest (custom AMI)
+      ec2_ami_id: ami-08ddb0acd99dc3d33 # aarch64, ubuntu-latest, 64g
+      compile_mode: native
+      opt: no_opt
+      lint: false
+      verbose: true
+      functest: true
+      kattest: false
+      nistkattest: false
+      acvptest: false
+      cbmc: true
+      cbmc_mlkem_k: 3
+    secrets: inherit
+  cbmc_k4:
+    name: CBMC (ML-KEM-1024)
+    if: ${{ github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork }}
+    permissions:
+      contents: 'read'
+      id-token: 'write'
+    uses: ./.github/workflows/ci_ec2_reusable.yml
+    with:
+      name: CBMC (MLKEM-1024)
+      ec2_instance_type: c7g.2xlarge
+      ec2_ami: ubuntu-latest (custom AMI)
+      ec2_ami_id: ami-08ddb0acd99dc3d33 # aarch64, ubuntu-latest, 64g
+      compile_mode: native
+      opt: no_opt
+      lint: false
+      verbose: true
+      functest: true
+      kattest: false
+      nistkattest: false
+      acvptest: false
+      cbmc: true
+      cbmc_mlkem_k: 4
+    secrets: inherit
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index b0b03a93b..b337760c1 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -1,6 +1,6 @@
 # SPDX-License-Identifier: Apache-2.0
 
-name: CI
+name: Extended tests
 permissions:
   contents: read
 on:
@@ -16,227 +16,7 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-  lint:
-    strategy:
-      fail-fast: false
-      matrix:
-        system: [ubuntu-latest, pqcp-arm64]
-    name: Linting
-    runs-on: ${{ matrix.system }}
-    steps:
-      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-      - uses: ./.github/actions/lint
-        with:
-          nix-shell: ci-linter
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          cross-prefix: "aarch64-unknown-linux-gnu-"
-  lint-markdown-link:
-    runs-on: ubuntu-latest
-    steps:
-    - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-    - uses: gaurav-nelson/github-action-markdown-link-check@1b916f2cf6c36510a6059943104e3c42ce6c16bc # v1.0.16
-  quickcheck:
-    strategy:
-      fail-fast: false
-      matrix:
-        external:
-         - ${{ github.repository_owner != 'pq-code-package' }}
-        target:
-         - runner: pqcp-arm64
-           name: 'aarch64'
-         - runner: ubuntu-latest
-           name: 'x86_64'
-         - runner: macos-latest
-           name: 'macos (aarch64)'
-         - runner: macos-13
-           name: 'macos (x86_64)'
-        exclude:
-          - {external: true,
-             target: {
-               runner: pqcp-arm64,
-               name: 'aarch64'
-             }}
-    name: Quickcheck (${{ matrix.target.name }})
-    runs-on: ${{ matrix.target.runner }}
-    steps:
-      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-      - name: make quickcheck
-        run: |
-          OPT=0 make quickcheck
-          make clean >/dev/null
-          OPT=1 make quickcheck
-      - uses: ./.github/actions/setup-os
-      - name: tests func
-        run: |
-          ./scripts/tests func
-      - name: tests bench
-        run: |
-          ./scripts/tests bench -c NO
-      - name: tests bench components
-        run: |
-          ./scripts/tests bench --components -c NO
-      - name: check namespacing
-        run: |
-          ./scripts/check-namespace
-  quickcheck-c90:
-    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: Quickcheck C90 (${{ matrix.target.name }})
-    runs-on: ${{ matrix.target.runner }}
-    steps:
-      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-      - name: make quickcheck
-        run: |
-          OPT=0 CFLAGS=-std=c90 make quickcheck
-          make clean >/dev/null
-          OPT=1 CFLAGS=-std=c90 make quickcheck
-      - uses: ./.github/actions/setup-apt
-      - name: tests func
-        run: |
-          ./scripts/tests func --cflags="-std=c90"
-      - name: tests bench
-        run: |
-          ./scripts/tests bench -c NO --cflags="-std=c90"
-      - name: tests bench components
-        run: |
-          ./scripts/tests bench --components -c NO --cflags="-std=c90"
-      - name: check namespacing
-        run: |
-          ./scripts/check-namespace
-  quickcheck-windows:
-    strategy:
-      fail-fast: false
-      matrix:
-        system: [windows-latest, windows-2022, windows-2019]
-    name: Quickcheck ${{ matrix.system }}
-    runs-on: ${{ matrix.system }}
-    steps:
-      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-      - uses: ilammy/msvc-dev-cmd@0b201ec74fa43914dc39ae48a89fd1d8cb592756 # v1.13.0
-      - name: Build test
-        shell: powershell
-        run: |
-          # print compiler version
-          cl
-          nmake /f ./Makefile.Microsoft_nmake quickcheck
-  quickcheck-windows-mingw-w64:
-    strategy:
-      fail-fast: false
-      matrix:
-        mingw-version: [5.4.0, 11.2.0, 12.2.0, 13.2.0]
-    name: Quickcheck (Mingw-w64 ${{ matrix.mingw-version }})
-    runs-on: windows-latest
-    steps:
-      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-      - name: Install MinGW-w64
-        run: choco install mingw --version=${{ matrix.mingw-version }} -y
-        shell: cmd
-      - name: make quickcheck
-        shell: bash
-        run: |
-          CC=gcc OPT=0 make quickcheck
-          CC=gcc make clean >/dev/null
-          CC=gcc OPT=1 make quickcheck
-  quickcheck-lib:
-    name: Quickcheck lib
-    strategy:
-      matrix:
-        system: [macos-latest, macos-13, ubuntu-latest, pqcp-arm64]
-    runs-on: ${{ matrix.system }}
-    steps:
-      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-      - name: make lib
-        run: |
-          make lib
-  examples:
-    name: Examples
-    strategy:
-      matrix:
-        system: [macos-latest, macos-13, ubuntu-latest, pqcp-arm64]
-    runs-on: ${{ matrix.system }}
-    steps:
-      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-      - name: mlkem_native_as_code_package
-        run: |
-          CFLAGS="-O0" make run -C examples/mlkem_native_as_code_package
-      - name: bring_your_own_fips202
-        run: |
-          CFLAGS="-O0" make run -C examples/bring_your_own_fips202
-      - name: custom_backend
-        run: |
-          CFLAGS="-O0" make run -C examples/custom_backend
-      - name: monolithic_build
-        run: |
-          CFLAGS="-O0" make run -C examples/monolithic_build
-      - name: monolithic_build_multilevel
-        run: |
-          CFLAGS="-O0" make run -C examples/monolithic_build_multilevel
-      - name: multilevel_build
-        run: |
-          CFLAGS="-O0" make run -C examples/multilevel_build
-      - name: multilevel_build_native
-        run: |
-          CFLAGS="-O0" make run -C examples/multilevel_build_native
-  check_autogenerated_files:
-    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint]
-    strategy:
-      fail-fast: false
-      matrix:
-        system: [ubuntu-latest, pqcp-arm64]
-    runs-on: ${{ matrix.system }}
-    name: Check autogenerated files
-    steps:
-      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-      - uses: ./.github/actions/setup-shell
-        with:
-          nix-shell: 'ci-cross' # Need cross-compiler for ASM simplification
-          nix-cache: 'true'
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          script: |
-            python3 ./scripts/autogen --dry-run --force-cross
-  simpasm:
-    strategy:
-      fail-fast: false
-      matrix:
-        backend:
-           - arg: '--aarch64-clean'
-             name: Clean
-           - arg: ''
-             name: Optimized
-        simplify:
-           - arg: ''
-             name: Simplified
-           - arg: '--no-simplify'
-             name: Unmodified
-    runs-on: pqcp-arm64
-    name: AArch64 dev backend (${{ matrix.backend.name }}, ${{ matrix.simplify.name }})
-    steps:
-      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-      - name: Reinstate and test backend
-        uses: ./.github/actions/setup-shell
-        with:
-          nix-shell: 'ci'
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
-          script: |
-            ./scripts/autogen ${{ matrix.backend.arg }} ${{ matrix.simplify.arg }}
-            make clean
-            OPT=1 make quickcheck
   build_kat:
-    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint]
     strategy:
       fail-fast: false
       matrix:
@@ -340,7 +120,6 @@ jobs:
           cflags: "-DMLKEM_DEBUG -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all"
   compiler_tests:
     name: Compiler tests  (${{ matrix.compiler.name }}, ${{ matrix.target.name }})
-    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint]
     strategy:
       fail-fast: false
       matrix:
@@ -444,7 +223,6 @@ jobs:
           cflags: "-std=c17"
   config_variations:
     name: Non-standard configurations
-    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint]
     strategy:
       fail-fast: false
       matrix:
@@ -546,7 +324,6 @@ jobs:
           acvp: false
   check-cf-protections:
     name: Test control-flow protections  (${{ matrix.compiler.name }}, x86_64)
-    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples]
     strategy:
       fail-fast: false
       matrix:
@@ -634,7 +411,6 @@ jobs:
     permissions:
       contents: 'read'
       id-token: 'write'
-    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint]
     if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
     uses: ./.github/workflows/ci_ec2_reusable.yml
     with:
@@ -661,7 +437,6 @@ jobs:
           - id: debian:bookworm
     name: Compatibility tests (${{ matrix.container.id }})
     runs-on: ubuntu-latest
-    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint]
     container:
       ${{ matrix.container.id }}
     steps:
@@ -724,7 +499,6 @@ jobs:
           - id: ubuntu-22.04-aarch:base
           - id: ubuntu-20.04-aarch:base
     name: Compatibility tests (${{ matrix.container.id }})
-    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint]
     permissions:
       contents: 'read'
       id-token: 'write'
@@ -746,75 +520,3 @@ jobs:
       verbose: true
       cflags: "-O0"
     secrets: inherit
-  cbmc_k2:
-    name: CBMC (ML-KEM-512)
-    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint]
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    uses: ./.github/workflows/ci_ec2_reusable.yml
-    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
-    with:
-      name: CBMC (MLKEM-512)
-      ec2_instance_type: c7g.2xlarge
-      ec2_ami: ubuntu-latest (custom AMI)
-      ec2_ami_id: ami-08ddb0acd99dc3d33 # aarch64, ubuntu-latest, 64g
-      compile_mode: native
-      opt: no_opt
-      lint: false
-      verbose: true
-      functest: true
-      kattest: false
-      nistkattest: false
-      acvptest: false
-      cbmc: true
-      cbmc_mlkem_k: 2
-    secrets: inherit
-  cbmc_k3:
-    name: CBMC (ML-KEM-768)
-    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint]
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    uses: ./.github/workflows/ci_ec2_reusable.yml
-    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
-    with:
-      name: CBMC (MLKEM-768)
-      ec2_instance_type: c7g.2xlarge
-      ec2_ami: ubuntu-latest (custom AMI)
-      ec2_ami_id: ami-08ddb0acd99dc3d33 # aarch64, ubuntu-latest, 64g
-      compile_mode: native
-      opt: no_opt
-      lint: false
-      verbose: true
-      functest: true
-      kattest: false
-      nistkattest: false
-      acvptest: false
-      cbmc: true
-      cbmc_mlkem_k: 3
-    secrets: inherit
-  cbmc_k4:
-    name: CBMC (ML-KEM-1024)
-    needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint]
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    uses: ./.github/workflows/ci_ec2_reusable.yml
-    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
-    with:
-      name: CBMC (MLKEM-1024)
-      ec2_instance_type: c7g.2xlarge
-      ec2_ami: ubuntu-latest (custom AMI)
-      ec2_ami_id: ami-08ddb0acd99dc3d33 # aarch64, ubuntu-latest, 64g
-      compile_mode: native
-      opt: no_opt
-      lint: false
-      verbose: true
-      functest: true
-      kattest: false
-      nistkattest: false
-      acvptest: false
-      cbmc: true
-      cbmc_mlkem_k: 4
-    secrets: inherit