diff --git a/.github/actions/cbmc/action.yml b/.github/actions/cbmc/action.yml
index f5915dc683..4da0ad7d59 100644
--- a/.github/actions/cbmc/action.yml
+++ b/.github/actions/cbmc/action.yml
@@ -20,6 +20,24 @@ inputs:
   mlkem_k:
     description: "Security level for ML-KEM (2,3,4)"
     default: "2"
+  cbmc-target:
+    description: "CBMC target platform; empty uses the default host model"
+    default: ""
+  proofs:
+    description: "Space-separated proof patterns to run; empty runs all proofs"
+    default: ""
+  single-step:
+    description: "Run proofs one at a time"
+    default: "false"
+  timeout:
+    description: "Timeout for individual CBMC proofs, in seconds"
+    default: "3600"
+  per-proof-timeout:
+    description: "Timeout passed to run-cbmc-proofs.py for each proof"
+    default: "1800"
+  report:
+    description: "Publish CBMC runtime regression report"
+    default: "true"
   gh_token:
     description: Github access token to use
     required: true
@@ -53,14 +71,44 @@ runs:
         env:
           GH_TOKEN: ${{ inputs.gh_token }}
         run: |
-          echo "::group::cbmc_${{ inputs.mlkem_k }}"
-          tests cbmc --mlkem-parameter-set ${{ inputs.mlkem_k }} --per-proof-timeout 1800 --output-result-json ${{ github.workspace }}/cbmc_result_k${{ inputs.mlkem_k }}.json || cbmc_failed=true
+          cbmc_failed=false
+          cbmc_target="${{ inputs.cbmc-target }}"
+          group_name="cbmc_${{ inputs.mlkem_k }}"
+          result_suffix=""
+          if [ -n "$cbmc_target" ]; then
+            group_name="${group_name}_${cbmc_target}"
+            result_suffix="_${cbmc_target//[^A-Za-z0-9_.-]/_}"
+          fi
+          result_json="${{ github.workspace }}/cbmc_result_k${{ inputs.mlkem_k }}${result_suffix}.json"
+          cbmc_args=(
+            --mlkem-parameter-set "${{ inputs.mlkem_k }}"
+            --timeout "${{ inputs.timeout }}"
+            --per-proof-timeout "${{ inputs.per-proof-timeout }}"
+          )
+          if [ -n "$cbmc_target" ]; then
+            cbmc_args+=(--cbmc-target "$cbmc_target")
+          fi
+          proofs="${{ inputs.proofs }}"
+          if [ -n "$proofs" ]; then
+            read -r -a proof_args <<< "$proofs"
+            cbmc_args+=(-p "${proof_args[@]}")
+          fi
+          if [ "${{ inputs.single-step }}" = "true" ]; then
+            cbmc_args+=(--single-step --fail-upon-error)
+          fi
+          if [ "${{ inputs.report }}" = "true" ]; then
+            cbmc_args+=(--output-result-json "$result_json")
+          fi
+          echo "::group::$group_name"
+          tests cbmc "${cbmc_args[@]}" || cbmc_failed=true
           echo "::endgroup::"
-          python3 ${{ github.action_path }}/report.py \
-            --results-json "${{ github.workspace }}/cbmc_result_k${{ inputs.mlkem_k }}.json" \
-            --mlkem-k "${{ inputs.mlkem_k }}" \
-            --min-runtime 20 \
-            --regression-threshold 1.5 \
-            --gh-pages-branch gh-pages \
-            --data-dir dev/cbmc
+          if [ "${{ inputs.report }}" = "true" ]; then
+            python3 ${{ github.action_path }}/report.py \
+              --results-json "$result_json" \
+              --mlkem-k "${{ inputs.mlkem_k }}" \
+              --min-runtime 20 \
+              --regression-threshold 1.5 \
+              --gh-pages-branch gh-pages \
+              --data-dir dev/cbmc
+          fi
           if [ "$cbmc_failed" = "true" ]; then exit 1; fi
diff --git a/.github/workflows/cbmc.yml b/.github/workflows/cbmc.yml
index 749f265ba4..e0e8a416e9 100644
--- a/.github/workflows/cbmc.yml
+++ b/.github/workflows/cbmc.yml
@@ -72,3 +72,40 @@ jobs:
       cbmc: true
       cbmc_mlkem_k: 4
     secrets: inherit
+  cbmc_target_model:
+    name: CBMC target model (${{ matrix.cbmc_target }})
+    if: ${{ github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork }}
+    permissions:
+      contents: 'read'
+      id-token: 'write'
+      pull-requests: 'write'
+    strategy:
+      fail-fast: false
+      matrix:
+        cbmc_target:
+          - i386-linux
+          - x86_64-linux
+          - aarch64-linux
+          - riscv64-linux
+          - ppc64le-linux
+    uses: ./.github/workflows/ci_ec2_reusable.yml
+    with:
+      name: CBMC target model (${{ matrix.cbmc_target }})
+      ec2_instance_type: r8g.xlarge
+      ec2_ami: ubuntu-latest (aarch64)
+      ec2_volume_size: 20
+      compile_mode: native
+      opt: no_opt
+      lint: false
+      verbose: true
+      test: false
+      cbmc: true
+      cbmc_nix_shell: cbmc32
+      cbmc_mlkem_k: 2
+      cbmc_target: ${{ matrix.cbmc_target }}
+      cbmc_proofs: cbmc_target_model
+      cbmc_single_step: true
+      cbmc_report: false
+      cbmc_timeout: 300
+      cbmc_per_proof_timeout: 300
+    secrets: inherit
diff --git a/.github/workflows/ci_ec2_reusable.yml b/.github/workflows/ci_ec2_reusable.yml
index fbaceb9cec..a4cd7ab7c2 100644
--- a/.github/workflows/ci_ec2_reusable.yml
+++ b/.github/workflows/ci_ec2_reusable.yml
@@ -67,9 +67,30 @@ on:
       slothy:
         type: boolean
         default: false
+      cbmc_nix_shell:
+        type: string
+        default: cbmc
       cbmc_mlkem_k:
         type: string
         default: 2
+      cbmc_target:
+        type: string
+        default: ''
+      cbmc_proofs:
+        type: string
+        default: ''
+      cbmc_single_step:
+        type: boolean
+        default: false
+      cbmc_report:
+        type: boolean
+        default: true
+      cbmc_timeout:
+        type: string
+        default: '3600'
+      cbmc_per_proof_timeout:
+        type: string
+        default: '1800'
 env:
   AWS_ROLE: arn:aws:iam::559050233797:role/mlkem-c-aarch64-gh-action
   AWS_REGION: us-east-1
@@ -194,9 +215,15 @@ jobs:
         if: ${{ inputs.cbmc && (success() || failure()) }}
         uses: ./.github/actions/cbmc
         with:
-          nix-shell: cbmc
+          nix-shell: ${{ inputs.cbmc_nix_shell }}
           nix-verbose: ${{ inputs.verbose }}
           mlkem_k: ${{ inputs.cbmc_mlkem_k }}
+          cbmc-target: ${{ inputs.cbmc_target }}
+          proofs: ${{ inputs.cbmc_proofs }}
+          single-step: ${{ inputs.cbmc_single_step }}
+          report: ${{ inputs.cbmc_report }}
+          timeout: ${{ inputs.cbmc_timeout }}
+          per-proof-timeout: ${{ inputs.cbmc_per_proof_timeout }}
           gh_token: ${{ secrets.AWS_GITHUB_TOKEN }}
       - name: SLOTHY
         if: ${{ inputs.slothy }}
diff --git a/flake.nix b/flake.nix
index 1e6d3b3f31..2fec952ee2 100644
--- a/flake.nix
+++ b/flake.nix
@@ -79,6 +79,7 @@
           packages.toolchains = util.toolchains;
           packages.toolchains_native = util.toolchains_native;
           packages.toolchain_x86_64 = util.toolchain_x86_64;
+          packages.toolchain_i686 = util.toolchain_i686;
           packages.toolchain_aarch64 = util.toolchain_aarch64;
           packages.toolchain_riscv64 = util.toolchain_riscv64;
           packages.toolchain_riscv32 = util.toolchain_riscv32;
@@ -116,6 +117,18 @@
           devShells.cbmc = util.mkShell {
             packages = builtins.attrValues { inherit (config.packages) cbmc toolchains_native; } ++ [ pkgs.gh ];
           };
+          devShells.cbmc32 = util.mkShell {
+            packages = builtins.attrValues
+              {
+                inherit (config.packages)
+                  cbmc
+                  toolchain_i686
+                  toolchain_x86_64
+                  toolchain_aarch64
+                  toolchain_riscv64
+                  toolchain_ppc64le;
+              } ++ [ pkgs.gh ];
+          };
           devShells.slothy = util.mkShell {
             packages = builtins.attrValues { inherit (config.packages) slothy linters toolchains_native; };
           };
diff --git a/nix/util.nix b/nix/util.nix
index bbe0d86888..7bd14f98da 100644
--- a/nix/util.nix
+++ b/nix/util.nix
@@ -34,6 +34,7 @@ rec {
   _toolchains = { cross ? true }:
     let
       x86_64-gcc = wrap-gcc pkgs.pkgsCross.gnu64;
+      i686-gcc = wrap-gcc pkgs.pkgsCross.gnu32;
       aarch64-gcc = wrap-gcc pkgs.pkgsCross.aarch64-multiplatform;
       riscv64-gcc = wrap-gcc pkgs.pkgsCross.riscv64;
       riscv32-gcc = wrap-gcc pkgs.pkgsCross.riscv32;
@@ -47,7 +48,7 @@ rec {
       #   and won't just work for now
       # - equip all toolchains if cross is explicitly set to true
       # - On some machines, `native-gcc` needed to be evaluated lastly (placed as the last element of the toolchain list), or else would result in environment variables (CC, AR, ...) overriding issue.
-    pkgs.lib.optionals cross [ pkgs.qemu pkgs.gcc-arm-embedded x86_64-gcc aarch64-gcc riscv64-gcc riscv32-gcc ppc64le-gcc ]
+    pkgs.lib.optionals cross [ pkgs.qemu pkgs.gcc-arm-embedded x86_64-gcc i686-gcc aarch64-gcc riscv64-gcc riscv32-gcc ppc64le-gcc ]
     ++ pkgs.lib.optionals (cross && pkgs.stdenv.isLinux && pkgs.stdenv.isx86_64) [ aarch64_be-gcc ]
     ++ pkgs.lib.optionals cross [ native-gcc ]
     # git is not available in the nix shell on Darwin. As a workaround we add git as a dependency here.
@@ -132,6 +133,11 @@ rec {
     cross_compilers = [ (wrap-gcc pkgs.pkgsCross.gnu64) ];
   };
 
+  toolchain_i686 = _individual_toolchain {
+    name = "i686";
+    cross_compilers = [ (wrap-gcc pkgs.pkgsCross.gnu32) ];
+  };
+
   toolchain_aarch64 = _individual_toolchain {
     name = "aarch64";
     cross_compilers = [ (wrap-gcc pkgs.pkgsCross.aarch64-multiplatform) ];
diff --git a/proofs/cbmc/Makefile.common b/proofs/cbmc/Makefile.common
index a890aa5eb0..0567b610f6 100644
--- a/proofs/cbmc/Makefile.common
+++ b/proofs/cbmc/Makefile.common
@@ -325,9 +325,91 @@ CHECKFLAGS += $(CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK)
 # initialized with unconstrained values.
 NONDET_STATIC ?=
 
+# Target platform for CBMC/goto-cc. Leave unset to preserve the historic
+# host-default model.
+CBMC_TARGET ?=
+CBMC_TARGET_CC ?=
+CBMC_TARGET_GOTO_FLAGS ?=
+CBMC_TARGET_CBMC_FLAGS ?=
+CBMC_TARGET_INSTRUMENT_ENV ?=
+CBMC_TARGET_GCC_AS_GCC_DIR ?=
+CBMC_TARGET_HOST_PATH ?= $(shell printf '%s' "$$PATH")
+CBMC_TARGET_POINTER_BYTES ?= 8
+CBMC_TARGET_SIZE_T_BYTES ?= 8
+CBMC_TARGET_LONG_BYTES ?= 8
+
+ifeq ($(strip $(CBMC_TARGET)),)
+  ifeq ($(strip $(CBMC_TARGET_CC)),)
+    CBMC_TARGET_CC = $(CC)
+  endif
+else ifeq ($(CBMC_TARGET),i386-linux)
+  ifeq ($(strip $(CBMC_TARGET_CC)),)
+    CBMC_TARGET_CC = i686-unknown-linux-gnu-gcc
+  endif
+  CBMC_TARGET_GOTO_FLAGS = --i386-linux
+  CBMC_TARGET_CBMC_FLAGS = --i386-linux
+  ifeq ($(strip $(CBMC_TARGET_GCC_AS_GCC_DIR)),)
+    CBMC_TARGET_GCC_AS_GCC_DIR = $(PROOF_ROOT)/tools/i686-gcc-as-gcc
+  endif
+  CBMC_TARGET_INSTRUMENT_ENV = PATH=$(CBMC_TARGET_GCC_AS_GCC_DIR):$(CBMC_TARGET_HOST_PATH) CC=$(CBMC_TARGET_CC) GCC=$(CBMC_TARGET_CC)
+  CBMC_TARGET_POINTER_BYTES = 4
+  CBMC_TARGET_SIZE_T_BYTES = 4
+  CBMC_TARGET_LONG_BYTES = 4
+else ifeq ($(CBMC_TARGET),x86_64-linux)
+  ifeq ($(strip $(CBMC_TARGET_CC)),)
+    CBMC_TARGET_CC = x86_64-unknown-linux-gnu-gcc
+  endif
+  CBMC_TARGET_CBMC_FLAGS = --arch x86_64 --os linux --LP64
+  ifeq ($(strip $(CBMC_TARGET_GCC_AS_GCC_DIR)),)
+    CBMC_TARGET_GCC_AS_GCC_DIR = $(PROOF_ROOT)/tools/x86_64-gcc-as-gcc
+  endif
+  CBMC_TARGET_INSTRUMENT_ENV = PATH=$(CBMC_TARGET_GCC_AS_GCC_DIR):$(CBMC_TARGET_HOST_PATH) CC=$(CBMC_TARGET_CC) GCC=$(CBMC_TARGET_CC)
+  CBMC_TARGET_POINTER_BYTES = 8
+  CBMC_TARGET_SIZE_T_BYTES = 8
+  CBMC_TARGET_LONG_BYTES = 8
+else ifeq ($(CBMC_TARGET),aarch64-linux)
+  ifeq ($(strip $(CBMC_TARGET_CC)),)
+    CBMC_TARGET_CC = aarch64-unknown-linux-gnu-gcc
+  endif
+  CBMC_TARGET_CBMC_FLAGS = --arch arm64 --os linux --LP64
+  ifeq ($(strip $(CBMC_TARGET_GCC_AS_GCC_DIR)),)
+    CBMC_TARGET_GCC_AS_GCC_DIR = $(PROOF_ROOT)/tools/aarch64-gcc-as-gcc
+  endif
+  CBMC_TARGET_INSTRUMENT_ENV = PATH=$(CBMC_TARGET_GCC_AS_GCC_DIR):$(CBMC_TARGET_HOST_PATH) CC=$(CBMC_TARGET_CC) GCC=$(CBMC_TARGET_CC)
+  CBMC_TARGET_POINTER_BYTES = 8
+  CBMC_TARGET_SIZE_T_BYTES = 8
+  CBMC_TARGET_LONG_BYTES = 8
+else ifeq ($(CBMC_TARGET),riscv64-linux)
+  ifeq ($(strip $(CBMC_TARGET_CC)),)
+    CBMC_TARGET_CC = riscv64-unknown-linux-gnu-gcc
+  endif
+  CBMC_TARGET_CBMC_FLAGS = --arch riscv64 --os linux --LP64
+  ifeq ($(strip $(CBMC_TARGET_GCC_AS_GCC_DIR)),)
+    CBMC_TARGET_GCC_AS_GCC_DIR = $(PROOF_ROOT)/tools/riscv64-gcc-as-gcc
+  endif
+  CBMC_TARGET_INSTRUMENT_ENV = PATH=$(CBMC_TARGET_GCC_AS_GCC_DIR):$(CBMC_TARGET_HOST_PATH) CC=$(CBMC_TARGET_CC) GCC=$(CBMC_TARGET_CC)
+  CBMC_TARGET_POINTER_BYTES = 8
+  CBMC_TARGET_SIZE_T_BYTES = 8
+  CBMC_TARGET_LONG_BYTES = 8
+else ifeq ($(CBMC_TARGET),ppc64le-linux)
+  ifeq ($(strip $(CBMC_TARGET_CC)),)
+    CBMC_TARGET_CC = powerpc64le-unknown-linux-gnu-gcc
+  endif
+  CBMC_TARGET_CBMC_FLAGS = --arch ppc64le --os linux --LP64
+  ifeq ($(strip $(CBMC_TARGET_GCC_AS_GCC_DIR)),)
+    CBMC_TARGET_GCC_AS_GCC_DIR = $(PROOF_ROOT)/tools/ppc64le-gcc-as-gcc
+  endif
+  CBMC_TARGET_INSTRUMENT_ENV = PATH=$(CBMC_TARGET_GCC_AS_GCC_DIR):$(CBMC_TARGET_HOST_PATH) CC=$(CBMC_TARGET_CC) GCC=$(CBMC_TARGET_CC)
+  CBMC_TARGET_POINTER_BYTES = 8
+  CBMC_TARGET_SIZE_T_BYTES = 8
+  CBMC_TARGET_LONG_BYTES = 8
+else
+  $(error Unsupported CBMC_TARGET '$(CBMC_TARGET)'; expected i386-linux, x86_64-linux, aarch64-linux, riscv64-linux, ppc64le-linux, or unset)
+endif
+
 # Flags to pass to goto-cc for compilation and linking
-COMPILE_FLAGS ?= -Wall -Werror --native-compiler $(CC)
-LINK_FLAGS ?= -Wall -Werror
+COMPILE_FLAGS ?= -Wall -Werror $(CBMC_TARGET_GOTO_FLAGS) --native-compiler $(CBMC_TARGET_CC)
+LINK_FLAGS ?= -Wall -Werror $(CBMC_TARGET_GOTO_FLAGS)
 EXPORT_FILE_LOCAL_SYMBOLS ?= --export-file-local-symbols
 
 # During instrumentation, it adds models of C library functions
@@ -555,6 +637,7 @@ endif
 ################################################################
 # CBMC flags common to all proofs
 CBMCFLAGS += $(CBMC_FLAG_FLUSH)
+CBMCFLAGS += $(CBMC_TARGET_CBMC_FLAGS)
 CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS)
 CBMCFLAGS += --slice-formula
 
@@ -563,6 +646,9 @@ CBMCFLAGS += --slice-formula
 DEFINES += -DCBMC=1
 DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS)
 DEFINES += -DCBMC_MAX_OBJECT_SIZE="(SIZE_MAX>>(CBMC_OBJECT_BITS+1))"
+DEFINES += -DCBMC_TARGET_POINTER_BYTES=$(CBMC_TARGET_POINTER_BYTES)
+DEFINES += -DCBMC_TARGET_SIZE_T_BYTES=$(CBMC_TARGET_SIZE_T_BYTES)
+DEFINES += -DCBMC_TARGET_LONG_BYTES=$(CBMC_TARGET_LONG_BYTES)
 
 
 ifndef MLKEM_K
@@ -719,7 +805,7 @@ $(PROOF_GOTO)0100.goto: $(PROOF_SOURCES)
 $(PROJECT_GOTO)0200.goto: $(PROJECT_GOTO)0100.goto
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \
+	    '$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
 	  --stdout-file $(LOGDIR)/remove_function_body-log.txt \
@@ -742,7 +828,7 @@ $(HARNESS_GOTO)0100.goto: $(PROOF_GOTO)0100.goto $(PROJECT_GOTO)0200.goto
 $(HARNESS_GOTO)0200.goto: $(HARNESS_GOTO)0100.goto
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) --remove-function-pointers $^ $@' \
+	    '$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) --remove-function-pointers $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
 	  --stdout-file $(LOGDIR)/restrict_function_pointer-log.txt \
@@ -764,7 +850,7 @@ ifneq ($(strip $(CODE_CONTRACTS)),)
 else
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(NONDET_STATIC) $^ $@' \
+	    '$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(NONDET_STATIC) $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
 	  --stdout-file $(LOGDIR)/nondet_static-log.txt \
@@ -778,7 +864,7 @@ $(HARNESS_GOTO)0400.goto: $(HARNESS_GOTO)0300.goto
 ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(ADD_LIBRARY_FLAG) $(CBMC_OPT_CONFIG_LIBRARY) $^ $@' \
+	    '$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(ADD_LIBRARY_FLAG) $(CBMC_OPT_CONFIG_LIBRARY) $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
 	  --stdout-file $(LOGDIR)/linking-library-models-log.txt \
@@ -801,7 +887,7 @@ $(HARNESS_GOTO)0500.goto: $(HARNESS_GOTO)0400.goto
 ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(UNWIND_0500_FLAGS) $^ $@' \
+	    '$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(UNWIND_0500_FLAGS) $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
 	  --stdout-file $(LOGDIR)/unwind_loops-log.txt \
@@ -811,7 +897,7 @@ ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
 else ifneq ($(strip $(CODE_CONTRACTS)),)
 	$(LITANI) add-job \
 	  --command \
-		'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \
+		'$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
 	  --stdout-file $(LOGDIR)/unwind_loops-log.txt \
@@ -833,7 +919,7 @@ endif
 $(HARNESS_GOTO)0600.goto: $(HARNESS_GOTO)0500.goto
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_USE_DYNAMIC_FRAMES) $(NONDET_STATIC) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $(CBMC_USE_FUNCTION_CONTRACTS) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \
+	    '$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_USE_DYNAMIC_FRAMES) $(NONDET_STATIC) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $(CBMC_USE_FUNCTION_CONTRACTS) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
 	  --stdout-file $(LOGDIR)/check_function_contracts-log.txt \
@@ -845,7 +931,7 @@ $(HARNESS_GOTO)0600.goto: $(HARNESS_GOTO)0500.goto
 $(HARNESS_GOTO)0700.goto: $(HARNESS_GOTO)0600.goto
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \
+	    '$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
 	  --stdout-file $(LOGDIR)/slice_global_inits-log.txt \
@@ -857,7 +943,7 @@ $(HARNESS_GOTO)0700.goto: $(HARNESS_GOTO)0600.goto
 $(HARNESS_GOTO)0800.goto: $(HARNESS_GOTO)0700.goto
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \
+	    '$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
 	  --stdout-file $(LOGDIR)/drop_unused_functions-log.txt \
diff --git a/proofs/cbmc/cbmc_target_model/Makefile b/proofs/cbmc/cbmc_target_model/Makefile
new file mode 100644
index 0000000000..4861eee310
--- /dev/null
+++ b/proofs/cbmc/cbmc_target_model/Makefile
@@ -0,0 +1,21 @@
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = cbmc_target_model_harness
+
+PROOF_UID = mlk_cbmc_target_model
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(PROOFDIR)/cbmc_target_model_project.c
+
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = harness
+
+CBMC_OBJECT_BITS = 8
+
+include ../Makefile.common
diff --git a/proofs/cbmc/cbmc_target_model/cbmc_target_model_harness.c b/proofs/cbmc/cbmc_target_model/cbmc_target_model_harness.c
new file mode 100644
index 0000000000..3081afd1a7
--- /dev/null
+++ b/proofs/cbmc/cbmc_target_model/cbmc_target_model_harness.c
@@ -0,0 +1,19 @@
+// Copyright (c) The mlkem-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include <stddef.h>
+#include <stdint.h>
+
+void __CPROVER_assert(_Bool, const char *);
+
+void harness(void)
+{
+  __CPROVER_assert(sizeof(void *) == CBMC_TARGET_POINTER_BYTES,
+                   "CBMC target pointer width matches selected model");
+  __CPROVER_assert(sizeof(size_t) == CBMC_TARGET_SIZE_T_BYTES,
+                   "CBMC target size_t width matches selected model");
+  __CPROVER_assert(sizeof(long) == CBMC_TARGET_LONG_BYTES,
+                   "CBMC target long width matches selected model");
+  __CPROVER_assert(sizeof(uint64_t) == 8,
+                   "CBMC target uint64_t width is 8 bytes");
+}
diff --git a/proofs/cbmc/cbmc_target_model/cbmc_target_model_project.c b/proofs/cbmc/cbmc_target_model/cbmc_target_model_project.c
new file mode 100644
index 0000000000..a4eee1de4d
--- /dev/null
+++ b/proofs/cbmc/cbmc_target_model/cbmc_target_model_project.c
@@ -0,0 +1,4 @@
+// Copyright (c) The mlkem-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+int cbmc_target_model_project_anchor;
diff --git a/proofs/cbmc/ntt_butterfly_block/Makefile b/proofs/cbmc/ntt_butterfly_block/Makefile
index c3badc6ef3..7c3b740564 100644
--- a/proofs/cbmc/ntt_butterfly_block/Makefile
+++ b/proofs/cbmc/ntt_butterfly_block/Makefile
@@ -26,7 +26,7 @@ USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
-CBMCFLAGS=--bitwuzla
+CBMCFLAGS=--smt2
 
 FUNCTION_NAME = mlk_ntt_butterfly_block
 
diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k2_native_aarch64/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k2_native_aarch64/Makefile
index b72fc2030c..e42237ed1d 100644
--- a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k2_native_aarch64/Makefile
+++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k2_native_aarch64/Makefile
@@ -12,7 +12,7 @@ PROOF_UID = polyvec_basemul_acc_montgomery_cached_k2_native_aarch64
 
 # We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be
 # included, which contains the CBMC specifications.
-DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/aarch64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
+DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/aarch64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_BUILD -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=
diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k2_native_x86_64/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k2_native_x86_64/Makefile
index aeb6f426da..ff2ee7b71e 100644
--- a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k2_native_x86_64/Makefile
+++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k2_native_x86_64/Makefile
@@ -12,7 +12,7 @@ PROOF_UID = polyvec_basemul_acc_montgomery_cached_k2_native_x86_64
 
 # We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be
 # included, which contains the CBMC specifications.
-DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
+DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_BUILD -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=
diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k3_native_aarch64/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k3_native_aarch64/Makefile
index d6a579b518..3ad9ce0640 100644
--- a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k3_native_aarch64/Makefile
+++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k3_native_aarch64/Makefile
@@ -12,7 +12,7 @@ PROOF_UID = polyvec_basemul_acc_montgomery_cached_k3_native_aarch64
 
 # We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be
 # included, which contains the CBMC specifications.
-DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/aarch64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
+DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/aarch64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_BUILD -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=
diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k3_native_x86_64/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k3_native_x86_64/Makefile
index c71ad524dc..e4c9707f9b 100644
--- a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k3_native_x86_64/Makefile
+++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k3_native_x86_64/Makefile
@@ -12,7 +12,7 @@ PROOF_UID = polyvec_basemul_acc_montgomery_cached_k3_native_x86_64
 
 # We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be
 # included, which contains the CBMC specifications.
-DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
+DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_BUILD -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=
diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k4_native_aarch64/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k4_native_aarch64/Makefile
index 4ef8df1fb8..a56575e705 100644
--- a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k4_native_aarch64/Makefile
+++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k4_native_aarch64/Makefile
@@ -12,7 +12,7 @@ PROOF_UID = polyvec_basemul_acc_montgomery_cached_k4_native_aarch64
 
 # We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be
 # included, which contains the CBMC specifications.
-DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/aarch64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
+DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/aarch64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_BUILD -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=
diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k4_native_x86_64/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k4_native_x86_64/Makefile
index eea6d0726d..b3928f4acd 100644
--- a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k4_native_x86_64/Makefile
+++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k4_native_x86_64/Makefile
@@ -12,7 +12,7 @@ PROOF_UID = polyvec_basemul_acc_montgomery_cached_k4_native_x86_64
 
 # We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be
 # included, which contains the CBMC specifications.
-DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
+DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_BUILD -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=
diff --git a/proofs/cbmc/tools/aarch64-gcc-as-gcc/gcc b/proofs/cbmc/tools/aarch64-gcc-as-gcc/gcc
new file mode 100755
index 0000000000..34e6ab660f
--- /dev/null
+++ b/proofs/cbmc/tools/aarch64-gcc-as-gcc/gcc
@@ -0,0 +1,5 @@
+#!/usr/bin/env sh
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+exec aarch64-unknown-linux-gnu-gcc "$@"
diff --git a/proofs/cbmc/tools/i686-gcc-as-gcc/gcc b/proofs/cbmc/tools/i686-gcc-as-gcc/gcc
new file mode 100755
index 0000000000..9bbaab4895
--- /dev/null
+++ b/proofs/cbmc/tools/i686-gcc-as-gcc/gcc
@@ -0,0 +1,5 @@
+#!/usr/bin/env sh
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+exec i686-unknown-linux-gnu-gcc "$@"
diff --git a/proofs/cbmc/tools/ppc64le-gcc-as-gcc/gcc b/proofs/cbmc/tools/ppc64le-gcc-as-gcc/gcc
new file mode 100755
index 0000000000..50c9e6fc44
--- /dev/null
+++ b/proofs/cbmc/tools/ppc64le-gcc-as-gcc/gcc
@@ -0,0 +1,5 @@
+#!/usr/bin/env sh
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+exec powerpc64le-unknown-linux-gnu-gcc "$@"
diff --git a/proofs/cbmc/tools/riscv64-gcc-as-gcc/gcc b/proofs/cbmc/tools/riscv64-gcc-as-gcc/gcc
new file mode 100755
index 0000000000..db7856213e
--- /dev/null
+++ b/proofs/cbmc/tools/riscv64-gcc-as-gcc/gcc
@@ -0,0 +1,5 @@
+#!/usr/bin/env sh
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+exec riscv64-unknown-linux-gnu-gcc "$@"
diff --git a/proofs/cbmc/tools/x86_64-gcc-as-gcc/gcc b/proofs/cbmc/tools/x86_64-gcc-as-gcc/gcc
new file mode 100755
index 0000000000..4dd78bf205
--- /dev/null
+++ b/proofs/cbmc/tools/x86_64-gcc-as-gcc/gcc
@@ -0,0 +1,5 @@
+#!/usr/bin/env sh
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+exec x86_64-unknown-linux-gnu-gcc "$@"
diff --git a/scripts/tests b/scripts/tests
index 8eb32f6c05..abe5759f57 100755
--- a/scripts/tests
+++ b/scripts/tests
@@ -414,7 +414,7 @@ class Tests:
         return res
 
     def make_j(self):
-        if self.args.j is None or int(self.args.j) == 1:
+        if self.args.j is None:
             return []
         return [f"-j{self.args.j}"]
 
@@ -930,8 +930,14 @@ class Tests:
                 print(p)
             exit(0)
 
-        def run_cbmc_single_step(mlkem_k, proofs):
+        def cbmc_envvars(mlkem_k):
             envvars = {"MLKEM_K": mlkem_k}
+            if self.args.cbmc_target is not None:
+                envvars["CBMC_TARGET"] = self.args.cbmc_target
+            return envvars
+
+        def run_cbmc_single_step(mlkem_k, proofs):
+            envvars = cbmc_envvars(mlkem_k)
             scheme = SCHEME.from_k(mlkem_k)
             num_proofs = len(proofs)
             for i, func in enumerate(proofs):
@@ -1000,7 +1006,7 @@ class Tests:
             if self.args.single_step:
                 run_cbmc_single_step(mlkem_k, proofs)
                 return
-            envvars = {"MLKEM_K": mlkem_k}
+            envvars = cbmc_envvars(mlkem_k)
             cmd = (
                 [
                     "python3",
@@ -1499,6 +1505,19 @@ def cli():
         default=None,
     )
 
+    cbmc_parser.add_argument(
+        "--cbmc-target",
+        help="CBMC target platform; omit to use the default host model",
+        choices=[
+            "i386-linux",
+            "x86_64-linux",
+            "aarch64-linux",
+            "riscv64-linux",
+            "ppc64le-linux",
+        ],
+        default=None,
+    )
+
     # hol_light arguments
     hol_light_parser = cmd_subparsers.add_parser(
         "hol_light",