diff --git a/.github/actions/bench/action.yml b/.github/actions/bench/action.yml
index 248e72b26..b321ecec5 100644
--- a/.github/actions/bench/action.yml
+++ b/.github/actions/bench/action.yml
@@ -32,24 +32,46 @@ inputs:
   gh_token:
      description: GitHub access token
      required: true
+  use-nix:
+    description: Whether to run in the default Nix environment
+    default: true
+  custom_shell:
+    description: The shell to use. Only relevant if use-nix is 'false'
+    default: 'bash'
 runs:
   using: composite
   steps:
-      - name: Run benchmark
-        shell: nix develop .#ci -c bash -e {0}
-        run: |
-          tests bench -c ${{ inputs.perf }} --cflags "${{ inputs.cflags }}" --arch-flags "${{ inputs.archflags }}" -v --output output.json ${{ inputs.bench_extra_args }}
-      - name: Dump benchmark
-        shell: bash
-        if: ${{ inputs.store_results != 'true' }}
-        run: |
-          cat output.json
-      - name: Store benchmark result
-        if: ${{ inputs.store_results == 'true' }}
-        uses: benchmark-action/github-action-benchmark@v1
-        with:
-          name: ${{ inputs.name }}
-          tool: 'customSmallerIsBetter'
-          output-file-path: output.json
-          github-token: ${{ inputs.gh_token }}
-          auto-push: true
+    - name: Setup nix
+      if: ${{ inputs.use-nix }}
+      uses: ./.github/actions/setup-nix
+      with:
+        devShell: ci
+        script: |
+          ARCH=$(uname -m)
+          cat >> $GITHUB_STEP_SUMMARY <<-EOF
+            ## Setup
+            Architecture: $ARCH
+            - $(uname -a)
+            - $(nix --version)
+            - $(${{ matrix.target.cross_prefix }}gcc --version | grep -m1 "")
+            - $(bash --version | grep -m1 "")
+
+            ## CPU Info
+            $(cat /proc/cpuinfo)
+          EOF
+    - name: Set shell
+      shell: bash
+      run: echo SHELL="${{ inputs.use-nix && 'nix develop .#ci -c bash -e {0}' || inputs.custom_shell }}" >> $GITHUB_ENV
+    - name: Run benchmark
+      shell: ${{ env.SHELL }}
+      run: |
+        tests bench -c ${{ inputs.perf }} --cflags "${{ inputs.cflags }}" --arch-flags "${{ inputs.archflags }}" -v --output output.json ${{ inputs.bench_extra_args }}
+    - name: Store benchmark result
+      if: ${{ inputs.store_results == 'true' }}
+      uses: benchmark-action/github-action-benchmark@v1
+      with:
+        name: ${{ inputs.name }}
+        tool: 'customSmallerIsBetter'
+        output-file-path: output.json
+        github-token: ${{ inputs.gh_token }}
+        auto-push: true
diff --git a/.github/actions/cbmc/action.yml b/.github/actions/cbmc/action.yml
new file mode 100644
index 000000000..a06207c0c
--- /dev/null
+++ b/.github/actions/cbmc/action.yml
@@ -0,0 +1,47 @@
+# SPDX-License-Identifier: Apache-2.0
+
+name: CBMC
+description: Run CBMC proofs for MLKEM-C_AArch64
+
+inputs:
+  use-nix:
+    description: Whether to run in the default Nix environment
+    default: true
+  custom_shell:
+    description: The shell to use. Only relevant if use-nix is 'false'
+    default: 'bash'
+  cross-prefix:
+    description: Binary prefix for cross compilation
+    default: ''
+runs:
+  using: composite
+  steps:
+      - uses: actions/checkout@v4
+      - name: Setup nix
+        if: ${{ inputs.use-nix }}
+        uses: ./.github/actions/setup-nix
+        with:
+          devShell: ci-cbmc
+          script: |
+            cat >> $GITHUB_STEP_SUMMARY << EOF
+              ## Setup
+              Architecture: $(uname -m)
+              - $(nix --version)
+              - $(cbmc --version)
+              - litani Version $(litani --version)
+              - Cadical Version $(cadical --version)
+              - $(${{ inputs.cross_prefix }}gcc --version | grep -m1 "")
+              - $(bash --version | grep -m1 "")
+            EOF
+      - name: Set shell
+        shell: bash
+        run: echo SHELL="${{ inputs.use-nix && 'nix develop .#ci-cbmc -c bash -e {0}' || inputs.custom_shell }}" >> $GITHUB_ENV
+      - name: Run CBMC proofs
+        shell: ${{ env.SHELL }}
+        run: |
+          cd cbmc/proofs;
+          echo "::group::cbmc"
+          KYBER_K=2 ./run-cbmc-proofs.py --summarize;
+          KYBER_K=3 ./run-cbmc-proofs.py --summarize;
+          KYBER_K=4 ./run-cbmc-proofs.py --summarize;
+          echo "::endgroup::"
diff --git a/.github/actions/functest/action.yml b/.github/actions/functest/action.yml
new file mode 100644
index 000000000..d0f4ec798
--- /dev/null
+++ b/.github/actions/functest/action.yml
@@ -0,0 +1,64 @@
+# SPDX-License-Identifier: Apache-2.0
+
+name: Functional tests
+description: Run functional tests for MLKEM-C_AArch64
+
+inputs:
+  use-nix:
+    description: Whether to run in the default Nix environment
+    default: true
+  cflags:
+    description: CFLAGS to pass to compilation
+    default: ''
+  cross-prefix:
+    description: Binary prefix for cross compilation
+    default: ''
+runs:
+  using: composite
+  steps:
+      - name: Setup nix
+        uses: ./.github/actions/setup-nix
+        if: ${{ inputs.use-nix }}
+        with:
+          devShell: ci
+          script: |
+            ARCH=$(uname -m)
+            cat >> $GITHUB_STEP_SUMMARY <<-EOF
+              ## Setup
+              Architecture: $ARCH
+              - $(uname -a)
+              - $(nix --version)
+              - $(${{ inputs.cross-prefix }}gcc --version | grep -m1 "")
+              - $(bash --version | grep -m1 "")
+            EOF
+      - name: Set shell
+        shell: bash
+        run: echo SHELL="${{ inputs.use-nix && 'nix develop .#ci -c bash -e {0}' || inputs.custom_shell }}" >> $GITHUB_ENV
+      - name: Run functional tests
+        id: func_test
+        shell: ${{ env.SHELL }}
+        run: |
+          echo "::group::func_test"
+          tests func --cross-prefix=${{ inputs.cross-prefix }} --cflags ${{ inputs.cflags }} -v
+          echo "::endgroup::"
+      - name: Run KAT tests
+        if: |
+          success()
+          || steps.func_test.conclusion == 'failure'
+        id: kat_test
+        shell: ${{ env.SHELL }}
+        run: |
+          echo "::group::func_test"
+          tests kat --cross-prefix=${{ inputs.cross-prefix }} --cflags ${{ inputs.cflags }} -v
+          echo "::endgroup::"
+      - name: Run Nistkat tests
+        id: nistkat_test
+        if: |
+          success()
+          || steps.func_test.conclusion == 'failure'
+          || steps.kat_test.conclusion == 'failure'
+        shell: ${{ env.SHELL }}
+        run: |
+          echo "::group::func_test"
+          tests nistkat --cross-prefix=${{ inputs.cross-prefix }} --cflags ${{ inputs.cflags }} -v
+          echo "::endgroup::"
diff --git a/.github/actions/lint/action.yml b/.github/actions/lint/action.yml
new file mode 100644
index 000000000..95ccb4b9e
--- /dev/null
+++ b/.github/actions/lint/action.yml
@@ -0,0 +1,41 @@
+# SPDX-License-Identifier: Apache-2.0
+
+name: Lint
+description: Lint MLKEM-C_AArch64
+
+inputs:
+  use-nix:
+    description: Whether to run in the default Nix environment
+    default: true
+  custom_shell:
+    description: The shell to use. Only relevant if use-nix is 'false'
+    default: 'bash'
+  cross-prefix:
+    description: Binary prefix for cross compilation
+    default: ''
+runs:
+  using: composite
+  steps:
+      - name: Setup nix
+        if: ${{ inputs.use-nix }}
+        uses: ./.github/actions/setup-nix
+        with:
+          devShell: ci-linter
+          script: |
+            cat >> $GITHUB_STEP_SUMMARY << EOF
+              ## Setup
+              Architecture: $(uname -m)
+              - $(uname -a)
+              - $(nix --version)
+              - $(astyle --version)
+              - $(${{ matrix.target.cross-prefix }}gcc --version | grep -m1 "")
+              - $(bash --version | grep -m1 "")
+            EOF
+      - name: Set shell
+        shell: bash
+        run: echo SHELL="${{ inputs.use-nix && 'nix develop .#ci-linter -c bash -e {0}' || inputs.custom_shell }}" >> $GITHUB_ENV
+      - name: Run linter
+        shell: ${{ env.SHELL }}
+        run: |
+          echo "## Lint & Checks" >> $GITHUB_STEP_SUMMARY
+          lint
diff --git a/.github/actions/setup-nix/action.yml b/.github/actions/setup-nix/action.yml
index db3c919a4..248d0b7fc 100644
--- a/.github/actions/setup-nix/action.yml
+++ b/.github/actions/setup-nix/action.yml
@@ -17,10 +17,10 @@ runs:
     - uses: DeterminateSystems/nix-installer-action@v13
     - uses: DeterminateSystems/magic-nix-cache-action@v7
     - name: Prepare nix dev shell
-      shell: nix develop .#${{ inputs.devShell }} -c bash -e {0}
+      shell: nix develop --quiet .#${{ inputs.devShell }} -c bash -e {0}
       run: |
     - name: Dependency check
-      shell: nix develop .#${{ inputs.devShell }} -c bash -e {0}
+      shell: nix develop --quiet .#${{ inputs.devShell }} -c bash -e {0}
       if: inputs.script != ''
       env:
         INPUT_SCRIPT: ${{ inputs.script }}
diff --git a/.github/workflows/bench.yml b/.github/workflows/bench.yml
index dfc9362a6..17ec4375f 100644
--- a/.github/workflows/bench.yml
+++ b/.github/workflows/bench.yml
@@ -32,35 +32,11 @@ jobs:
           archflags: "-mcpu=cortex-a55 -march=armv8.2-a"
           cflags: "-static -DFORCE_AARCH64"
           bench_extra_args: -w exec-on-a55
-    runs-on: self-hosted-${{ matrix.target.system }}
-    defaults:
-      run:
-        shell: nix develop .#ci -c bash -e {0}
-    permissions:
-      contents: write
     if: github.repository_owner == 'pq-code-package' && (github.event.label.name == 'benchmark' || github.ref == 'refs/heads/main')
+    runs-on: self-hosted-${{ matrix.target.system }}
     steps:
       - uses: actions/checkout@v4
-      - name: Setup nix
-        uses: ./.github/actions/setup-nix
-        with:
-          devShell: ci
-          script: |
-            ARCH=$(uname -m)
-            cat >> $GITHUB_STEP_SUMMARY <<-EOF
-              ## Setup
-              Architecture: $ARCH
-              - $(uname -a)
-              - $(nix --version)
-              - $(astyle --version)
-              - $(${{ matrix.target.cross_prefix }}gcc --version | grep -m1 "")
-              - $(bash --version | grep -m1 "")
-
-              ## CPU Info
-              $(cat /proc/cpuinfo)
-            EOF
-      - name: Run benchmark
-        uses: ./.github/actions/bench
+      - uses: ./.github/actions/bench
         with:
           name: ${{ matrix.target.name }}
           cflags: ${{ matrix.target.cflags }}
@@ -68,4 +44,4 @@ jobs:
           perf: ${{ matrix.target.bench_pmu }}
           store_results: ${{ github.repository_owner == 'pq-code-package' && github.ref == 'refs/heads/main' }}
           bench_extra_args: ${{ matrix.target.bench_extra_args }}
-          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          gh_token: ${{ secrets.AWS_GITHUB_TOKEN }}
diff --git a/.github/workflows/bench_ec2_all.yml b/.github/workflows/bench_ec2_all.yml
index f4eb50611..910985bd8 100644
--- a/.github/workflows/bench_ec2_all.yml
+++ b/.github/workflows/bench_ec2_all.yml
@@ -1,3 +1,5 @@
+# SPDX-License-Identifier: Apache-2.0
+
 name: Bench EC2
 on:
   workflow_dispatch:
diff --git a/.github/workflows/bench_ec2_any.yml b/.github/workflows/bench_ec2_any.yml
index 82fac8a49..2d9c8d89e 100644
--- a/.github/workflows/bench_ec2_any.yml
+++ b/.github/workflows/bench_ec2_any.yml
@@ -1,3 +1,5 @@
+# SPDX-License-Identifier: Apache-2.0
+
 name: bench-ec2-any
 on:
   workflow_dispatch:
diff --git a/.github/workflows/bench_ec2_reusable.yml b/.github/workflows/bench_ec2_reusable.yml
index 1be2955a2..3eef059e3 100644
--- a/.github/workflows/bench_ec2_reusable.yml
+++ b/.github/workflows/bench_ec2_reusable.yml
@@ -1,3 +1,5 @@
+# SPDX-License-Identifier: Apache-2.0
+
 name: bench-ec2-reusable
 on:
   workflow_call:
@@ -72,31 +74,13 @@ jobs:
           security-group-id: sg-0ab2e297196c8c381
   bench:
     name: Bench ${{ inputs.name }}
+    runs-on: ${{ needs.start-ec2-runner.outputs.label }}
     needs: start-ec2-runner # required to start the main job when the runner is ready
-    runs-on: ${{ needs.start-ec2-runner.outputs.label }} # run the job on the newly created runner
     steps:
       - uses: actions/checkout@v4
-      - name: Setup nix
-        uses: ./.github/actions/setup-nix
-        with:
-          devShell: ci
-          script: |
-            ARCH=$(uname -m)
-            cat >> $GITHUB_STEP_SUMMARY <<-EOF
-              ## Setup
-              Architecture: $ARCH
-              - $(uname -a)
-              - $(nix --version)
-              - $(astyle --version)
-              - $(${{ matrix.target.cross_prefix }}gcc --version | grep -m1 "")
-              - $(bash --version | grep -m1 "")
-
-              ## CPU Info
-              $(cat /proc/cpuinfo)
-            EOF
-      - name: Run benchmark
-        uses: ./.github/actions/bench
+      - uses: ./.github/actions/bench
         with:
+          use-nix: true
           name: ${{ inputs.name }}
           cflags: ${{ inputs.cflags }}
           archflags: ${{ inputs.archflags }}
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 3c33d9597..4225de911 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -34,110 +34,35 @@ jobs:
            target:
              - runner: 'pqcp-arm64'
                name: 'ubuntu-latest (aarch64)'
-    name: build_kat (${{ matrix.target.name }})
+    name: Functional tests (${{ matrix.target.name }})
     runs-on: ${{ matrix.target.runner }}
-    defaults:
-      run:
-        shell: nix develop .#ci -c bash -e {0}
     steps:
       - uses: actions/checkout@v4
-      - name: Setup nix
-        uses: ./.github/actions/setup-nix
+      - uses: ./.github/actions/functest
         with:
-          devShell: ci
-          script: |
-            ARCH=$(uname -m)
-            cat >> $GITHUB_STEP_SUMMARY <<-EOF
-              ## Setup
-              Architecture: $ARCH
-              - $(uname -a)
-              - $(nix --version)
-              - $(astyle --version)
-              - $(${{ matrix.target.cross-prefix }}gcc --version | grep -m1 "")
-              - $(bash --version | grep -m1 "")
-            EOF
-
-            if [[ "$ARCH" != ${{ matrix.target.arch }} ]]; then
-              echo ":x: Expecting to run on ${{ matrix.target.arch }}, but instead running on $ARCH" >> $GITHUB_STEP_SUMMARY
-              exit 1
-            fi
-      - name: Run functional tests
-        id: func_test
-        run: |
-          tests func --cross-prefix=${{ matrix.target.cross-prefix }} --cflags ${{ matrix.target.cflags }} -v
-      - name: Run KAT tests
-        id: kat_test
-        if: |
-          success()
-          || steps.func_test.conclusion == 'failure'
-        run: |
-          tests kat --cross-prefix=${{ matrix.target.cross-prefix }} --cflags ${{ matrix.target.cflags }} -v
-      - name: Run Nistkat tests
-        id: nistkat_test
-        if: |
-          success()
-          || steps.func_test.conclusion == 'failure'
-          || steps.kat_test.conclusion == 'failure'
-        run: |
-          tests nistkat --cross-prefix=${{ matrix.target.cross-prefix }} --cflags ${{ matrix.target.cflags }} -v
+          use-nix: true
+          cflags: ${{ matrix.target.cflags }}
+          cross-prefix: ${{ matrix.target.cross-prefix }}
   lint:
     strategy:
       matrix:
         system: [ubuntu-latest]
+    name: Linting
     runs-on: ${{ matrix.system }}
-    defaults:
-      run:
-        shell: nix develop .#ci-linter -c bash -e {0}
-    env:
-      CROSS_PREFIX: "${{ (matrix.system == 'ubuntu-latest' && 'aarch64-unknown-linux-gnu-') || '' }}"
     steps:
       - uses: actions/checkout@v4
-      - name: Setup nix
-        uses: ./.github/actions/setup-nix
+      - uses: ./.github/actions/lint
         with:
-          devShell: ci-linter
-          script: |
-            cat >> $GITHUB_STEP_SUMMARY << EOF
-              ## Setup
-              Architecture: $(uname -m)
-              - $(uname -a)
-              - $(nix --version)
-              - $(astyle --version)
-              - $(${{ matrix.target.cross-prefix }}gcc --version | grep -m1 "")
-              - $(bash --version | grep -m1 "")
-            EOF
-      - name: Lint
-        run: |
-          echo "## Lint & Checks" >> $GITHUB_STEP_SUMMARY
-          lint
+          use-nix: true
+          cross-prefix: "aarch64-unknown-linux-gnu-"
   cbmc:
     strategy:
       matrix:
         system: [macos-latest]
+    name: CBMC
     runs-on: ${{ matrix.system }}
-    defaults:
-      run:
-        shell: nix develop .#ci-cbmc -c bash -e {0}
     steps:
       - uses: actions/checkout@v4
-      - name: Setup nix
-        uses: ./.github/actions/setup-nix
+      - uses: ./.github/actions/cbmc
         with:
-          devShell: ci-cbmc
-          script: |
-            cat >> $GITHUB_STEP_SUMMARY << EOF
-              ## Setup
-              Architecture: $(uname -m)
-              - $(nix --version)
-              - $(cbmc --version)
-              - litani Version $(litani --version)
-              - Cadical Version $(cadical --version)
-              - $(${{ matrix.cross_prefix }}gcc --version | grep -m1 "")
-              - $(bash --version | grep -m1 "")
-            EOF
-      - name: Run CBMC proofs
-        run: |
-          cd cbmc/proofs;
-          KYBER_K=2 ./run-cbmc-proofs.py --summarize;
-          KYBER_K=3 ./run-cbmc-proofs.py --summarize;
-          KYBER_K=4 ./run-cbmc-proofs.py --summarize;
+          use-nix: true
diff --git a/.github/workflows/ci_ec2_any.yml b/.github/workflows/ci_ec2_any.yml
new file mode 100644
index 000000000..8db8ad305
--- /dev/null
+++ b/.github/workflows/ci_ec2_any.yml
@@ -0,0 +1,46 @@
+# SPDX-License-Identifier: Apache-2.0
+
+name: ci-ec2-any
+on:
+  workflow_dispatch:
+    inputs:
+      name:
+        description: Alternative name of instance
+        default: Graviton2
+      ec2_instance_type:
+        description: Type if EC2 instance to run on
+        default: t4g.small
+      ec2_ami_id:
+        description: AMI ID
+        default: ami-096ea6a12ea24a797
+      cflags:
+        description: Custom CFLAGS for compilation
+        default:
+      cross-prefix:
+        description: Cross-compilation binary prefix, if any
+        default: ' '
+      always_terminate:
+        description: Indicates if instance should always be terminated, even on failure
+        default: 'true'
+      functest:
+        description: Whether to run functional tests
+        default: 'true'
+      lint:
+        description: Whether to lint
+        default: 'true'
+      cbmc:
+        description: Whether to run CBMC proofs
+        default: 'false'
+jobs:
+  ci-ec2-any:
+    name: Ad-hoc CI on $${{ github.event.inputs.ec2_instance_type }}
+    uses: ./.github/workflows/ci_ec2_reusable.yml
+    with:
+      ec2_instance_type: ${{ github.event.inputs.ec2_instance_type }}
+      ec2_ami_id: ${{ github.event.inputs.ec2_ami_id }}
+      cflags: ${{ github.event.inputs.cflags }}
+      crosss-prefix: ${{ github.event.inputs.cross-prefix }}
+      functest: ${{ github.event.inputs.functest }}
+      lint: ${{ github.event.inputs.lint }}
+      cbmc: ${{ github.event.inputs.cbmc }}
+    secrets: inherit
diff --git a/.github/workflows/ci_ec2_reusable.yml b/.github/workflows/ci_ec2_reusable.yml
new file mode 100644
index 000000000..14cfc10f5
--- /dev/null
+++ b/.github/workflows/ci_ec2_reusable.yml
@@ -0,0 +1,132 @@
+# SPDX-License-Identifier: Apache-2.0
+
+name: ci-ec2-reusable
+on:
+  workflow_call:
+    inputs:
+      name:
+        type: string
+        description: Alternative name of instance
+        default: Graviton2
+      ec2_instance_type:
+        type: string
+        description: Type if EC2 instance to benchmark on
+        default: t4g.small
+      ec2_ami_id:
+        type: string
+        description: AMI ID
+        default: ami-096ea6a12ea24a797
+      cflags:
+        type: string
+        description: Custom CFLAGS for compilation
+        default:
+      cross-prefix:
+        type: string
+        description: Cross-compilation binary prefix, if any
+        default: ' '
+      always_terminate:
+        type: string
+        description: Indicates if instance should always be terminated, even on failure
+        default: 'true'
+      functest:
+        type: boolean
+        default: 'true'
+      lint:
+        type: boolean
+        default: 'true'
+      cbmc:
+        type: boolean
+        default: 'false'
+env:
+  AWS_ROLE: arn:aws:iam::559050233797:role/mlkem-c-aarch64-gh-action
+  AWS_REGION: us-east-1
+jobs:
+  start-ec2-runner:
+    name: Start ${{ github.event.inputs.name }} (${{ github.event.inputs.ec2_instance_type }})
+    permissions:
+      contents: 'read'
+      id-token: 'write'
+    runs-on: ubuntu-latest
+    outputs:
+      label: ${{ steps.start-ec2-runner.outputs.label }}
+      ec2-instance-id: ${{ steps.start-ec2-runner.outputs.ec2-instance-id }}
+    steps:
+      - uses: actions/checkout@v4
+      - name: Clear nix-installer action cache
+        uses: ./.github/actions/clear-cache
+        with:
+           key_prefix: determinatesystem-nix-installer-
+           repository: ${{ github.repository }}
+           gh_token: ${{ secrets.AWS_GITHUB_TOKEN }}
+      - name: Configure AWS credentials
+        uses: aws-actions/configure-aws-credentials@v4
+        with:
+          role-to-assume: ${{ env.AWS_ROLE }}
+          aws-region: ${{ env.AWS_REGION }}
+      - name: Start EC2 runner
+        id: start-ec2-runner
+        uses: machulav/ec2-github-runner@v2
+        with:
+          mode: start
+          github-token: ${{ secrets.AWS_GITHUB_TOKEN }}
+          ec2-image-id: ${{ inputs.ec2_ami_id }}
+          ec2-instance-type: ${{ inputs.ec2_instance_type }}
+          subnet-id: subnet-07b2729e5e065962f
+          security-group-id: sg-0ab2e297196c8c381
+  functest:
+    name: Functional tests ${{ inputs.name }}
+    needs: start-ec2-runner
+    runs-on: ${{ needs.start-ec2-runner.outputs.label }}
+    if: ${{ inputs.functest == 'true' }}
+    steps:
+      - uses: actions/checkout@v4
+      - uses: ./.github/actions/functest
+        with:
+          use-nix: true
+          cflags: ${{ matrix.target.cflags }}
+          cross-prefix: ${{ matrix.target.cross-prefix }}
+  lint:
+    name: Linting ${{ inputs.name }}
+    needs: start-ec2-runner
+    runs-on: ${{ needs.start-ec2-runner.outputs.label }}
+    if: ${{ inputs.lint == 'true' }}
+    steps:
+      - uses: actions/checkout@v4
+      - uses: ./.github/actions/lint
+        with:
+          use-nix: true
+          cross-prefix: ${{ inputs.cross-prefix }}
+  cbmc:
+    name: CBMC ${{ inputs.name }}
+    needs: start-ec2-runner
+    runs-on: ${{ needs.start-ec2-runner.outputs.label }}
+    if: ${{ inputs.cbmc == 'true' }}
+    steps:
+      - uses: actions/checkout@v4
+      - uses: ./.github/actions/cbmc
+        with:
+          use-nix: true
+          cross-prefix: ${{ inputs.cross-prefix }}
+  stop-ec2-runner:
+    name: Stop ${{ github.event.inputs.name }} (${{ github.event.inputs.ec2_instance_type }})
+    permissions:
+      contents: 'read'
+      id-token: 'write'
+    needs:
+      - start-ec2-runner
+      - bench # required to wait when the main job is done
+    runs-on: ubuntu-latestn
+    if: ${{ (inputs.always_terminate == 'true' && always()) || success() }} # required to stop the runner even if the error happened in the previous jobs
+    steps:
+      - name: Configure AWS credentials
+        uses: aws-actions/configure-aws-credentials@v4
+        with:
+          role-to-assume: ${{ env.AWS_ROLE }}
+          aws-region: ${{ env.AWS_REGION }}
+      - name: Stop EC2 runner
+        uses: machulav/ec2-github-runner@v2
+        with:
+          mode: stop
+          github-token: ${{ secrets.AWS_GITHUB_TOKEN }}
+          label: ${{ needs.start-ec2-runner.outputs.label }}
+          ec2-instance-id: ${{ needs.start-ec2-runner.outputs.ec2-instance-id }}