diff --git a/.github/actions/config-variations/action.yml b/.github/actions/config-variations/action.yml
index 1c0d9abb5..5799a0f39 100644
--- a/.github/actions/config-variations/action.yml
+++ b/.github/actions/config-variations/action.yml
@@ -7,7 +7,7 @@ inputs:
     description: 'GitHub token'
     required: true
   tests:
-    description: 'List of tests to run (space-separated IDs) or "all" for all tests. Available IDs: pct-enabled, pct-enabled-broken, custom-zeroize, no-asm, custom-randombytes, custom-memcpy, custom-memset, custom-stdlib'
+    description: 'List of tests to run (space-separated IDs) or "all" for all tests. Available IDs: pct-enabled, pct-enabled-broken, custom-zeroize, no-asm, custom-randombytes, custom-memcpy, custom-memset, custom-stdlib, serial-fips202'
     required: false
     default: 'all'
   opt:
@@ -123,3 +123,16 @@ runs:
         acvp: true
         opt: ${{ inputs.opt }}
         examples: false # Some examples use a custom config themselves
+    - name: "Serial FIPS202 (no batched Keccak)"
+      if: ${{ inputs.tests == 'all' || contains(inputs.tests, 'serial-fips202') }}
+      uses: ./.github/actions/multi-functest
+      with:
+        gh_token: ${{ inputs.gh_token }}
+        compile_mode: native
+        cflags: "-std=c11 -D_GNU_SOURCE -DMLD_CONFIG_FILE=\\\\\\\"../../test/serial_fips202_config.h\\\\\\\" -fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all"
+        ldflags: "-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all"
+        func: true
+        kat: true
+        acvp: true
+        opt: ${{ inputs.opt }}
+        examples: false # Some examples use a custom config themselves
diff --git a/BIBLIOGRAPHY.md b/BIBLIOGRAPHY.md
index 86c16884a..9835853d4 100644
--- a/BIBLIOGRAPHY.md
+++ b/BIBLIOGRAPHY.md
@@ -30,6 +30,7 @@ source code and documentation.
   - [test/custom_stdlib_config.h](test/custom_stdlib_config.h)
   - [test/custom_zeroize_config.h](test/custom_zeroize_config.h)
   - [test/no_asm_config.h](test/no_asm_config.h)
+  - [test/serial_fips202_config.h](test/serial_fips202_config.h)
 
 ### `FIPS202`
 
@@ -72,6 +73,7 @@ source code and documentation.
   - [test/custom_stdlib_config.h](test/custom_stdlib_config.h)
   - [test/custom_zeroize_config.h](test/custom_zeroize_config.h)
   - [test/no_asm_config.h](test/no_asm_config.h)
+  - [test/serial_fips202_config.h](test/serial_fips202_config.h)
 
 ### `HYBRID`
 
@@ -310,6 +312,8 @@ source code and documentation.
   - [examples/basic/test_only_rng/notrandombytes.h](examples/basic/test_only_rng/notrandombytes.h)
   - [examples/bring_your_own_fips202/test_only_rng/notrandombytes.c](examples/bring_your_own_fips202/test_only_rng/notrandombytes.c)
   - [examples/bring_your_own_fips202/test_only_rng/notrandombytes.h](examples/bring_your_own_fips202/test_only_rng/notrandombytes.h)
+  - [examples/bring_your_own_fips202_static/test_only_rng/notrandombytes.c](examples/bring_your_own_fips202_static/test_only_rng/notrandombytes.c)
+  - [examples/bring_your_own_fips202_static/test_only_rng/notrandombytes.h](examples/bring_your_own_fips202_static/test_only_rng/notrandombytes.h)
   - [test/notrandombytes/notrandombytes.c](test/notrandombytes/notrandombytes.c)
   - [test/notrandombytes/notrandombytes.h](test/notrandombytes/notrandombytes.h)
 
@@ -323,6 +327,8 @@ source code and documentation.
   - [FIPS202.md](FIPS202.md)
   - [README.md](README.md)
   - [examples/bring_your_own_fips202/README.md](examples/bring_your_own_fips202/README.md)
+  - [examples/bring_your_own_fips202_static/README.md](examples/bring_your_own_fips202_static/README.md)
+  - [examples/bring_your_own_fips202_static/custom_fips202/README.md](examples/bring_your_own_fips202_static/custom_fips202/README.md)
 
 ### `tweetfips`
 
diff --git a/examples/bring_your_own_fips202_static/.gitignore b/examples/bring_your_own_fips202_static/.gitignore
new file mode 100644
index 000000000..834e99720
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/.gitignore
@@ -0,0 +1,4 @@
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+build/
+*.d
diff --git a/examples/bring_your_own_fips202_static/Makefile b/examples/bring_your_own_fips202_static/Makefile
new file mode 100644
index 000000000..da37b9c55
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/Makefile
@@ -0,0 +1,125 @@
+# Copyright (c) The mlkem-native project authors
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+.PHONY: build run clean
+.DEFAULT_GOAL := all
+
+CC  ?= gcc
+
+# Adjust CFLAGS if needed
+CFLAGS := \
+	-Wall \
+	-Wextra \
+	-Werror=unused-result \
+	-Wpedantic \
+	-Werror \
+	-Wmissing-prototypes \
+	-Wshadow \
+	-Wpointer-arith \
+	-Wredundant-decls \
+	-Wconversion \
+	-Wsign-conversion \
+	-Wno-long-long \
+	-Wno-unknown-pragmas \
+	-Wno-unused-command-line-argument \
+	-O3 \
+	-fomit-frame-pointer \
+	-std=c99 \
+	-pedantic \
+	-MMD \
+	$(CFLAGS)
+
+# If you want to use the native backends, the compiler needs to know about
+# the target architecture. Here, we import the default host detection from
+# mldsa-native's tests, but you can write your own or specialize accordingly.
+AUTO ?= 1
+include auto.mk
+
+# The following only concerns the cross-compilation tests.
+# You can likely ignore the following for your application.
+#
+# Append cross-prefix for cross compilation
+# When called from the root Makefile, CROSS_PREFIX has already been added here
+ifeq (,$(findstring $(CROSS_PREFIX),$(CC)))
+CC  := $(CROSS_PREFIX)$(CC)
+endif
+
+# Part A:
+#
+# mldsa-native source and header files
+#
+# In this example, we compile the individual mldsa-native source files directly.
+# Alternatively, you can compile the 'monobuild' source file mldsa_native.c.
+# See examples/monolithic_build for that.
+MLD_SOURCE=$(wildcard \
+	mldsa_native/*.c \
+	mldsa_native/**/*.c \
+	mldsa_native/**/**/*.c \
+	mldsa_native/**/**/**/*.c)
+
+INC=-Imldsa_native/
+
+# Part B:
+#
+# Custom FIPS-202 implementation
+FIPS202_SOURCE=custom_fips202/tiny_sha3/sha3.c
+
+# Part C:
+#
+# Random number generator
+#
+# !!! WARNING !!!
+#
+# The randombytes() implementation used here is for TESTING ONLY.
+# You MUST NOT use this implementation outside of testing.
+#
+# !!! WARNING !!!
+RNG_SOURCE=$(wildcard test_only_rng/*.c)
+
+# Part D:
+#
+# Your application source code
+APP_SOURCE=$(wildcard *.c)
+
+ALL_SOURCE=$(MLD_SOURCE) $(FIPS202_SOURCE) $(RNG_SOURCE) $(APP_SOURCE)
+
+#
+# Configuration adjustments
+#
+
+# Pick prefix
+CFLAGS += -DMLD_CONFIG_NAMESPACE_PREFIX=mldsa
+# Tell mldsa-native to use serial-FIPS202 only
+CFLAGS += -DMLD_CONFIG_SERIAL_FIPS202_ONLY
+# Tell mldsa-native where to find the header for the custom FIPS202
+CFLAGS += -DMLD_CONFIG_FIPS202_CUSTOM_HEADER="\"../custom_fips202/fips202.h\""
+
+BUILD_DIR=build
+BIN=test_binary
+
+BINARY_NAME_FULL_44=$(BUILD_DIR)/$(BIN)44
+BINARY_NAME_FULL_65=$(BUILD_DIR)/$(BIN)65
+BINARY_NAME_FULL_87=$(BUILD_DIR)/$(BIN)87
+BINARIES_FULL=$(BINARY_NAME_FULL_44) $(BINARY_NAME_FULL_65) $(BINARY_NAME_FULL_87)
+
+$(BINARY_NAME_FULL_44): CFLAGS += -DMLD_CONFIG_PARAMETER_SET=44
+$(BINARY_NAME_FULL_65): CFLAGS += -DMLD_CONFIG_PARAMETER_SET=65
+$(BINARY_NAME_FULL_87): CFLAGS += -DMLD_CONFIG_PARAMETER_SET=87
+
+$(BINARIES_FULL): $(ALL_SOURCE)
+	echo "$@"
+	mkdir -p $(BUILD_DIR)
+	$(CC) $(CFLAGS) $(INC) $^ -o $@
+
+all: build
+
+build: $(BINARIES_FULL)
+
+run: $(BINARIES_FULL)
+	$(EXEC_WRAPPER) ./$(BINARY_NAME_FULL_44)
+	$(EXEC_WRAPPER) ./$(BINARY_NAME_FULL_65)
+	$(EXEC_WRAPPER) ./$(BINARY_NAME_FULL_87)
+
+clean:
+	rm -rf $(BUILD_DIR)
diff --git a/examples/bring_your_own_fips202_static/README.md b/examples/bring_your_own_fips202_static/README.md
new file mode 100644
index 000000000..624a0f01a
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/README.md
@@ -0,0 +1,35 @@
+[//]: # (SPDX-License-Identifier: CC-BY-4.0)
+
+# Bring your own FIPS-202 (Static State Variant)
+
+This directory contains a minimal example for how to use mldsa-native with external FIPS-202
+HW/SW-implementations that use a single global state (for example, some hardware accelerators).
+Specifically, this example demonstrates the use of the serial-only FIPS-202 configuration
+`MLD_CONFIG_SERIAL_FIPS202_ONLY`.
+
+**WARNING:** This example is EXPECTED TO PRODUCE INCORRECT RESULTS because ML-DSA requires
+multiple independent FIPS-202 contexts to be active simultaneously. This example demonstrates
+what happens when only a single global state is available.
+
+## Components
+
+An application using mldsa-native with a custom FIPS-202 implementation needs the following:
+
+1. Arithmetic part of the mldsa-native source tree: [`mldsa/src/`](../../mldsa/src)
+2. A secure pseudo random number generator, implementing [`randombytes.h`](../../mldsa/src/randombytes.h).
+3. A custom FIPS-202 with `fips202.h` header compatible with [`mldsa/fips202/fips202.h`](../../mldsa/src/fips202/fips202.h).
+   With `MLD_CONFIG_SERIAL_FIPS202_ONLY`, the FIPS-202x4 parallel API is not used.
+4. The application source code
+
+**WARNING:** The `randombytes()` implementation used here is for TESTING ONLY. You MUST NOT use this implementation
+outside of testing.
+
+## Usage
+
+Build this example with `make build`, run with `make run`.
+
+You should see verification failures, which is the expected behavior demonstrating that a single
+global FIPS-202 state is insufficient for ML-DSA.
+
+<!--- bibliography --->
+[^tiny_sha3]: Markku-Juhani O. Saarinen: tiny_sha3, [https://github.com/mjosaarinen/tiny_sha3](https://github.com/mjosaarinen/tiny_sha3)
diff --git a/examples/bring_your_own_fips202_static/auto.mk b/examples/bring_your_own_fips202_static/auto.mk
new file mode 120000
index 000000000..ce5c161cb
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/auto.mk
@@ -0,0 +1 @@
+../../test/mk/auto.mk
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/custom_fips202/README.md b/examples/bring_your_own_fips202_static/custom_fips202/README.md
new file mode 100644
index 000000000..c507f4baa
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/custom_fips202/README.md
@@ -0,0 +1,43 @@
+<!-- SPDX-License-Identifier: CC-BY-4.0 -->
+
+# Custom FIPS-202 Implementation (Static Global State)
+
+This directory contains a custom FIPS-202 implementation that wraps `tiny_sha3`[^tiny_sha3]
+using a **single global static state** for all operations.
+
+## Purpose
+
+This example demonstrates how mldsa-native can integrate with FIPS-202 implementations
+that maintain a single global state, such as:
+- Hardware accelerators with a single Keccak engine
+- Embedded systems with limited memory
+- Libraries that don't support multiple independent contexts
+
+## How It Works
+
+Instead of storing the Keccak state in each context structure, this implementation:
+
+1. Uses a **static global state** for SHA-3/SHAKE operations
+2. Provides **dummy context structures** that are ignored by the API functions
+3. Includes **state machine assertions** to verify correct API usage
+## Configuration
+
+Enable this mode with:
+```c
+#define MLD_CONFIG_FIPS202_CUSTOM_HEADER "\"fips202.h\""
+#define MLD_CONFIG_SERIAL_FIPS202_ONLY
+```
+
+The `MLD_CONFIG_SERIAL_FIPS202_ONLY` flag tells mldsa-native to avoid
+using the parallel x4 API.
+
+## Files
+
+- `fips202.h` - Custom FIPS-202 wrapper with static global state
+- `tiny_sha3/` - Symlink to the tiny_sha3 implementation
+- `README.md` - This file
+
+[^tiny_sha3]: https://github.com/mjosaarinen/tiny_sha3
+
+<!--- bibliography --->
+[^tiny_sha3]: Markku-Juhani O. Saarinen: tiny_sha3, [https://github.com/mjosaarinen/tiny_sha3](https://github.com/mjosaarinen/tiny_sha3)
diff --git a/examples/bring_your_own_fips202_static/custom_fips202/fips202.h b/examples/bring_your_own_fips202_static/custom_fips202/fips202.h
new file mode 100644
index 000000000..941a1dd10
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/custom_fips202/fips202.h
@@ -0,0 +1,262 @@
+/*
+ * Copyright (c) The mlkem-native project authors
+ * Copyright (c) The mldsa-native project authors
+ * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+ */
+
+/*
+ * This is a shim establishing the FIPS-202 API required by mldsa-native
+ * from the API exposed by tiny_sha3.
+ */
+
+#ifndef FIPS202_H
+#define FIPS202_H
+
+#include <assert.h>
+#include <stddef.h>
+#include <stdint.h>
+#include <string.h>
+
+#include "../custom_fips202/tiny_sha3/sha3.h"
+
+/* We need the MLD_INLINE definition from sys.h */
+#ifndef MLD_INLINE
+#if defined(__GNUC__) || defined(__clang__)
+#define MLD_INLINE __attribute__((always_inline)) static inline
+#else
+#define MLD_INLINE static inline
+#endif
+#endif
+
+#define SHAKE128_RATE 168
+#define SHAKE256_RATE 136
+#define SHA3_256_RATE 136
+#define SHA3_512_RATE 72
+#define SHA3_256_HASHBYTES 32
+#define SHA3_512_HASHBYTES 64
+
+typedef enum
+{
+  FIPS202_STATE_ABSORBING = 1,
+  FIPS202_STATE_SQUEEZING = 2,
+  FIPS202_STATE_FINALIZED = 3,
+  FIPS202_STATE_RESET = 4
+} fips202_state_t;
+
+/* Static state for serial FIPS202 - SHAKE128 */
+static struct
+{
+  fips202_state_t state;
+  sha3_ctx_t ctx;
+} static_shake128_state = {FIPS202_STATE_RESET, {{{0}}, 0, 0, 0}};
+
+/* Static state for serial FIPS202 - SHAKE256 */
+static struct
+{
+  fips202_state_t state;
+  sha3_ctx_t ctx;
+} static_shake256_state = {FIPS202_STATE_RESET, {{{0}}, 0, 0, 0}};
+
+/* Dummy context types - the actual state is static */
+typedef struct
+{
+  int dummy;
+} mld_shake128ctx;
+
+typedef struct
+{
+  int dummy;
+} mld_shake256ctx;
+
+/*************************************************
+ * Name:        mld_shake128_init
+ *
+ * Description: Initializes state for use as SHAKE128 XOF
+ *
+ * Arguments:   - mld_shake128ctx *state: pointer to (uninitialized) state
+ **************************************************/
+#define mld_shake128_init MLD_NAMESPACE(shake128_init)
+static MLD_INLINE void mld_shake128_init(mld_shake128ctx *state)
+{
+  (void)state;
+  assert(static_shake128_state.state == FIPS202_STATE_RESET);
+  shake128_init(&static_shake128_state.ctx);
+  static_shake128_state.state = FIPS202_STATE_ABSORBING;
+}
+
+/*************************************************
+ * Name:        mld_shake128_absorb
+ *
+ * Description: Absorb step of the SHAKE128 XOF. Absorbs arbitrarily many bytes.
+ *              Can be called multiple times to absorb multiple chunks of data.
+ *
+ * Arguments:   - mld_shake128ctx *state: pointer to (initialized) output state
+ *              - const uint8_t *in: pointer to input to be absorbed into s
+ *              - size_t inlen: length of input in bytes
+ **************************************************/
+#define mld_shake128_absorb MLD_NAMESPACE(shake128_absorb)
+static MLD_INLINE void mld_shake128_absorb(mld_shake128ctx *state,
+                                           const uint8_t *in, size_t inlen)
+{
+  (void)state;
+  assert(static_shake128_state.state == FIPS202_STATE_ABSORBING);
+  shake_update(&static_shake128_state.ctx, in, inlen);
+}
+
+/*************************************************
+ * Name:        mld_shake128_finalize
+ *
+ * Description: Concludes the absorb phase of the SHAKE128 XOF.
+ *
+ * Arguments:   - mld_shake128ctx *state: pointer to state
+ **************************************************/
+#define mld_shake128_finalize MLD_NAMESPACE(shake128_finalize)
+static MLD_INLINE void mld_shake128_finalize(mld_shake128ctx *state)
+{
+  (void)state;
+  assert(static_shake128_state.state == FIPS202_STATE_ABSORBING);
+  shake_xof(&static_shake128_state.ctx);
+  static_shake128_state.state = FIPS202_STATE_SQUEEZING;
+}
+
+/*************************************************
+ * Name:        mld_shake128_squeeze
+ *
+ * Description: Squeeze step of SHAKE128 XOF. Squeezes arbitrarily many
+ *              bytes. Can be called multiple times to keep squeezing.
+ *
+ * Arguments:   - uint8_t *out: pointer to output blocks
+ *              - size_t outlen : number of bytes to be squeezed (written to
+ *output)
+ *              - mld_shake128ctx *s: pointer to input/output state
+ **************************************************/
+#define mld_shake128_squeeze MLD_NAMESPACE(shake128_squeeze)
+static MLD_INLINE void mld_shake128_squeeze(uint8_t *out, size_t outlen,
+                                            mld_shake128ctx *state)
+{
+  (void)state;
+  assert(static_shake128_state.state == FIPS202_STATE_SQUEEZING);
+  shake_out(&static_shake128_state.ctx, out, outlen);
+}
+
+/*************************************************
+ * Name:        mld_shake128_release
+ *
+ * Description: Release and securely zero the SHAKE128 state.
+ *
+ * Arguments:   - mld_shake128ctx *state: pointer to state
+ **************************************************/
+#define mld_shake128_release MLD_NAMESPACE(shake128_release)
+static MLD_INLINE void mld_shake128_release(mld_shake128ctx *state)
+{
+  (void)state;
+  static_shake128_state.state = FIPS202_STATE_RESET;
+}
+
+/*************************************************
+ * Name:        mld_shake256_init
+ *
+ * Description: Initializes state for use as SHAKE256 XOF
+ *
+ * Arguments:   - mld_shake256ctx *state: pointer to (uninitialized) state
+ **************************************************/
+#define mld_shake256_init MLD_NAMESPACE(shake256_init)
+static MLD_INLINE void mld_shake256_init(mld_shake256ctx *state)
+{
+  (void)state;
+  assert(static_shake256_state.state == FIPS202_STATE_RESET);
+  shake256_init(&static_shake256_state.ctx);
+  static_shake256_state.state = FIPS202_STATE_ABSORBING;
+}
+
+/*************************************************
+ * Name:        mld_shake256_absorb
+ *
+ * Description: Absorb step of the SHAKE256 XOF. Absorbs arbitrarily many bytes.
+ *              Can be called multiple times to absorb multiple chunks of data.
+ *
+ * Arguments:   - mld_shake256ctx *state: pointer to (initialized) output state
+ *              - const uint8_t *in: pointer to input to be absorbed into s
+ *              - size_t inlen: length of input in bytes
+ **************************************************/
+#define mld_shake256_absorb MLD_NAMESPACE(shake256_absorb)
+static MLD_INLINE void mld_shake256_absorb(mld_shake256ctx *state,
+                                           const uint8_t *in, size_t inlen)
+{
+  (void)state;
+  assert(static_shake256_state.state == FIPS202_STATE_ABSORBING);
+  shake_update(&static_shake256_state.ctx, in, inlen);
+}
+
+/*************************************************
+ * Name:        mld_shake256_finalize
+ *
+ * Description: Concludes the absorb phase of the SHAKE256 XOF.
+ *
+ * Arguments:   - mld_shake256ctx *state: pointer to state
+ **************************************************/
+#define mld_shake256_finalize MLD_NAMESPACE(shake256_finalize)
+static MLD_INLINE void mld_shake256_finalize(mld_shake256ctx *state)
+{
+  (void)state;
+  assert(static_shake256_state.state == FIPS202_STATE_ABSORBING);
+  shake_xof(&static_shake256_state.ctx);
+  static_shake256_state.state = FIPS202_STATE_SQUEEZING;
+}
+
+/*************************************************
+ * Name:        mld_shake256_squeeze
+ *
+ * Description: Squeeze step of SHAKE256 XOF. Squeezes arbitrarily many
+ *              bytes. Can be called multiple times to keep squeezing.
+ *
+ * Arguments:   - uint8_t *out: pointer to output blocks
+ *              - size_t outlen : number of bytes to be squeezed (written to
+ *output)
+ *              - mld_shake256ctx *s: pointer to input/output state
+ **************************************************/
+#define mld_shake256_squeeze MLD_NAMESPACE(shake256_squeeze)
+static MLD_INLINE void mld_shake256_squeeze(uint8_t *out, size_t outlen,
+                                            mld_shake256ctx *state)
+{
+  (void)state;
+  assert(static_shake256_state.state == FIPS202_STATE_SQUEEZING);
+  shake_out(&static_shake256_state.ctx, out, outlen);
+}
+
+/*************************************************
+ * Name:        mld_shake256_release
+ *
+ * Description: Release and securely zero the SHAKE256 state.
+ *
+ * Arguments:   - mld_shake256ctx *state: pointer to state
+ **************************************************/
+#define mld_shake256_release MLD_NAMESPACE(shake256_release)
+static MLD_INLINE void mld_shake256_release(mld_shake256ctx *state)
+{
+  (void)state;
+  static_shake256_state.state = FIPS202_STATE_RESET;
+}
+
+/*************************************************
+ * Name:        mld_shake256
+ *
+ * Description: SHAKE256 XOF with non-incremental API
+ *
+ * Arguments:   - uint8_t *out: pointer to output
+ *              - size_t outlen: requested output length in bytes
+ *              - const uint8_t *in: pointer to input
+ *              - size_t inlen: length of input in bytes
+ **************************************************/
+#define mld_shake256 MLD_NAMESPACE(shake256)
+static MLD_INLINE void mld_shake256(uint8_t *out, size_t outlen,
+                                    const uint8_t *in, size_t inlen)
+{
+  sha3_ctx_t c;
+  shake256_init(&c);
+  shake_update(&c, in, inlen);
+  shake_xof(&c);
+  shake_out(&c, out, outlen);
+}
+
+#endif /* FIPS202_H */
diff --git a/examples/bring_your_own_fips202_static/custom_fips202/tiny_sha3 b/examples/bring_your_own_fips202_static/custom_fips202/tiny_sha3
new file mode 120000
index 000000000..f59919ab1
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/custom_fips202/tiny_sha3
@@ -0,0 +1 @@
+../../bring_your_own_fips202/custom_fips202/tiny_sha3
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/expected_signatures.h b/examples/bring_your_own_fips202_static/expected_signatures.h
new file mode 120000
index 000000000..694d65628
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/expected_signatures.h
@@ -0,0 +1 @@
+../basic/expected_signatures.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/main.c b/examples/bring_your_own_fips202_static/main.c
new file mode 100644
index 000000000..dd9501b7c
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/main.c
@@ -0,0 +1,91 @@
+/*
+ * Copyright (c) The mldsa-native project authors
+ * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+ */
+
+#include <stddef.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <string.h>
+
+/* Import public mldsa-native API
+ *
+ * This requires specifying the parameter set and namespace prefix
+ * used for the build.
+ */
+#define MLD_CONFIG_API_PARAMETER_SET MLD_CONFIG_PARAMETER_SET
+#define MLD_CONFIG_API_NAMESPACE_PREFIX mldsa
+#include <mldsa_native.h>
+#include "expected_signatures.h"
+#include "test_only_rng/notrandombytes.h"
+
+/*
+ * This example demonstrates a static global state FIPS-202 implementation
+ * that works correctly with ML-DSA when FIPS-202 operations are used serially.
+ *
+ * This implementation uses a single global state for SHAKE128 and SHAKE256,
+ * requiring that no interleaved FIPS-202 operations occur.
+ */
+
+#define CHECK(x)                                              \
+  do                                                          \
+  {                                                           \
+    int rc;                                                   \
+    rc = (x);                                                 \
+    if (!rc)                                                  \
+    {                                                         \
+      fprintf(stderr, "ERROR (%s,%d)\n", __FILE__, __LINE__); \
+      return 1;                                               \
+    }                                                         \
+  } while (0)
+
+int main(void)
+{
+  uint8_t pk[CRYPTO_PUBLICKEYBYTES];
+  uint8_t sk[CRYPTO_SECRETKEYBYTES];
+  uint8_t sig[CRYPTO_BYTES];
+  size_t siglen;
+
+  const char *test_msg =
+      "This is a test message for ML-DSA digital signature algorithm!";
+  const char *test_ctx = "test_context_123";
+
+  /* WARNING: Test-only
+   * Normally, you would want to seed a PRNG with trustworthy entropy here. */
+  randombytes_reset();
+
+  printf("Generating keypair ... ");
+
+  CHECK(crypto_sign_keypair(pk, sk) == 0);
+
+  printf("DONE\n");
+  printf("Signing... ");
+
+  CHECK(crypto_sign_signature(sig, &siglen, (const uint8_t *)test_msg,
+                              strlen(test_msg), (const uint8_t *)test_ctx,
+                              strlen(test_ctx), sk) == 0);
+
+  printf("DONE\n");
+  printf("Verifying... ");
+
+  CHECK(crypto_sign_verify(sig, siglen, (const uint8_t *)test_msg,
+                           strlen(test_msg), (const uint8_t *)test_ctx,
+                           strlen(test_ctx), pk) == 0);
+  printf("DONE\n");
+
+#if !defined(MLD_CONFIG_KEYGEN_PCT)
+  /* Check against expected signature to make sure that
+   * we integrated the library correctly */
+  printf("Checking deterministic signature... ");
+  CHECK(siglen == sizeof(expected_signature));
+  CHECK(memcmp(sig, expected_signature, siglen) == 0);
+  printf("DONE\n");
+#else
+  printf(
+      "[WARNING] Skipping KAT test since PCT is enabled and modifies PRNG\n");
+#endif
+
+  printf("OK\n");
+
+  return 0;
+}
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/mldsa_native.h b/examples/bring_your_own_fips202_static/mldsa_native/mldsa_native.h
new file mode 120000
index 000000000..f25191336
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/mldsa_native.h
@@ -0,0 +1 @@
+../../../mldsa/mldsa_native.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/cbmc.h b/examples/bring_your_own_fips202_static/mldsa_native/src/cbmc.h
new file mode 120000
index 000000000..9fd253c4c
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/cbmc.h
@@ -0,0 +1 @@
+../../../../mldsa/src/cbmc.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/common.h b/examples/bring_your_own_fips202_static/mldsa_native/src/common.h
new file mode 120000
index 000000000..7baea8129
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/common.h
@@ -0,0 +1 @@
+../../../../mldsa/src/common.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/config.h b/examples/bring_your_own_fips202_static/mldsa_native/src/config.h
new file mode 120000
index 000000000..e8185dc91
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/config.h
@@ -0,0 +1 @@
+../../../../mldsa/src/config.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/ct.c b/examples/bring_your_own_fips202_static/mldsa_native/src/ct.c
new file mode 120000
index 000000000..3f32692cc
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/ct.c
@@ -0,0 +1 @@
+../../../../mldsa/src/ct.c
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/ct.h b/examples/bring_your_own_fips202_static/mldsa_native/src/ct.h
new file mode 120000
index 000000000..d46bb57d3
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/ct.h
@@ -0,0 +1 @@
+../../../../mldsa/src/ct.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/debug.c b/examples/bring_your_own_fips202_static/mldsa_native/src/debug.c
new file mode 120000
index 000000000..e4b0d5d00
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/debug.c
@@ -0,0 +1 @@
+../../../../mldsa/src/debug.c
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/debug.h b/examples/bring_your_own_fips202_static/mldsa_native/src/debug.h
new file mode 120000
index 000000000..92949bb27
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/debug.h
@@ -0,0 +1 @@
+../../../../mldsa/src/debug.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/fips202 b/examples/bring_your_own_fips202_static/mldsa_native/src/fips202
new file mode 120000
index 000000000..829380ed0
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/fips202
@@ -0,0 +1 @@
+../../../../mldsa/src/fips202
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/native b/examples/bring_your_own_fips202_static/mldsa_native/src/native
new file mode 120000
index 000000000..cf1622b7f
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/native
@@ -0,0 +1 @@
+../../../../mldsa/src/native
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/ntt.c b/examples/bring_your_own_fips202_static/mldsa_native/src/ntt.c
new file mode 120000
index 000000000..a8ab8e18c
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/ntt.c
@@ -0,0 +1 @@
+../../../../mldsa/src/ntt.c
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/ntt.h b/examples/bring_your_own_fips202_static/mldsa_native/src/ntt.h
new file mode 120000
index 000000000..6cf19a6b3
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/ntt.h
@@ -0,0 +1 @@
+../../../../mldsa/src/ntt.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/packing.c b/examples/bring_your_own_fips202_static/mldsa_native/src/packing.c
new file mode 120000
index 000000000..0da6e8062
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/packing.c
@@ -0,0 +1 @@
+../../../../mldsa/src/packing.c
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/packing.h b/examples/bring_your_own_fips202_static/mldsa_native/src/packing.h
new file mode 120000
index 000000000..3dc7c9dae
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/packing.h
@@ -0,0 +1 @@
+../../../../mldsa/src/packing.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/params.h b/examples/bring_your_own_fips202_static/mldsa_native/src/params.h
new file mode 120000
index 000000000..0a530a256
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/params.h
@@ -0,0 +1 @@
+../../../../mldsa/src/params.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/poly.c b/examples/bring_your_own_fips202_static/mldsa_native/src/poly.c
new file mode 120000
index 000000000..2a793df40
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/poly.c
@@ -0,0 +1 @@
+../../../../mldsa/src/poly.c
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/poly.h b/examples/bring_your_own_fips202_static/mldsa_native/src/poly.h
new file mode 120000
index 000000000..0cdab9983
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/poly.h
@@ -0,0 +1 @@
+../../../../mldsa/src/poly.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/poly_kl.c b/examples/bring_your_own_fips202_static/mldsa_native/src/poly_kl.c
new file mode 120000
index 000000000..8a27154af
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/poly_kl.c
@@ -0,0 +1 @@
+../../../../mldsa/src/poly_kl.c
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/poly_kl.h b/examples/bring_your_own_fips202_static/mldsa_native/src/poly_kl.h
new file mode 120000
index 000000000..f981ad481
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/poly_kl.h
@@ -0,0 +1 @@
+../../../../mldsa/src/poly_kl.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/polyvec.c b/examples/bring_your_own_fips202_static/mldsa_native/src/polyvec.c
new file mode 120000
index 000000000..33e86a831
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/polyvec.c
@@ -0,0 +1 @@
+../../../../mldsa/src/polyvec.c
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/polyvec.h b/examples/bring_your_own_fips202_static/mldsa_native/src/polyvec.h
new file mode 120000
index 000000000..417aa2e0c
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/polyvec.h
@@ -0,0 +1 @@
+../../../../mldsa/src/polyvec.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/prehash.c b/examples/bring_your_own_fips202_static/mldsa_native/src/prehash.c
new file mode 120000
index 000000000..b47ab34db
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/prehash.c
@@ -0,0 +1 @@
+../../../../mldsa/src/prehash.c
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/prehash.h b/examples/bring_your_own_fips202_static/mldsa_native/src/prehash.h
new file mode 120000
index 000000000..c7dec4db1
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/prehash.h
@@ -0,0 +1 @@
+../../../../mldsa/src/prehash.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/randombytes.h b/examples/bring_your_own_fips202_static/mldsa_native/src/randombytes.h
new file mode 120000
index 000000000..d372260e5
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/randombytes.h
@@ -0,0 +1 @@
+../../../../mldsa/src/randombytes.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/reduce.h b/examples/bring_your_own_fips202_static/mldsa_native/src/reduce.h
new file mode 120000
index 000000000..e1405ac0a
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/reduce.h
@@ -0,0 +1 @@
+../../../../mldsa/src/reduce.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/rounding.h b/examples/bring_your_own_fips202_static/mldsa_native/src/rounding.h
new file mode 120000
index 000000000..c58bd9fae
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/rounding.h
@@ -0,0 +1 @@
+../../../../mldsa/src/rounding.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/sign.c b/examples/bring_your_own_fips202_static/mldsa_native/src/sign.c
new file mode 120000
index 000000000..fad774fba
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/sign.c
@@ -0,0 +1 @@
+../../../../mldsa/src/sign.c
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/sign.h b/examples/bring_your_own_fips202_static/mldsa_native/src/sign.h
new file mode 120000
index 000000000..2ba1e2a0e
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/sign.h
@@ -0,0 +1 @@
+../../../../mldsa/src/sign.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/symmetric.h b/examples/bring_your_own_fips202_static/mldsa_native/src/symmetric.h
new file mode 120000
index 000000000..eb4af39ca
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/symmetric.h
@@ -0,0 +1 @@
+../../../../mldsa/src/symmetric.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/sys.h b/examples/bring_your_own_fips202_static/mldsa_native/src/sys.h
new file mode 120000
index 000000000..7322c1c94
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/sys.h
@@ -0,0 +1 @@
+../../../../mldsa/src/sys.h
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/mldsa_native/src/zetas.inc b/examples/bring_your_own_fips202_static/mldsa_native/src/zetas.inc
new file mode 120000
index 000000000..b9361143a
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/mldsa_native/src/zetas.inc
@@ -0,0 +1 @@
+../../../../mldsa/src/zetas.inc
\ No newline at end of file
diff --git a/examples/bring_your_own_fips202_static/test_only_rng/notrandombytes.c b/examples/bring_your_own_fips202_static/test_only_rng/notrandombytes.c
new file mode 100644
index 000000000..c069a6a26
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/test_only_rng/notrandombytes.c
@@ -0,0 +1,113 @@
+/*
+ * Copyright (c) The mlkem-native project authors
+ * Copyright (c) The mldsa-native project authors
+ * SPDX-License-Identifier: LicenseRef-PD-hp OR CC0-1.0 OR 0BSD OR MIT-0 OR MIT
+ */
+
+/* References
+ * ==========
+ *
+ * - [surf]
+ *   SURF: Simple Unpredictable Random Function
+ *   Daniel J. Bernstein
+ *   https://cr.yp.to/papers.html#surf
+ */
+
+/* Based on @[surf]. */
+
+/**
+ * WARNING
+ *
+ * The randombytes() implementation in this file is for TESTING ONLY.
+ * You MUST NOT use this implementation outside of testing.
+ *
+ */
+
+#include <stdint.h>
+#include <string.h>
+
+#include "notrandombytes.h"
+
+static uint32_t seed[32] = {3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5, 8, 9, 7, 9, 3,
+                            2, 3, 8, 4, 6, 2, 6, 4, 3, 3, 8, 3, 2, 7, 9, 5};
+static uint32_t in[12];
+static uint32_t out[8];
+static int32_t outleft = 0;
+
+void randombytes_reset(void)
+{
+  memset(in, 0, sizeof(in));
+  memset(out, 0, sizeof(out));
+  outleft = 0;
+}
+
+#define ROTATE(x, b) (((x) << (b)) | ((x) >> (32 - (b))))
+#define MUSH(i, b) x = t[i] += (((x ^ seed[i]) + sum) ^ ROTATE(x, b));
+
+static void surf(void)
+{
+  uint32_t t[12];
+  uint32_t x;
+  uint32_t sum = 0;
+  int32_t r;
+  int32_t i;
+  int32_t loop;
+
+  for (i = 0; i < 12; ++i)
+  {
+    t[i] = in[i] ^ seed[12 + i];
+  }
+  for (i = 0; i < 8; ++i)
+  {
+    out[i] = seed[24 + i];
+  }
+  x = t[11];
+  for (loop = 0; loop < 2; ++loop)
+  {
+    for (r = 0; r < 16; ++r)
+    {
+      sum += 0x9e3779b9;
+      MUSH(0, 5)
+      MUSH(1, 7)
+      MUSH(2, 9)
+      MUSH(3, 13)
+      MUSH(4, 5)
+      MUSH(5, 7)
+      MUSH(6, 9)
+      MUSH(7, 13)
+      MUSH(8, 5)
+      MUSH(9, 7)
+      MUSH(10, 9)
+      MUSH(11, 13)
+    }
+    for (i = 0; i < 8; ++i)
+    {
+      out[i] ^= t[i + 4];
+    }
+  }
+}
+
+void randombytes(uint8_t *buf, size_t n)
+{
+  while (n > 0)
+  {
+    if (!outleft)
+    {
+      if (!++in[0])
+      {
+        if (!++in[1])
+        {
+          if (!++in[2])
+          {
+            ++in[3];
+          }
+        }
+      }
+      surf();
+      outleft = 8;
+    }
+    *buf = (uint8_t)out[--outleft];
+    ++buf;
+    --n;
+  }
+}
diff --git a/examples/bring_your_own_fips202_static/test_only_rng/notrandombytes.h b/examples/bring_your_own_fips202_static/test_only_rng/notrandombytes.h
new file mode 100644
index 000000000..b2a464372
--- /dev/null
+++ b/examples/bring_your_own_fips202_static/test_only_rng/notrandombytes.h
@@ -0,0 +1,35 @@
+/*
+ * Copyright (c) The mlkem-native project authors
+ * Copyright (c) The mldsa-native project authors
+ * SPDX-License-Identifier: LicenseRef-PD-hp OR CC0-1.0 OR 0BSD OR MIT-0 OR MI
+ */
+
+/* References
+ * ==========
+ *
+ * - [surf]
+ *   SURF: Simple Unpredictable Random Function
+ *   Daniel J. Bernstein
+ *   https://cr.yp.to/papers.html#surf
+ */
+
+/* Based on @[surf]. */
+
+#ifndef NOTRANDOMBYTES_H
+#define NOTRANDOMBYTES_H
+
+#include <stdint.h>
+#include <stdlib.h>
+
+/**
+ * WARNING
+ *
+ * The randombytes() implementation in this file is for TESTING ONLY.
+ * You MUST NOT use this implementation outside of testing.
+ *
+ */
+
+void randombytes_reset(void);
+void randombytes(uint8_t *buf, size_t n);
+
+#endif /* !NOTRANDOMBYTES_H */
diff --git a/examples/monolithic_build/config_44.h b/examples/monolithic_build/config_44.h
index 2509a9e92..4d5762aed 100644
--- a/examples/monolithic_build/config_44.h
+++ b/examples/monolithic_build/config_44.h
@@ -426,7 +426,28 @@
  *****************************************************************************/
 /* #define MLD_CONFIG_NO_ASM_VALUE_BARRIER */
 
-
+/******************************************************************************
+ * Name:        MLD_CONFIG_SERIAL_FIPS202_ONLY
+ *
+ * Description: Set this to use a FIPS202 implementation with global state
+ *              that supports only one active Keccak computation at a time
+ *              (e.g. some hardware accelerators).
+ *
+ *              If this option is set, ML-DSA will use FIPS202 operations
+ *              serially, ensuring that only one SHAKE context is active
+ *              at any given time.
+ *
+ *              This allows offloading Keccak computations to a hardware
+ *              accelerator that holds only a single Keccak state locally,
+ *              rather than requiring support for multiple concurrent
+ *              Keccak states.
+ *
+ *              NOTE: Depending on the target CPU, this may reduce
+ *              performance when using software FIPS202 implementations.
+ *              Only enable this when you have to.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
 /*************************  Config internals  ********************************/
 
diff --git a/examples/monolithic_build/config_65.h b/examples/monolithic_build/config_65.h
index 29286f7e8..bbe5fc8bc 100644
--- a/examples/monolithic_build/config_65.h
+++ b/examples/monolithic_build/config_65.h
@@ -426,7 +426,28 @@
  *****************************************************************************/
 /* #define MLD_CONFIG_NO_ASM_VALUE_BARRIER */
 
-
+/******************************************************************************
+ * Name:        MLD_CONFIG_SERIAL_FIPS202_ONLY
+ *
+ * Description: Set this to use a FIPS202 implementation with global state
+ *              that supports only one active Keccak computation at a time
+ *              (e.g. some hardware accelerators).
+ *
+ *              If this option is set, ML-DSA will use FIPS202 operations
+ *              serially, ensuring that only one SHAKE context is active
+ *              at any given time.
+ *
+ *              This allows offloading Keccak computations to a hardware
+ *              accelerator that holds only a single Keccak state locally,
+ *              rather than requiring support for multiple concurrent
+ *              Keccak states.
+ *
+ *              NOTE: Depending on the target CPU, this may reduce
+ *              performance when using software FIPS202 implementations.
+ *              Only enable this when you have to.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
 /*************************  Config internals  ********************************/
 
diff --git a/examples/monolithic_build/config_87.h b/examples/monolithic_build/config_87.h
index 65019bdbf..2c67fac8a 100644
--- a/examples/monolithic_build/config_87.h
+++ b/examples/monolithic_build/config_87.h
@@ -426,7 +426,28 @@
  *****************************************************************************/
 /* #define MLD_CONFIG_NO_ASM_VALUE_BARRIER */
 
-
+/******************************************************************************
+ * Name:        MLD_CONFIG_SERIAL_FIPS202_ONLY
+ *
+ * Description: Set this to use a FIPS202 implementation with global state
+ *              that supports only one active Keccak computation at a time
+ *              (e.g. some hardware accelerators).
+ *
+ *              If this option is set, ML-DSA will use FIPS202 operations
+ *              serially, ensuring that only one SHAKE context is active
+ *              at any given time.
+ *
+ *              This allows offloading Keccak computations to a hardware
+ *              accelerator that holds only a single Keccak state locally,
+ *              rather than requiring support for multiple concurrent
+ *              Keccak states.
+ *
+ *              NOTE: Depending on the target CPU, this may reduce
+ *              performance when using software FIPS202 implementations.
+ *              Only enable this when you have to.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
 /*************************  Config internals  ********************************/
 
diff --git a/examples/monolithic_build_multilevel/multilevel_config.h b/examples/monolithic_build_multilevel/multilevel_config.h
index e9538a68b..1c41716b3 100644
--- a/examples/monolithic_build_multilevel/multilevel_config.h
+++ b/examples/monolithic_build_multilevel/multilevel_config.h
@@ -427,7 +427,28 @@
  *****************************************************************************/
 /* #define MLD_CONFIG_NO_ASM_VALUE_BARRIER */
 
-
+/******************************************************************************
+ * Name:        MLD_CONFIG_SERIAL_FIPS202_ONLY
+ *
+ * Description: Set this to use a FIPS202 implementation with global state
+ *              that supports only one active Keccak computation at a time
+ *              (e.g. some hardware accelerators).
+ *
+ *              If this option is set, ML-DSA will use FIPS202 operations
+ *              serially, ensuring that only one SHAKE context is active
+ *              at any given time.
+ *
+ *              This allows offloading Keccak computations to a hardware
+ *              accelerator that holds only a single Keccak state locally,
+ *              rather than requiring support for multiple concurrent
+ *              Keccak states.
+ *
+ *              NOTE: Depending on the target CPU, this may reduce
+ *              performance when using software FIPS202 implementations.
+ *              Only enable this when you have to.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
 /*************************  Config internals  ********************************/
 
diff --git a/integration/liboqs/config_aarch64.h b/integration/liboqs/config_aarch64.h
index 8068275a2..43b6774b9 100644
--- a/integration/liboqs/config_aarch64.h
+++ b/integration/liboqs/config_aarch64.h
@@ -272,6 +272,29 @@ static MLD_INLINE void mld_randombytes(uint8_t *ptr, size_t len)
 #define MLD_CONFIG_EXTERNAL_API_QUALIFIER OQS_API
 #endif /* !__ASSEMBLER__ */
 
+/******************************************************************************
+ * Name:        MLD_CONFIG_SERIAL_FIPS202_ONLY
+ *
+ * Description: Set this to use a FIPS202 implementation with global state
+ *              that supports only one active Keccak computation at a time
+ *              (e.g. some hardware accelerators).
+ *
+ *              If this option is set, ML-DSA will use FIPS202 operations
+ *              serially, ensuring that only one SHAKE context is active
+ *              at any given time.
+ *
+ *              This allows offloading Keccak computations to a hardware
+ *              accelerator that holds only a single Keccak state locally,
+ *              rather than requiring support for multiple concurrent
+ *              Keccak states.
+ *
+ *              NOTE: Depending on the target CPU, this may reduce
+ *              performance when using software FIPS202 implementations.
+ *              Only enable this when you have to.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_SERIAL_FIPS202_ONLY */
+
 /*************************  Config internals  ********************************/
 
 /* Default namespace
diff --git a/integration/liboqs/config_c.h b/integration/liboqs/config_c.h
index 1bab0533f..f32d33d9f 100644
--- a/integration/liboqs/config_c.h
+++ b/integration/liboqs/config_c.h
@@ -276,6 +276,29 @@ static MLD_INLINE void mld_randombytes(uint8_t *ptr, size_t len)
 #define MLD_CONFIG_EXTERNAL_API_QUALIFIER OQS_API
 #endif /* !__ASSEMBLER__ */
 
+/******************************************************************************
+ * Name:        MLD_CONFIG_SERIAL_FIPS202_ONLY
+ *
+ * Description: Set this to use a FIPS202 implementation with global state
+ *              that supports only one active Keccak computation at a time
+ *              (e.g. some hardware accelerators).
+ *
+ *              If this option is set, ML-DSA will use FIPS202 operations
+ *              serially, ensuring that only one SHAKE context is active
+ *              at any given time.
+ *
+ *              This allows offloading Keccak computations to a hardware
+ *              accelerator that holds only a single Keccak state locally,
+ *              rather than requiring support for multiple concurrent
+ *              Keccak states.
+ *
+ *              NOTE: Depending on the target CPU, this may reduce
+ *              performance when using software FIPS202 implementations.
+ *              Only enable this when you have to.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_SERIAL_FIPS202_ONLY */
+
 /*************************  Config internals  ********************************/
 
 /* Default namespace
diff --git a/integration/liboqs/config_x86_64.h b/integration/liboqs/config_x86_64.h
index 146c8dba1..e13a0ab33 100644
--- a/integration/liboqs/config_x86_64.h
+++ b/integration/liboqs/config_x86_64.h
@@ -274,6 +274,29 @@ static MLD_INLINE void mld_randombytes(uint8_t *ptr, size_t len)
  *****************************************************************************/
 /* #define MLD_CONFIG_NO_ASM_VALUE_BARRIER */
 
+/******************************************************************************
+ * Name:        MLD_CONFIG_SERIAL_FIPS202_ONLY
+ *
+ * Description: Set this to use a FIPS202 implementation with global state
+ *              that supports only one active Keccak computation at a time
+ *              (e.g. some hardware accelerators).
+ *
+ *              If this option is set, ML-DSA will use FIPS202 operations
+ *              serially, ensuring that only one SHAKE context is active
+ *              at any given time.
+ *
+ *              This allows offloading Keccak computations to a hardware
+ *              accelerator that holds only a single Keccak state locally,
+ *              rather than requiring support for multiple concurrent
+ *              Keccak states.
+ *
+ *              NOTE: Depending on the target CPU, this may reduce
+ *              performance when using software FIPS202 implementations.
+ *              Only enable this when you have to.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_SERIAL_FIPS202_ONLY */
+
 /*************************  Config internals  ********************************/
 
 /* Default namespace
diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c
index c34076985..06afc8ffb 100644
--- a/mldsa/mldsa_native.c
+++ b/mldsa/mldsa_native.c
@@ -231,6 +231,7 @@
 #undef mld_poly_chknorm
 #undef mld_poly_decompose
 #undef mld_poly_make_hint
+#undef mld_poly_uniform_eta
 #undef mld_poly_uniform_eta_4x
 #undef mld_poly_uniform_gamma1
 #undef mld_poly_uniform_gamma1_4x
@@ -246,6 +247,7 @@
 #undef mld_polyvec_matrix_pointwise_montgomery
 #undef mld_polyveck
 #undef mld_polyveck_add
+#undef mld_polyveck_add_error
 #undef mld_polyveck_caddq
 #undef mld_polyveck_chknorm
 #undef mld_polyveck_decompose
diff --git a/mldsa/src/config.h b/mldsa/src/config.h
index 588fa043a..f78577fbd 100644
--- a/mldsa/src/config.h
+++ b/mldsa/src/config.h
@@ -412,7 +412,28 @@
  *****************************************************************************/
 /* #define MLD_CONFIG_NO_ASM_VALUE_BARRIER */
 
-
+/******************************************************************************
+ * Name:        MLD_CONFIG_SERIAL_FIPS202_ONLY
+ *
+ * Description: Set this to use a FIPS202 implementation with global state
+ *              that supports only one active Keccak computation at a time
+ *              (e.g. some hardware accelerators).
+ *
+ *              If this option is set, ML-DSA will use FIPS202 operations
+ *              serially, ensuring that only one SHAKE context is active
+ *              at any given time.
+ *
+ *              This allows offloading Keccak computations to a hardware
+ *              accelerator that holds only a single Keccak state locally,
+ *              rather than requiring support for multiple concurrent
+ *              Keccak states.
+ *
+ *              NOTE: Depending on the target CPU, this may reduce
+ *              performance when using software FIPS202 implementations.
+ *              Only enable this when you have to.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
 /*************************  Config internals  ********************************/
 
diff --git a/mldsa/src/poly.c b/mldsa/src/poly.c
index d07e90e8e..0e21734cb 100644
--- a/mldsa/src/poly.c
+++ b/mldsa/src/poly.c
@@ -352,6 +352,7 @@ void mld_poly_uniform(mld_poly *a, const uint8_t seed[MLDSA_SEEDBYTES + 2])
   mld_zeroize(buf, sizeof(buf));
 }
 
+#if !defined(MLD_CONFIG_SERIAL_FIPS202_ONLY)
 MLD_INTERNAL_API
 void mld_poly_uniform_4x(mld_poly *vec0, mld_poly *vec1, mld_poly *vec2,
                          mld_poly *vec3,
@@ -416,6 +417,7 @@ void mld_poly_uniform_4x(mld_poly *vec0, mld_poly *vec1, mld_poly *vec2,
   mld_zeroize(buf, sizeof(buf));
 }
 
+#endif /* !MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
 MLD_INTERNAL_API
 void mld_polyt1_pack(uint8_t *r, const mld_poly *a)
diff --git a/mldsa/src/poly_kl.c b/mldsa/src/poly_kl.c
index 2fb191ef3..3c45fd8fe 100644
--- a/mldsa/src/poly_kl.c
+++ b/mldsa/src/poly_kl.c
@@ -324,6 +324,7 @@ __contract__(
   return ctr;
 }
 
+#if !defined(MLD_CONFIG_SERIAL_FIPS202_ONLY)
 MLD_INTERNAL_API
 void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2,
                              mld_poly *r3, const uint8_t seed[MLDSA_CRHBYTES],
@@ -407,11 +408,68 @@ void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2,
   mld_zeroize(buf, sizeof(buf));
   mld_zeroize(extseed, sizeof(extseed));
 }
+#else  /* !MLD_CONFIG_SERIAL_FIPS202_ONLY */
+
+MLD_INTERNAL_API
+void mld_poly_uniform_eta(mld_poly *r, const uint8_t seed[MLDSA_CRHBYTES],
+                          uint8_t nonce)
+{
+  /* Temporary buffer for XOF output before rejection sampling */
+  MLD_ALIGN uint8_t buf[POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES];
+  MLD_ALIGN uint8_t extseed[MLDSA_CRHBYTES + 2];
+
+  /* Tracks the number of coefficients we have already sampled */
+  unsigned ctr;
+  mld_xof256_ctx state;
+  unsigned buflen;
+
+  mld_memcpy(extseed, seed, MLDSA_CRHBYTES);
+  extseed[MLDSA_CRHBYTES] = nonce;
+  extseed[MLDSA_CRHBYTES + 1] = 0;
+
+  mld_xof256_init(&state);
+  mld_xof256_absorb_once(&state, extseed, MLDSA_CRHBYTES + 2);
+
+  /*
+   * Initially, squeeze heuristic number of POLY_UNIFORM_ETA_NBLOCKS.
+   * This should generate the coefficients with high probability.
+   */
+  mld_xof256_squeezeblocks(buf, POLY_UNIFORM_ETA_NBLOCKS, &state);
+  buflen = POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES;
+
+  ctr = mld_rej_eta(r->coeffs, MLDSA_N, 0, buf, buflen);
+
+  /*
+   * So long as not all entries have been generated, squeeze
+   * one more block a time until we're done.
+   */
+  buflen = STREAM256_BLOCKBYTES;
+  while (ctr < MLDSA_N)
+  __loop__(
+    assigns(ctr, memory_slice(&state, sizeof(mld_xof256_ctx)),
+      memory_slice(buf, STREAM256_BLOCKBYTES), memory_slice(r, sizeof(mld_poly)))
+    invariant(ctr <= MLDSA_N)
+    invariant(state.pos <= SHAKE256_RATE)
+    invariant(array_abs_bound(r->coeffs, 0, ctr, MLDSA_ETA + 1)))
+  {
+    mld_xof256_squeezeblocks(buf, 1, &state);
+    ctr = mld_rej_eta(r->coeffs, MLDSA_N, ctr, buf, buflen);
+  }
+
+  mld_xof256_release(&state);
+
+  mld_assert_abs_bound(r->coeffs, MLDSA_N, MLDSA_ETA + 1);
+
+  /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
+  mld_zeroize(buf, sizeof(buf));
+  mld_zeroize(extseed, sizeof(extseed));
+}
+#endif /* MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
 #define POLY_UNIFORM_GAMMA1_NBLOCKS \
   ((MLDSA_POLYZ_PACKEDBYTES + STREAM256_BLOCKBYTES - 1) / STREAM256_BLOCKBYTES)
 
-#if MLD_CONFIG_PARAMETER_SET == 65
+#if MLD_CONFIG_PARAMETER_SET == 65 || defined(MLD_CONFIG_SERIAL_FIPS202_ONLY)
 MLD_INTERNAL_API
 void mld_poly_uniform_gamma1(mld_poly *a, const uint8_t seed[MLDSA_CRHBYTES],
                              uint16_t nonce)
@@ -438,8 +496,10 @@ void mld_poly_uniform_gamma1(mld_poly *a, const uint8_t seed[MLDSA_CRHBYTES],
   mld_zeroize(buf, sizeof(buf));
   mld_zeroize(extseed, sizeof(extseed));
 }
-#endif /* MLD_CONFIG_PARAMETER_SET == 65 */
+#endif /* MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_SERIAL_FIPS202_ONLY */
+
 
+#if !defined(MLD_CONFIG_SERIAL_FIPS202_ONLY)
 MLD_INTERNAL_API
 void mld_poly_uniform_gamma1_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2,
                                 mld_poly *r3,
@@ -488,6 +548,7 @@ void mld_poly_uniform_gamma1_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2,
   mld_zeroize(buf, sizeof(buf));
   mld_zeroize(extseed, sizeof(extseed));
 }
+#endif /* !MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
 MLD_INTERNAL_API
 void mld_poly_challenge(mld_poly *c, const uint8_t seed[MLDSA_CTILDEBYTES])
diff --git a/mldsa/src/poly_kl.h b/mldsa/src/poly_kl.h
index 6bc25a0fe..86e15eda3 100644
--- a/mldsa/src/poly_kl.h
+++ b/mldsa/src/poly_kl.h
@@ -161,7 +161,32 @@ __contract__(
   ensures(array_abs_bound(r3->coeffs, 0, MLDSA_N, MLDSA_ETA + 1))
 );
 
-#if MLD_CONFIG_PARAMETER_SET == 65
+#if defined(MLD_CONFIG_SERIAL_FIPS202_ONLY)
+#define mld_poly_uniform_eta MLD_NAMESPACE_KL(poly_uniform_eta)
+/*************************************************
+ * Name:        mld_poly_uniform_eta
+ *
+ * Description: Sample polynomial with uniformly random coefficients
+ *              in [-MLDSA_ETA,MLDSA_ETA] by performing rejection sampling on
+ *              the output stream from SHAKE256(seed|nonce)
+ *
+ * Arguments:   - mld_poly *r: pointer to output polynomial
+ *              - const uint8_t seed[]: byte array with seed of length
+ *                MLDSA_CRHBYTES
+ *              - uint8_t nonce: nonce
+ **************************************************/
+MLD_INTERNAL_API
+void mld_poly_uniform_eta(mld_poly *r, const uint8_t seed[MLDSA_CRHBYTES],
+                          uint8_t nonce)
+__contract__(
+  requires(memory_no_alias(r, sizeof(mld_poly)))
+  requires(memory_no_alias(seed, MLDSA_CRHBYTES))
+  assigns(memory_slice(r, sizeof(mld_poly)))
+  ensures(array_abs_bound(r->coeffs, 0, MLDSA_N, MLDSA_ETA + 1))
+);
+#endif /* MLD_CONFIG_SERIAL_FIPS202_ONLY */
+
+#if MLD_CONFIG_PARAMETER_SET == 65 || defined(MLD_CONFIG_SERIAL_FIPS202_ONLY)
 #define mld_poly_uniform_gamma1 MLD_NAMESPACE_KL(poly_uniform_gamma1)
 /*************************************************
  * Name:        mld_poly_uniform_gamma1
@@ -184,7 +209,7 @@ __contract__(
   assigns(memory_slice(a, sizeof(mld_poly)))
   ensures(array_bound(a->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
 );
-#endif /* MLD_CONFIG_PARAMETER_SET == 65 */
+#endif /* MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
 #define mld_poly_uniform_gamma1_4x MLD_NAMESPACE_KL(poly_uniform_gamma1_4x)
 /*************************************************
diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c
index 8469c8654..c5ca3d977 100644
--- a/mldsa/src/polyvec.c
+++ b/mldsa/src/polyvec.c
@@ -45,20 +45,14 @@ void mld_polyvec_matrix_expand(mld_polyvecl mat[MLDSA_K],
    * of the same parent object.
    */
 
-  MLD_ALIGN uint8_t seed_ext[4][MLD_ALIGN_UP(MLDSA_SEEDBYTES + 2)];
+  MLD_ALIGN uint8_t single_seed[MLD_ALIGN_UP(MLDSA_SEEDBYTES + 2)];
 
-  for (j = 0; j < 4; j++)
-  __loop__(
-    assigns(j, object_whole(seed_ext))
-    invariant(j <= 4)
-  )
-  {
-    mld_memcpy(seed_ext[j], rho, MLDSA_SEEDBYTES);
-  }
+#if !defined(MLD_CONFIG_SERIAL_FIPS202_ONLY)
+  MLD_ALIGN uint8_t batched_seeds[4][MLD_ALIGN_UP(MLDSA_SEEDBYTES + 2)];
   /* Sample 4 matrix entries a time. */
   for (i = 0; i < (MLDSA_K * MLDSA_L / 4) * 4; i += 4)
   __loop__(
-    assigns(i, j, object_whole(seed_ext), memory_slice(mat, MLDSA_K * sizeof(mld_polyvecl)))
+    assigns(i, j, object_whole(batched_seeds), memory_slice(mat, MLDSA_K * sizeof(mld_polyvecl)))
     invariant(i <= (MLDSA_K * MLDSA_L / 4) * 4 && i % 4 == 0)
     /* vectors 0 .. i / MLDSA_L are completely sampled */
     invariant(forall(k1, 0, i / MLDSA_L, forall(l1, 0, MLDSA_L,
@@ -70,28 +64,38 @@ void mld_polyvec_matrix_expand(mld_polyvecl mat[MLDSA_K],
   {
     for (j = 0; j < 4; j++)
     __loop__(
-      assigns(j, object_whole(seed_ext))
+      assigns(j, object_whole(batched_seeds))
       invariant(j <= 4)
     )
     {
       uint8_t x = (uint8_t)((i + j) / MLDSA_L);
       uint8_t y = (uint8_t)((i + j) % MLDSA_L);
 
-      seed_ext[j][MLDSA_SEEDBYTES + 0] = y;
-      seed_ext[j][MLDSA_SEEDBYTES + 1] = x;
+      mld_memcpy(batched_seeds[j], rho, MLDSA_SEEDBYTES);
+      batched_seeds[j][MLDSA_SEEDBYTES + 0] = y;
+      batched_seeds[j][MLDSA_SEEDBYTES + 1] = x;
     }
 
     mld_poly_uniform_4x(&mat[i / MLDSA_L].vec[i % MLDSA_L],
                         &mat[(i + 1) / MLDSA_L].vec[(i + 1) % MLDSA_L],
                         &mat[(i + 2) / MLDSA_L].vec[(i + 2) % MLDSA_L],
                         &mat[(i + 3) / MLDSA_L].vec[(i + 3) % MLDSA_L],
-                        seed_ext);
+                        batched_seeds);
   }
 
+  /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
+  mld_zeroize(batched_seeds, sizeof(batched_seeds));
+
+#else  /* !MLD_CONFIG_SERIAL_FIPS202_ONLY */
+  i = 0;
+#endif /* MLD_CONFIG_SERIAL_FIPS202_ONLY */
+
+  mld_memcpy(single_seed, rho, MLDSA_SEEDBYTES);
+
   /* For MLDSA_K=6, MLDSA_L=5, process the last two entries individually */
   while (i < MLDSA_K * MLDSA_L)
   __loop__(
-    assigns(i, object_whole(seed_ext), memory_slice(mat, MLDSA_K * sizeof(mld_polyvecl)))
+    assigns(i, object_whole(single_seed), memory_slice(mat, MLDSA_K * sizeof(mld_polyvecl)))
     invariant(i <= MLDSA_K * MLDSA_L)
     /* vectors 0 .. i / MLDSA_L are completely sampled */
     invariant(forall(k1, 0, i / MLDSA_L, forall(l1, 0, MLDSA_L,
@@ -105,17 +109,20 @@ void mld_polyvec_matrix_expand(mld_polyvecl mat[MLDSA_K],
     uint8_t y = (uint8_t)(i % MLDSA_L);
     mld_poly *this_poly = &mat[i / MLDSA_L].vec[i % MLDSA_L];
 
-    seed_ext[0][MLDSA_SEEDBYTES + 0] = y;
-    seed_ext[0][MLDSA_SEEDBYTES + 1] = x;
+    single_seed[MLDSA_SEEDBYTES + 0] = y;
+    single_seed[MLDSA_SEEDBYTES + 1] = x;
 
-    mld_poly_uniform(this_poly, seed_ext[0]);
+    mld_poly_uniform(this_poly, single_seed);
     i++;
   }
 
   /*
    * The public matrix is generated in NTT domain. If the native backend
-   * uses a custom order in NTT domain, permute A accordingly.
+   * uses a custom order in NTT domain, permute A accordingly. This does
+   * not affect the bounds on the coefficients, so we ignore this for CBMC
+   * to simplify proof.
    */
+#ifndef CBMC
   for (i = 0; i < MLDSA_K; i++)
   {
     for (j = 0; j < MLDSA_L; j++)
@@ -123,9 +130,10 @@ void mld_polyvec_matrix_expand(mld_polyvecl mat[MLDSA_K],
       mld_poly_permute_bitrev_to_custom(mat[i].vec[j].coeffs);
     }
   }
+#endif /* !CBMC */
 
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
-  mld_zeroize(seed_ext, sizeof(seed_ext));
+  mld_zeroize(single_seed, sizeof(single_seed));
 }
 
 MLD_INTERNAL_API
@@ -158,10 +166,20 @@ void mld_polyvecl_uniform_gamma1(mld_polyvecl *v,
                                  const uint8_t seed[MLDSA_CRHBYTES],
                                  uint16_t nonce)
 {
+#if defined(MLD_CONFIG_SERIAL_FIPS202_ONLY)
+  int i;
+#endif
+
   /* Safety: nonce is at most ((UINT16_MAX - MLDSA_L) / MLDSA_L), and, hence,
    * this cast is safe. See NONCE_UB comment in sign.c. */
   nonce = (uint16_t)(MLDSA_L * nonce);
   /* Now, nonce <= UINT16_MAX - (MLDSA_L - 1), so the casts below are safe. */
+#if defined(MLD_CONFIG_SERIAL_FIPS202_ONLY)
+  for (i = 0; i < MLDSA_L; i++)
+  {
+    mld_poly_uniform_gamma1(&v->vec[i], seed, (uint16_t)(nonce + i));
+  }
+#else /* MLD_CONFIG_SERIAL_FIPS202_ONLY */
 #if MLDSA_L == 4
   mld_poly_uniform_gamma1_4x(&v->vec[0], &v->vec[1], &v->vec[2], &v->vec[3],
                              seed, nonce, (uint16_t)(nonce + 1),
@@ -180,6 +198,7 @@ void mld_polyvecl_uniform_gamma1(mld_polyvecl *v,
                              seed, (uint16_t)(nonce + 3), (uint16_t)(nonce + 4),
                              (uint16_t)(nonce + 5), (uint16_t)(nonce + 6));
 #endif /* MLDSA_L == 7 */
+#endif /* !MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
   mld_assert_bound_2d(v->vec, MLDSA_L, MLDSA_N, -(MLDSA_GAMMA1 - 1),
                       MLDSA_GAMMA1 + 1);
@@ -219,7 +238,6 @@ void mld_polyvecl_add(mld_polyvecl *u, const mld_polyvecl *v)
     invariant(i <= MLDSA_L)
     invariant(forall(k0, i, MLDSA_L,
               forall(k1, 0, MLDSA_N, u->vec[k0].coeffs[k1] == loop_entry(*u).vec[k0].coeffs[k1])))
-    invariant(forall(k4, 0, i, forall(k5, 0, MLDSA_N, u->vec[k4].coeffs[k5] == loop_entry(*u).vec[k4].coeffs[k5] + v->vec[k4].coeffs[k5])))
     invariant(forall(k6, 0, i, array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX)))
   )
   {
@@ -287,12 +305,13 @@ void mld_polyvecl_pointwise_poly_montgomery(mld_polyvecl *r, const mld_poly *a,
   mld_assert_abs_bound_2d(r->vec, MLDSA_L, MLDSA_N, MLDSA_Q);
 }
 
+#if defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4) && \
+    MLD_CONFIG_PARAMETER_SET == 44
+
 MLD_INTERNAL_API
 void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
                                            const mld_polyvecl *v)
 {
-#if defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4) && \
-    MLD_CONFIG_PARAMETER_SET == 44
   /* TODO: proof */
   mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, 0, MLDSA_Q);
   mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND);
@@ -300,8 +319,14 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
       w->coeffs, (const int32_t(*)[MLDSA_N])u->vec,
       (const int32_t(*)[MLDSA_N])v->vec);
   mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q);
+}
+
 #elif defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5) && \
     MLD_CONFIG_PARAMETER_SET == 65
+
+void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
+                                           const mld_polyvecl *v)
+{
   /* TODO: proof */
   mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, 0, MLDSA_Q);
   mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND);
@@ -309,8 +334,13 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
       w->coeffs, (const int32_t(*)[MLDSA_N])u->vec,
       (const int32_t(*)[MLDSA_N])v->vec);
   mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q);
+}
+
 #elif defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7) && \
     MLD_CONFIG_PARAMETER_SET == 87
+void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
+                                           const mld_polyvecl *v)
+{
   /* TODO: proof */
   mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, 0, MLDSA_Q);
   mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND);
@@ -318,17 +348,34 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
       w->coeffs, (const int32_t(*)[MLDSA_N])u->vec,
       (const int32_t(*)[MLDSA_N])v->vec);
   mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q);
-#else  /* !(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4 && \
-          MLD_CONFIG_PARAMETER_SET == 44) &&                       \
-          !(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5 && \
-          MLD_CONFIG_PARAMETER_SET == 65) &&                       \
-          MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7 &&   \
-          MLD_CONFIG_PARAMETER_SET == 87 */
-  unsigned int i, j;
-  mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, 0, MLDSA_Q);
-  mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND);
-  /* The first input is bounded by [0, Q-1] inclusive
-   * The second input is bounded by [-9Q+1, 9Q-1] inclusive . Hence, we can
+}
+
+#else /* !(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4 && \
+         MLD_CONFIG_PARAMETER_SET == 44) &&                       \
+         !(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5 && \
+         MLD_CONFIG_PARAMETER_SET == 65) &&                       \
+         MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7 &&   \
+         MLD_CONFIG_PARAMETER_SET == 87 */
+
+#define mld_pointwise_sum_of_products \
+  MLD_NAMESPACE_KL(mld_pointwise_sum_of_products)
+static int64_t mld_pointwise_sum_of_products(const mld_polyvecl *u,
+                                             const mld_polyvecl *v,
+                                             unsigned int i)
+__contract__(
+  requires(memory_no_alias(u, sizeof(mld_polyvecl)))
+  requires(memory_no_alias(v, sizeof(mld_polyvecl)))
+  requires(i < MLDSA_N)
+  requires(forall(l0, 0, MLDSA_L,
+                  array_bound(u->vec[l0].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))
+  requires(forall(l1, 0, MLDSA_L,
+    array_abs_bound(v->vec[l1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
+  ensures(return_value >= -(int64_t) MLDSA_L*(MLDSA_Q - 1)*(MLD_NTT_BOUND - 1))
+  ensures(return_value <=  (int64_t) MLDSA_L*(MLDSA_Q - 1)*(MLD_NTT_BOUND - 1))
+)
+{
+  /* Input vector u is bounded by [0, Q-1] inclusive
+   * Input vector v is bounded by [-9Q+1, 9Q-1] inclusive . Hence, we can
    * safely accumulate in 64-bits without intermediate reductions as
    * MLDSA_L * (MLD_NTT_BOUND-1) * (Q-1) < INT64_MAX
    *
@@ -336,38 +383,53 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
    * (and likewise for negative values)
    */
 
+  int64_t t = 0;
+  unsigned int j;
+  for (j = 0; j < MLDSA_L; j++)
+  __loop__(
+    assigns(j, t)
+    invariant(j <= MLDSA_L)
+    invariant(t >= -(int64_t)j*(MLDSA_Q - 1)*(MLD_NTT_BOUND - 1))
+    invariant(t <= (int64_t)j*(MLDSA_Q - 1)*(MLD_NTT_BOUND - 1))
+  )
+  {
+    const int64_t u64 = (int64_t)u->vec[j].coeffs[i];
+    const int64_t v64 = (int64_t)v->vec[j].coeffs[i];
+    /* Helper assertions for proof efficiency. Do not remove */
+    mld_assert(u64 >= 0 && u64 < MLDSA_Q);
+    mld_assert(v64 > -MLD_NTT_BOUND && v64 < MLD_NTT_BOUND);
+    t += (u64 * v64);
+  }
+  return t;
+}
+
+void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
+                                           const mld_polyvecl *v)
+{
+  unsigned int i;
+
+  mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, 0, MLDSA_Q);
+  mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND);
   for (i = 0; i < MLDSA_N; i++)
   __loop__(
-    assigns(i, j, object_whole(w))
+    assigns(i, object_whole(w))
     invariant(i <= MLDSA_N)
     invariant(array_abs_bound(w->coeffs, 0, i, MLDSA_Q))
   )
   {
-    int64_t t = 0;
-    int32_t r;
-    for (j = 0; j < MLDSA_L; j++)
-    __loop__(
-      assigns(j, t)
-      invariant(j <= MLDSA_L)
-      invariant(t >= -(int64_t)j*(MLDSA_Q - 1)*(MLD_NTT_BOUND - 1))
-      invariant(t <= (int64_t)j*(MLDSA_Q - 1)*(MLD_NTT_BOUND - 1))
-    )
-    {
-      t += (int64_t)u->vec[j].coeffs[i] * v->vec[j].coeffs[i];
-    }
-
-    r = mld_montgomery_reduce(t);
-    w->coeffs[i] = r;
+    w->coeffs[i] =
+        mld_montgomery_reduce(mld_pointwise_sum_of_products(u, v, i));
   }
 
   mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q);
+}
+
 #endif /* !(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4 && \
           MLD_CONFIG_PARAMETER_SET == 44) &&                       \
           !(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5 && \
           MLD_CONFIG_PARAMETER_SET == 65) &&                       \
           !(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7 && \
           MLD_CONFIG_PARAMETER_SET == 87) */
-}
 
 MLD_INTERNAL_API
 uint32_t mld_polyvecl_chknorm(const mld_polyvecl *v, int32_t bound)
@@ -450,7 +512,6 @@ void mld_polyveck_add(mld_polyveck *u, const mld_polyveck *v)
     invariant(i <= MLDSA_K)
     invariant(forall(k0, i, MLDSA_K,
               forall(k1, 0, MLDSA_N, u->vec[k0].coeffs[k1] == loop_entry(*u).vec[k0].coeffs[k1])))
-    invariant(forall(k4, 0, i, forall(k5, 0, MLDSA_N, u->vec[k4].coeffs[k5] == loop_entry(*u).vec[k4].coeffs[k5] + v->vec[k4].coeffs[k5])))
     invariant(forall(k6, 0, i, array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX)))
   )
   {
@@ -459,6 +520,28 @@ void mld_polyveck_add(mld_polyveck *u, const mld_polyveck *v)
   mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX);
 }
 
+/* Reference: We use destructive version (output=first input) to avoid
+ *            reasoning about aliasing in the CBMC specification */
+MLD_INTERNAL_API
+void mld_polyveck_add_error(mld_polyveck *u, const mld_polyveck *v)
+{
+  unsigned int i;
+
+  for (i = 0; i < MLDSA_K; ++i)
+  __loop__(
+    assigns(i, memory_slice(u, sizeof(mld_polyveck)))
+    invariant(i <= MLDSA_K)
+    invariant(forall(k0, i, MLDSA_K,
+              forall(k1, 0, MLDSA_N, u->vec[k0].coeffs[k1] == loop_entry(*u).vec[k0].coeffs[k1])))
+    invariant(forall(k6, 0, i, array_abs_bound(u->vec[k6].coeffs, 0, MLDSA_N, MLDSA_Q)))
+  )
+  {
+    mld_poly_add(&u->vec[i], &v->vec[i]);
+  }
+  mld_assert_abs_bound_2d(u->vec, MLDSA_L, MLDSA_N, MLDSA_Q);
+}
+
+
 MLD_INTERNAL_API
 void mld_polyveck_sub(mld_polyveck *u, const mld_polyveck *v)
 {
diff --git a/mldsa/src/polyvec.h b/mldsa/src/polyvec.h
index 06f1174ec..17fa6815a 100644
--- a/mldsa/src/polyvec.h
+++ b/mldsa/src/polyvec.h
@@ -93,7 +93,6 @@ __contract__(
   requires(forall(k0, 0, MLDSA_L, forall(k1, 0, MLDSA_N, (int64_t) u->vec[k0].coeffs[k1] + v->vec[k0].coeffs[k1] < REDUCE32_DOMAIN_MAX)))
   requires(forall(k2, 0, MLDSA_L, forall(k3, 0, MLDSA_N, (int64_t) u->vec[k2].coeffs[k3] + v->vec[k2].coeffs[k3] >= INT32_MIN)))
   assigns(object_whole(u))
-  ensures(forall(k4, 0, MLDSA_L, forall(k5, 0, MLDSA_N, u->vec[k4].coeffs[k5] == old(*u).vec[k4].coeffs[k5] + v->vec[k4].coeffs[k5])))
   ensures(forall(k6, 0, MLDSA_L,
                  array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX)))
 );
@@ -291,9 +290,29 @@ __contract__(
   requires(forall(k0, 0, MLDSA_K, forall(k1, 0, MLDSA_N, (int64_t) u->vec[k0].coeffs[k1] + v->vec[k0].coeffs[k1] < REDUCE32_DOMAIN_MAX)))
   requires(forall(k2, 0, MLDSA_K, forall(k3, 0, MLDSA_N, (int64_t) u->vec[k2].coeffs[k3] + v->vec[k2].coeffs[k3] >= INT32_MIN)))
   assigns(object_whole(u))
-  ensures(forall(k4, 0, MLDSA_K, forall(k5, 0, MLDSA_N, u->vec[k4].coeffs[k5] == old(*u).vec[k4].coeffs[k5] + v->vec[k4].coeffs[k5])))
-  ensures(forall(k6, 0, MLDSA_L,
-                array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX)))
+  ensures(forall(k6, 0, MLDSA_K, array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX)))
+);
+
+#define mld_polyveck_add_error MLD_NAMESPACE_KL(polyveck_add_error)
+/*************************************************
+ * Name:        mld_polyveck_add_error
+ *
+ * Description: As mld_polyveck_add(), but special
+ *              case (and stronger contracts) when
+ *              input vector v is an error term
+ *              where all coefficients are bounded
+ *              in absolute value by MLDSA_ETA.
+ **************************************************/
+MLD_INTERNAL_API
+void mld_polyveck_add_error(mld_polyveck *u, const mld_polyveck *v)
+__contract__(
+  requires(memory_no_alias(u, sizeof(mld_polyveck)))
+  requires(memory_no_alias(v, sizeof(mld_polyveck)))
+  requires(forall(k0, 0, MLDSA_K, forall(k1, 0, MLDSA_N, (int64_t) u->vec[k0].coeffs[k1] + v->vec[k0].coeffs[k1] < MLDSA_Q)))
+  requires(forall(k2, 0, MLDSA_K, forall(k3, 0, MLDSA_N, (int64_t) u->vec[k2].coeffs[k3] + v->vec[k2].coeffs[k3] > -MLDSA_Q)))
+  requires(forall(k4, 0, MLDSA_K, array_abs_bound(v->vec[k4].coeffs, 0, MLDSA_N, MLDSA_ETA + 1)))
+  assigns(object_whole(u))
+  ensures(forall(k6, 0, MLDSA_K, array_abs_bound(u->vec[k6].coeffs, 0, MLDSA_N, MLDSA_Q)))
 );
 
 #define mld_polyveck_sub MLD_NAMESPACE_KL(polyveck_sub)
diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c
index 695e802ed..38e02243f 100644
--- a/mldsa/src/sign.c
+++ b/mldsa/src/sign.c
@@ -131,6 +131,20 @@ __contract__(
 )
 {
 /* Sample short vectors s1 and s2 */
+#if defined(MLD_CONFIG_SERIAL_FIPS202_ONLY)
+  int i;
+  uint16_t nonce = 0;
+  /* Safety: The nonces are at most 14 (MLDSA_L + MLDSA_K - 1), and, hence, the
+   * casts are safe. */
+  for (i = 0; i < MLDSA_L; i++)
+  {
+    mld_poly_uniform_eta(&s1->vec[i], seed, (uint8_t)(nonce + i));
+  }
+  for (i = 0; i < MLDSA_K; i++)
+  {
+    mld_poly_uniform_eta(&s2->vec[i], seed, (uint8_t)(nonce + MLDSA_L + i));
+  }
+#else /* MLD_CONFIG_SERIAL_FIPS202_ONLY */
 #if MLD_CONFIG_PARAMETER_SET == 44
   mld_poly_uniform_eta_4x(&s1->vec[0], &s1->vec[1], &s1->vec[2], &s1->vec[3],
                           seed, 0, 1, 2, 3);
@@ -155,6 +169,7 @@ __contract__(
   mld_poly_uniform_eta_4x(&s2->vec[4], &s2->vec[5], &s2->vec[6], &s2->vec[7],
                           seed, 11, 12, 13, 14);
 #endif /* MLD_CONFIG_PARAMETER_SET == 87 */
+#endif /* !MLD_CONFIG_SERIAL_FIPS202_ONLY */
 }
 
 MLD_MUST_CHECK_RETURN_VALUE
@@ -195,7 +210,7 @@ int crypto_sign_keypair_internal(uint8_t pk[CRYPTO_PUBLICKEYBYTES],
   mld_polyveck_invntt_tomont(&t1);
 
   /* Add error vector s2 */
-  mld_polyveck_add(&t1, &s2);
+  mld_polyveck_add_error(&t1, &s2);
 
   /* Extract t1 and write public key */
   mld_polyveck_caddq(&t1);
diff --git a/mldsa/src/symmetric.h b/mldsa/src/symmetric.h
index b0706a973..38d122a0b 100644
--- a/mldsa/src/symmetric.h
+++ b/mldsa/src/symmetric.h
@@ -10,7 +10,9 @@
 #include "common.h"
 
 #include MLD_FIPS202_HEADER_FILE
+#if !defined(MLD_CONFIG_SERIAL_FIPS202_ONLY)
 #include MLD_FIPS202X4_HEADER_FILE
+#endif
 
 #define STREAM128_BLOCKBYTES SHAKE128_RATE
 #define STREAM256_BLOCKBYTES SHAKE256_RATE
diff --git a/proofs/cbmc/crypto_sign_keypair_internal/Makefile b/proofs/cbmc/crypto_sign_keypair_internal/Makefile
index b99c2a53b..3d2595319 100644
--- a/proofs/cbmc/crypto_sign_keypair_internal/Makefile
+++ b/proofs/cbmc/crypto_sign_keypair_internal/Makefile
@@ -27,7 +27,7 @@ USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvecl_ntt
 USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvec_matrix_pointwise_montgomery
 USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_reduce
 USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_invntt_tomont
-USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_add
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_add_error
 USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_caddq
 USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_power2round
 USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)pack_pk
diff --git a/proofs/cbmc/pack_pk/Makefile b/proofs/cbmc/pack_pk/Makefile
index 3552b2cd5..4907cd63f 100644
--- a/proofs/cbmc/pack_pk/Makefile
+++ b/proofs/cbmc/pack_pk/Makefile
@@ -25,8 +25,7 @@ USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
-CBMCFLAGS=--smt2
-CBMCFLAGS += --slice-formula
+CBMCFLAGS=--smt2 --no-array-field-sensitivity --slice-formula
 
 FUNCTION_NAME = pack_pk
 
@@ -37,7 +36,7 @@ FUNCTION_NAME = pack_pk
 # EXPENSIVE = true
 
 # This function is large enough to need...
-CBMC_OBJECT_BITS = 8
+CBMC_OBJECT_BITS = 11
 
 # If you require access to a file-local ("static") function or object to conduct
 # your proof, set the following (and do not include the original source file
diff --git a/proofs/cbmc/pointwise_sum_of_products/Makefile b/proofs/cbmc/pointwise_sum_of_products/Makefile
new file mode 100644
index 000000000..68e842a3f
--- /dev/null
+++ b/proofs/cbmc/pointwise_sum_of_products/Makefile
@@ -0,0 +1,55 @@
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = pointwise_sum_of_products_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = pointwise_sum_of_products
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)mld_pointwise_sum_of_products
+USE_FUNCTION_CONTRACTS=
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2 --slice-formula --no-array-field-sensitivity
+
+FUNCTION_NAME = pointwise_sum_of_products
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 12
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mldsa/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common
diff --git a/proofs/cbmc/pointwise_sum_of_products/pointwise_sum_of_products_harness.c b/proofs/cbmc/pointwise_sum_of_products/pointwise_sum_of_products_harness.c
new file mode 100644
index 000000000..36d263fe4
--- /dev/null
+++ b/proofs/cbmc/pointwise_sum_of_products/pointwise_sum_of_products_harness.c
@@ -0,0 +1,17 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include "polyvec.h"
+
+#define mld_pointwise_sum_of_products \
+  MLD_NAMESPACE_KL(mld_pointwise_sum_of_products)
+int64_t mld_pointwise_sum_of_products(const mld_polyvecl *u,
+                                      const mld_polyvecl *v, unsigned int i);
+
+void harness(void)
+{
+  mld_polyvecl *u, *v;
+  unsigned int i;
+  int64_t r;
+  r = mld_pointwise_sum_of_products(u, v, i);
+}
diff --git a/proofs/cbmc/poly_uniform_eta/Makefile b/proofs/cbmc/poly_uniform_eta/Makefile
new file mode 100644
index 000000000..a0efb9243
--- /dev/null
+++ b/proofs/cbmc/poly_uniform_eta/Makefile
@@ -0,0 +1,61 @@
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = poly_uniform_eta_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = poly_uniform_eta
+
+DEFINES += -DMLD_CONFIG_SERIAL_FIPS202_ONLY
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_eta
+USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256_init
+USE_FUNCTION_CONTRACTS+=$(FIPS202_NAMESPACE)shake256_absorb
+USE_FUNCTION_CONTRACTS+=$(FIPS202_NAMESPACE)shake256_finalize
+USE_FUNCTION_CONTRACTS+=$(FIPS202_NAMESPACE)shake256_squeeze
+USE_FUNCTION_CONTRACTS+=mld_rej_eta
+USE_FUNCTION_CONTRACTS+=$(FIPS202_NAMESPACE)shake256_release
+USE_FUNCTION_CONTRACTS+=mld_zeroize
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = poly_uniform_eta
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 9
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mldsa/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common
diff --git a/proofs/cbmc/poly_uniform_eta/poly_uniform_eta_harness.c b/proofs/cbmc/poly_uniform_eta/poly_uniform_eta_harness.c
new file mode 100644
index 000000000..f22f22891
--- /dev/null
+++ b/proofs/cbmc/poly_uniform_eta/poly_uniform_eta_harness.c
@@ -0,0 +1,13 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include "poly_kl.h"
+
+void harness(void)
+{
+  mld_poly *r0;
+  const uint8_t *seed;
+  uint8_t n0;
+
+  mld_poly_uniform_eta(r0, seed, n0);
+}
diff --git a/proofs/cbmc/polyvec_matrix_expand_serial/Makefile b/proofs/cbmc/polyvec_matrix_expand_serial/Makefile
new file mode 100644
index 000000000..d29d6c872
--- /dev/null
+++ b/proofs/cbmc/polyvec_matrix_expand_serial/Makefile
@@ -0,0 +1,55 @@
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = polyvec_matrix_expand_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = polyvec_matrix_expand_serial
+
+DEFINES += -DMLD_CONFIG_SERIAL_FIPS202_ONLY
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvec_matrix_expand
+USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2 --arrays-uf-always --slice-formula
+
+FUNCTION_NAME = polyvec_matrix_expand_serial
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 11
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mldsa/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common
diff --git a/proofs/cbmc/polyvec_matrix_expand_serial/polyvec_matrix_expand_harness.c b/proofs/cbmc/polyvec_matrix_expand_serial/polyvec_matrix_expand_harness.c
new file mode 100644
index 000000000..775a9c637
--- /dev/null
+++ b/proofs/cbmc/polyvec_matrix_expand_serial/polyvec_matrix_expand_harness.c
@@ -0,0 +1,12 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include "polyvec.h"
+
+void harness(void)
+{
+  mld_polyvecl *mat;
+  uint8_t *rho;
+
+  mld_polyvec_matrix_expand(mat, rho);
+}
diff --git a/proofs/cbmc/polyveck_add_error/Makefile b/proofs/cbmc/polyveck_add_error/Makefile
new file mode 100644
index 000000000..e1feef49d
--- /dev/null
+++ b/proofs/cbmc/polyveck_add_error/Makefile
@@ -0,0 +1,55 @@
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = polyveck_add_error_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = polyveck_add_error
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_add_error
+USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_add
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2 --arrays-uf-always --slice-formula
+
+FUNCTION_NAME = polyveck_add_error
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 8
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mldsa/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common
diff --git a/proofs/cbmc/polyveck_add_error/polyveck_add_error_harness.c b/proofs/cbmc/polyveck_add_error/polyveck_add_error_harness.c
new file mode 100644
index 000000000..26f2a9408
--- /dev/null
+++ b/proofs/cbmc/polyveck_add_error/polyveck_add_error_harness.c
@@ -0,0 +1,10 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include "polyvec.h"
+
+void harness(void)
+{
+  mld_polyveck *r, *b;
+  mld_polyveck_add_error(r, b);
+}
diff --git a/proofs/cbmc/polyvecl_add/Makefile b/proofs/cbmc/polyvecl_add/Makefile
index 9dd5289e1..38de96cdd 100644
--- a/proofs/cbmc/polyvecl_add/Makefile
+++ b/proofs/cbmc/polyvecl_add/Makefile
@@ -37,7 +37,7 @@ FUNCTION_NAME = polyvecl_add
 # EXPENSIVE = true
 
 # This function is large enough to need...
-CBMC_OBJECT_BITS = 8
+CBMC_OBJECT_BITS = 10
 
 # If you require access to a file-local ("static") function or object to conduct
 # your proof, set the following (and do not include the original source file
diff --git a/proofs/cbmc/polyvecl_pointwise_acc_montgomery/Makefile b/proofs/cbmc/polyvecl_pointwise_acc_montgomery/Makefile
index 9f139398b..8f81c0309 100644
--- a/proofs/cbmc/polyvecl_pointwise_acc_montgomery/Makefile
+++ b/proofs/cbmc/polyvecl_pointwise_acc_montgomery/Makefile
@@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_pointwise_acc_montgomery
-USE_FUNCTION_CONTRACTS=mld_montgomery_reduce
+USE_FUNCTION_CONTRACTS=mld_montgomery_reduce $(MLD_NAMESPACE)mld_pointwise_sum_of_products
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
diff --git a/proofs/cbmc/polyvecl_uniform_gamma1_serial/Makefile b/proofs/cbmc/polyvecl_uniform_gamma1_serial/Makefile
new file mode 100644
index 000000000..d63af8b40
--- /dev/null
+++ b/proofs/cbmc/polyvecl_uniform_gamma1_serial/Makefile
@@ -0,0 +1,57 @@
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = polyvecl_uniform_gamma1_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = polyvecl_uniform_gamma1_serial
+
+DEFINES += -DMLD_CONFIG_SERIAL_FIPS202_ONLY
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+
+UNWINDSET += $(MLD_NAMESPACE)polyvecl_uniform_gamma1.0:7 # Largest value of MLDSA_L
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_uniform_gamma1
+USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_gamma1
+
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = polyvecl_uniform_gamma1_serial
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 10
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mldsa/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common
diff --git a/proofs/cbmc/polyvecl_uniform_gamma1_serial/polyvecl_uniform_gamma1_harness.c b/proofs/cbmc/polyvecl_uniform_gamma1_serial/polyvecl_uniform_gamma1_harness.c
new file mode 100644
index 000000000..da4d75a99
--- /dev/null
+++ b/proofs/cbmc/polyvecl_uniform_gamma1_serial/polyvecl_uniform_gamma1_harness.c
@@ -0,0 +1,13 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include "polyvec.h"
+
+void harness(void)
+{
+  mld_polyvecl *v;
+  const uint8_t *seed;
+  uint16_t nonce;
+
+  mld_polyvecl_uniform_gamma1(v, seed, nonce);
+}
diff --git a/proofs/cbmc/sample_s1_s2_serial/Makefile b/proofs/cbmc/sample_s1_s2_serial/Makefile
new file mode 100644
index 000000000..701a6a417
--- /dev/null
+++ b/proofs/cbmc/sample_s1_s2_serial/Makefile
@@ -0,0 +1,56 @@
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = sample_s1_s2_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = mld_sample_s1_s2_serial
+
+DEFINES += -DMLD_CONFIG_SERIAL_FIPS202_ONLY
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET += mld_sample_s1_s2.0:7 # Largest value of MLDSA_L
+UNWINDSET += mld_sample_s1_s2.1:8 # Largest value of MLDSA_K
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/sign.c
+
+CHECK_FUNCTION_CONTRACTS=mld_sample_s1_s2
+USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_eta
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = mld_sample_s1_s2_serial
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 10
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mldsa/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common
diff --git a/proofs/cbmc/sample_s1_s2_serial/sample_s1_s2_harness.c b/proofs/cbmc/sample_s1_s2_serial/sample_s1_s2_harness.c
new file mode 100644
index 000000000..84a392a09
--- /dev/null
+++ b/proofs/cbmc/sample_s1_s2_serial/sample_s1_s2_harness.c
@@ -0,0 +1,16 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include "sign.h"
+
+static void mld_sample_s1_s2(mld_polyvecl *s1, mld_polyveck *s2,
+                             const uint8_t seed[MLDSA_CRHBYTES]);
+
+void harness(void)
+{
+  mld_polyvecl *s1;
+  mld_polyveck *s2;
+  uint8_t *seed;
+
+  mld_sample_s1_s2(s1, s2, seed);
+}
diff --git a/scripts/tests b/scripts/tests
index a7be6612c..2a70c1383 100755
--- a/scripts/tests
+++ b/scripts/tests
@@ -204,6 +204,7 @@ class TEST_TYPES(Enum):
     BRING_YOUR_OWN_FIPS202 = 9
     MONOLITHIC_BUILD = 10
     MONOLITHIC_BUILD_MULTILEVEL = 11
+    BRING_YOUR_OWN_FIPS202_STATIC = 12
 
     def is_benchmark(self):
         return self in [TEST_TYPES.BENCH, TEST_TYPES.BENCH_COMPONENTS]
@@ -218,6 +219,7 @@ class TEST_TYPES(Enum):
             TEST_TYPES.BRING_YOUR_OWN_FIPS202,
             TEST_TYPES.MONOLITHIC_BUILD,
             TEST_TYPES.MONOLITHIC_BUILD_MULTILEVEL,
+            TEST_TYPES.BRING_YOUR_OWN_FIPS202_STATIC,
         ]
 
     @staticmethod
@@ -255,6 +257,8 @@ class TEST_TYPES(Enum):
             return "Example (single compilation unit)"
         if self == TEST_TYPES.MONOLITHIC_BUILD_MULTILEVEL:
             return "Example (single compilation unit, multilevel)"
+        if self == TEST_TYPES.BRING_YOUR_OWN_FIPS202_STATIC:
+            return "Example (bring your own FIPS-202, static)"
 
     def make_dir(self):
         if self == TEST_TYPES.BASIC:
@@ -265,6 +269,8 @@ class TEST_TYPES(Enum):
             return "examples/monolithic_build"
         if self == TEST_TYPES.MONOLITHIC_BUILD_MULTILEVEL:
             return "examples/monolithic_build_multilevel"
+        if self == TEST_TYPES.BRING_YOUR_OWN_FIPS202_STATIC:
+            return "examples/bring_your_own_fips202_static"
         return ""
 
     def make_target(self):
@@ -286,6 +292,8 @@ class TEST_TYPES(Enum):
             return ""
         if self == TEST_TYPES.BRING_YOUR_OWN_FIPS202:
             return ""
+        if self == TEST_TYPES.BRING_YOUR_OWN_FIPS202_STATIC:
+            return ""
         return ""
 
     def make_run_target(self, scheme):
@@ -973,6 +981,7 @@ def cli():
             "bring_your_own_fips202",
             "monolithic_build",
             "monolithic_build_multilevel",
+            "bring_your_own_fips202_static",
         ],
         action="append",
     )
diff --git a/test/break_pct_config.h b/test/break_pct_config.h
index aff15bbc9..ed58a349d 100644
--- a/test/break_pct_config.h
+++ b/test/break_pct_config.h
@@ -432,7 +432,28 @@ static MLD_INLINE int mld_break_pct(void)
  *****************************************************************************/
 /* #define MLD_CONFIG_NO_ASM_VALUE_BARRIER */
 
-
+/******************************************************************************
+ * Name:        MLD_CONFIG_SERIAL_FIPS202_ONLY
+ *
+ * Description: Set this to use a FIPS202 implementation with global state
+ *              that supports only one active Keccak computation at a time
+ *              (e.g. some hardware accelerators).
+ *
+ *              If this option is set, ML-DSA will use FIPS202 operations
+ *              serially, ensuring that only one SHAKE context is active
+ *              at any given time.
+ *
+ *              This allows offloading Keccak computations to a hardware
+ *              accelerator that holds only a single Keccak state locally,
+ *              rather than requiring support for multiple concurrent
+ *              Keccak states.
+ *
+ *              NOTE: Depending on the target CPU, this may reduce
+ *              performance when using software FIPS202 implementations.
+ *              Only enable this when you have to.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
 /*************************  Config internals  ********************************/
 
diff --git a/test/configs.yml b/test/configs.yml
index a83ed8e60..82f9399f6 100644
--- a/test/configs.yml
+++ b/test/configs.yml
@@ -23,6 +23,11 @@ configs:
           }
           #endif
 
+  - path: test/serial_fips202_config.h
+    description: "Test configuration with serial FIPS202 only"
+    defines:
+      MLD_CONFIG_SERIAL_FIPS202_ONLY: true
+
   - path: test/custom_randombytes_config.h
     description: "Test configuration with custom randombytes"
     defines:
diff --git a/test/custom_memcpy_config.h b/test/custom_memcpy_config.h
index 632a5dd22..db8da58e6 100644
--- a/test/custom_memcpy_config.h
+++ b/test/custom_memcpy_config.h
@@ -435,7 +435,28 @@ static MLD_INLINE void *mld_memcpy(void *dest, const void *src, size_t n)
  *****************************************************************************/
 /* #define MLD_CONFIG_NO_ASM_VALUE_BARRIER */
 
-
+/******************************************************************************
+ * Name:        MLD_CONFIG_SERIAL_FIPS202_ONLY
+ *
+ * Description: Set this to use a FIPS202 implementation with global state
+ *              that supports only one active Keccak computation at a time
+ *              (e.g. some hardware accelerators).
+ *
+ *              If this option is set, ML-DSA will use FIPS202 operations
+ *              serially, ensuring that only one SHAKE context is active
+ *              at any given time.
+ *
+ *              This allows offloading Keccak computations to a hardware
+ *              accelerator that holds only a single Keccak state locally,
+ *              rather than requiring support for multiple concurrent
+ *              Keccak states.
+ *
+ *              NOTE: Depending on the target CPU, this may reduce
+ *              performance when using software FIPS202 implementations.
+ *              Only enable this when you have to.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
 /*************************  Config internals  ********************************/
 
diff --git a/test/custom_memset_config.h b/test/custom_memset_config.h
index 4efcc8f5b..5153e01d6 100644
--- a/test/custom_memset_config.h
+++ b/test/custom_memset_config.h
@@ -434,7 +434,28 @@ static MLD_INLINE void *mld_memset(void *s, int c, size_t n)
  *****************************************************************************/
 /* #define MLD_CONFIG_NO_ASM_VALUE_BARRIER */
 
-
+/******************************************************************************
+ * Name:        MLD_CONFIG_SERIAL_FIPS202_ONLY
+ *
+ * Description: Set this to use a FIPS202 implementation with global state
+ *              that supports only one active Keccak computation at a time
+ *              (e.g. some hardware accelerators).
+ *
+ *              If this option is set, ML-DSA will use FIPS202 operations
+ *              serially, ensuring that only one SHAKE context is active
+ *              at any given time.
+ *
+ *              This allows offloading Keccak computations to a hardware
+ *              accelerator that holds only a single Keccak state locally,
+ *              rather than requiring support for multiple concurrent
+ *              Keccak states.
+ *
+ *              NOTE: Depending on the target CPU, this may reduce
+ *              performance when using software FIPS202 implementations.
+ *              Only enable this when you have to.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
 /*************************  Config internals  ********************************/
 
diff --git a/test/custom_randombytes_config.h b/test/custom_randombytes_config.h
index 7187e6013..3a28f952e 100644
--- a/test/custom_randombytes_config.h
+++ b/test/custom_randombytes_config.h
@@ -428,7 +428,28 @@ static MLD_INLINE void mld_randombytes(uint8_t *ptr, size_t len)
  *****************************************************************************/
 /* #define MLD_CONFIG_NO_ASM_VALUE_BARRIER */
 
-
+/******************************************************************************
+ * Name:        MLD_CONFIG_SERIAL_FIPS202_ONLY
+ *
+ * Description: Set this to use a FIPS202 implementation with global state
+ *              that supports only one active Keccak computation at a time
+ *              (e.g. some hardware accelerators).
+ *
+ *              If this option is set, ML-DSA will use FIPS202 operations
+ *              serially, ensuring that only one SHAKE context is active
+ *              at any given time.
+ *
+ *              This allows offloading Keccak computations to a hardware
+ *              accelerator that holds only a single Keccak state locally,
+ *              rather than requiring support for multiple concurrent
+ *              Keccak states.
+ *
+ *              NOTE: Depending on the target CPU, this may reduce
+ *              performance when using software FIPS202 implementations.
+ *              Only enable this when you have to.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
 /*************************  Config internals  ********************************/
 
diff --git a/test/custom_stdlib_config.h b/test/custom_stdlib_config.h
index 0a529ef84..7308c57cf 100644
--- a/test/custom_stdlib_config.h
+++ b/test/custom_stdlib_config.h
@@ -443,7 +443,28 @@ static MLD_INLINE void *mld_memset(void *s, int c, size_t n)
  *****************************************************************************/
 /* #define MLD_CONFIG_NO_ASM_VALUE_BARRIER */
 
-
+/******************************************************************************
+ * Name:        MLD_CONFIG_SERIAL_FIPS202_ONLY
+ *
+ * Description: Set this to use a FIPS202 implementation with global state
+ *              that supports only one active Keccak computation at a time
+ *              (e.g. some hardware accelerators).
+ *
+ *              If this option is set, ML-DSA will use FIPS202 operations
+ *              serially, ensuring that only one SHAKE context is active
+ *              at any given time.
+ *
+ *              This allows offloading Keccak computations to a hardware
+ *              accelerator that holds only a single Keccak state locally,
+ *              rather than requiring support for multiple concurrent
+ *              Keccak states.
+ *
+ *              NOTE: Depending on the target CPU, this may reduce
+ *              performance when using software FIPS202 implementations.
+ *              Only enable this when you have to.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
 /*************************  Config internals  ********************************/
 
diff --git a/test/custom_zeroize_config.h b/test/custom_zeroize_config.h
index eec8cda42..1ca8ea6d4 100644
--- a/test/custom_zeroize_config.h
+++ b/test/custom_zeroize_config.h
@@ -428,7 +428,28 @@ static MLD_INLINE void mld_zeroize_native(void *ptr, size_t len)
  *****************************************************************************/
 /* #define MLD_CONFIG_NO_ASM_VALUE_BARRIER */
 
-
+/******************************************************************************
+ * Name:        MLD_CONFIG_SERIAL_FIPS202_ONLY
+ *
+ * Description: Set this to use a FIPS202 implementation with global state
+ *              that supports only one active Keccak computation at a time
+ *              (e.g. some hardware accelerators).
+ *
+ *              If this option is set, ML-DSA will use FIPS202 operations
+ *              serially, ensuring that only one SHAKE context is active
+ *              at any given time.
+ *
+ *              This allows offloading Keccak computations to a hardware
+ *              accelerator that holds only a single Keccak state locally,
+ *              rather than requiring support for multiple concurrent
+ *              Keccak states.
+ *
+ *              NOTE: Depending on the target CPU, this may reduce
+ *              performance when using software FIPS202 implementations.
+ *              Only enable this when you have to.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
 /*************************  Config internals  ********************************/
 
diff --git a/test/no_asm_config.h b/test/no_asm_config.h
index 1783636ba..9d4b27a92 100644
--- a/test/no_asm_config.h
+++ b/test/no_asm_config.h
@@ -429,7 +429,28 @@ static MLD_INLINE void mld_zeroize_native(void *ptr, size_t len)
  *****************************************************************************/
 /* #define MLD_CONFIG_NO_ASM_VALUE_BARRIER */
 
-
+/******************************************************************************
+ * Name:        MLD_CONFIG_SERIAL_FIPS202_ONLY
+ *
+ * Description: Set this to use a FIPS202 implementation with global state
+ *              that supports only one active Keccak computation at a time
+ *              (e.g. some hardware accelerators).
+ *
+ *              If this option is set, ML-DSA will use FIPS202 operations
+ *              serially, ensuring that only one SHAKE context is active
+ *              at any given time.
+ *
+ *              This allows offloading Keccak computations to a hardware
+ *              accelerator that holds only a single Keccak state locally,
+ *              rather than requiring support for multiple concurrent
+ *              Keccak states.
+ *
+ *              NOTE: Depending on the target CPU, this may reduce
+ *              performance when using software FIPS202 implementations.
+ *              Only enable this when you have to.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_SERIAL_FIPS202_ONLY */
 
 /*************************  Config internals  ********************************/
 
diff --git a/test/serial_fips202_config.h b/test/serial_fips202_config.h
new file mode 100644
index 000000000..3cf2b1e9c
--- /dev/null
+++ b/test/serial_fips202_config.h
@@ -0,0 +1,475 @@
+/*
+ * Copyright (c) The mldsa-native project authors
+ * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+ */
+
+/* References
+ * ==========
+ *
+ * - [FIPS140_3_IG]
+ *   Implementation Guidance for FIPS 140-3 and the Cryptographic Module
+ *   Validation Program National Institute of Standards and Technology
+ *   https://csrc.nist.gov/projects/cryptographic-module-validation-program/fips-140-3-ig-announcements
+ *
+ * - [FIPS204]
+ *   FIPS 204 Module-Lattice-Based Digital Signature Standard
+ *   National Institute of Standards and Technology
+ *   https://csrc.nist.gov/pubs/fips/204/final
+ */
+
+/*
+ * WARNING: This file is auto-generated from scripts/autogen
+ *          in the mldsa-native repository.
+ *          Do not modify it directly.
+ */
+
+/*
+ * Test configuration: Test configuration with serial FIPS202 only
+ *
+ * This configuration differs from the default mldsa/src/config.h in the
+ * following places:
+ *   - MLD_CONFIG_SERIAL_FIPS202_ONLY
+ */
+
+
+#ifndef MLD_CONFIG_H
+#define MLD_CONFIG_H
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_PARAMETER_SET
+ *
+ * Description: Specifies the parameter set for ML-DSA
+ *              - MLD_CONFIG_PARAMETER_SET=44 corresponds to ML-DSA-44
+ *              - MLD_CONFIG_PARAMETER_SET=65 corresponds to ML-DSA-65
+ *              - MLD_CONFIG_PARAMETER_SET=87 corresponds to ML-DSA-87
+ *
+ *              This can also be set using CFLAGS.
+ *
+ *****************************************************************************/
+#ifndef MLD_CONFIG_PARAMETER_SET
+#define MLD_CONFIG_PARAMETER_SET \
+  44 /* Change this for different security strengths */
+#endif
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_NAMESPACE_PREFIX
+ *
+ * Description: The prefix to use to namespace global symbols from mldsa/.
+ *
+ *              In a multi-level build (that is, if either
+ *              - MLD_CONFIG_MULTILEVEL_WITH_SHARED, or
+ *              - MLD_CONFIG_MULTILEVEL_NO_SHARED,
+ *              are set, level-dependent symbols will additionally be prefixed
+ *              with the parameter set (44/65/87).
+ *
+ *              This can also be set using CFLAGS.
+ *
+ *****************************************************************************/
+#if !defined(MLD_CONFIG_NAMESPACE_PREFIX)
+#define MLD_CONFIG_NAMESPACE_PREFIX MLD_DEFAULT_NAMESPACE_PREFIX
+#endif
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_MULTILEVEL_WITH_SHARED
+ *
+ * Description: This is for multi-level builds of mldsa-native only. If you
+ *              need only a single parameter set, keep this unset.
+ *
+ *              If this is set, all MLD_CONFIG_PARAMETER_SET-independent
+ *              code will be included in the build, including code needed only
+ *              for other parameter sets.
+ *
+ *              Example: TODO: add example
+ *
+ *              To build mldsa-native with support for all parameter sets,
+ *              build it three times -- once per parameter set -- and set the
+ *              option MLD_CONFIG_MULTILEVEL_WITH_SHARED for exactly one of
+ *              them, and MLD_CONFIG_MULTILEVEL_NO_SHARED for the others.
+ *
+ *              See examples/multilevel_build_mldsa for an example.
+ *
+ *              This can also be set using CFLAGS.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_MULTILEVEL_WITH_SHARED */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_MULTILEVEL_NO_SHARED
+ *
+ * Description: This is for multi-level builds of mldsa-native only. If you
+ *              need only a single parameter set, keep this unset.
+ *
+ *              If this is set, no MLD_CONFIG_PARAMETER_SET-independent code
+ *              will be included in the build.
+ *
+ *              To build mldsa-native with support for all parameter sets,
+ *              build it three times -- once per parameter set -- and set the
+ *              option MLD_CONFIG_MULTILEVEL_WITH_SHARED for exactly one of
+ *              them, and MLD_CONFIG_MULTILEVEL_NO_SHARED for the others.
+ *
+ *              See examples/multilevel_build_mldsa for an example.
+ *
+ *              This can also be set using CFLAGS.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_MULTILEVEL_NO_SHARED */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_FILE
+ *
+ * Description: If defined, this is a header that will be included instead
+ *              of the default configuration file mldsa/src/config.h.
+ *
+ *              When you need to build mldsa-native in multiple configurations,
+ *              using varying MLD_CONFIG_FILE can be more convenient
+ *              then configuring everything through CFLAGS.
+ *
+ *              To use, MLD_CONFIG_FILE _must_ be defined prior
+ *              to the inclusion of any mldsa-native headers. For example,
+ *              it can be set by passing `-DMLD_CONFIG_FILE="..."`
+ *              on the command line.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_FILE "config.h" */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_ARITH_BACKEND_FILE
+ *
+ * Description: The arithmetic backend to use.
+ *
+ *              If MLD_CONFIG_USE_NATIVE_BACKEND_ARITH is unset, this option
+ *              is ignored.
+ *
+ *              If MLD_CONFIG_USE_NATIVE_BACKEND_ARITH is set, this option must
+ *              either be undefined or the filename of an arithmetic backend.
+ *              If unset, the default backend will be used.
+ *
+ *              This can be set using CFLAGS.
+ *
+ *****************************************************************************/
+#if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH) && \
+    !defined(MLD_CONFIG_ARITH_BACKEND_FILE)
+#define MLD_CONFIG_ARITH_BACKEND_FILE "native/meta.h"
+#endif
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_FIPS202_BACKEND_FILE
+ *
+ * Description: The FIPS-202 backend to use.
+ *
+ *              If MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 is set, this option
+ *              must either be undefined or the filename of a FIPS202 backend.
+ *              If unset, the default backend will be used.
+ *
+ *              This can be set using CFLAGS.
+ *
+ *****************************************************************************/
+#if defined(MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202) && \
+    !defined(MLD_CONFIG_FIPS202_BACKEND_FILE)
+#define MLD_CONFIG_FIPS202_BACKEND_FILE "fips202/native/auto.h"
+#endif
+/******************************************************************************
+ * Name:        MLD_CONFIG_FIPS202_CUSTOM_HEADER
+ *
+ * Description: Custom header to use for FIPS-202
+ *
+ *              This should only be set if you intend to use a custom
+ *              FIPS-202 implementation, different from the one shipped
+ *              with mldsa-native.
+ *
+ *              If set, it must be the name of a file serving as the
+ *              replacement for mldsa/src/fips202/fips202.h, and exposing
+ *              the same API (see FIPS202.md).
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_FIPS202_CUSTOM_HEADER "SOME_FILE.h" */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_FIPS202X4_CUSTOM_HEADER
+ *
+ * Description: Custom header to use for FIPS-202-X4
+ *
+ *              This should only be set if you intend to use a custom
+ *              FIPS-202 implementation, different from the one shipped
+ *              with mldsa-native.
+ *
+ *              If set, it must be the name of a file serving as the
+ *              replacement for mldsa/src/fips202/fips202x4.h, and exposing
+ *              the same API (see FIPS202.md).
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_FIPS202X4_CUSTOM_HEADER "SOME_FILE.h" */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_CUSTOM_ZEROIZE
+ *
+ * Description: In compliance with @[FIPS204, Section 3.6.3], mldsa-native,
+ *              zeroizes intermediate stack buffers before returning from
+ *              function calls.
+ *
+ *              Set this option and define `mld_zeroize_native` if you want to
+ *              use a custom method to zeroize intermediate stack buffers.
+ *              The default implementation uses SecureZeroMemory on Windows
+ *              and a memset + compiler barrier otherwise. If neither of those
+ *              is available on the target platform, compilation will fail,
+ *              and you will need to use MLD_CONFIG_CUSTOM_ZEROIZE to provide
+ *              a custom implementation of `mld_zeroize_native()`.
+ *
+ *              WARNING:
+ *              The explicit stack zeroization conducted by mldsa-native
+ *              reduces the likelihood of data leaking on the stack, but
+ *              does not eliminate it! The C standard makes no guarantee about
+ *              where a compiler allocates structures and whether/where it makes
+ *              copies of them. Also, in addition to entire structures, there
+ *              may also be potentially exploitable leakage of individual values
+ *              on the stack.
+ *
+ *              If you need bullet-proof zeroization of the stack, you need to
+ *              consider additional measures instead of what this feature
+ *              provides. In this case, you can set mld_zeroize_native to a
+ *              no-op.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_CUSTOM_ZEROIZE
+   #if !defined(__ASSEMBLER__)
+   #include <stdint.h>
+   #include "sys.h"
+   static MLD_INLINE void mld_zeroize_native(void *ptr, size_t len)
+   {
+       ... your implementation ...
+   }
+   #endif
+*/
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_CUSTOM_MEMCPY
+ *
+ * Description: Set this option and define `mld_memcpy` if you want to
+ *              use a custom method to copy memory instead of the standard
+ *              library memcpy function.
+ *
+ *              The custom implementation must have the same signature and
+ *              behavior as the standard memcpy function:
+ *              void *mld_memcpy(void *dest, const void *src, size_t n)
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_CUSTOM_MEMCPY
+   #if !defined(__ASSEMBLER__)
+   #include <stdint.h>
+   #include "sys.h"
+   static MLD_INLINE void *mld_memcpy(void *dest, const void *src, size_t n)
+   {
+       ... your implementation ...
+   }
+   #endif
+*/
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_CUSTOM_MEMSET
+ *
+ * Description: Set this option and define `mld_memset` if you want to
+ *              use a custom method to set memory instead of the standard
+ *              library memset function.
+ *
+ *              The custom implementation must have the same signature and
+ *              behavior as the standard memset function:
+ *              void *mld_memset(void *s, int c, size_t n)
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_CUSTOM_MEMSET
+   #if !defined(__ASSEMBLER__)
+   #include <stdint.h>
+   #include "sys.h"
+   static MLD_INLINE void *mld_memset(void *s, int c, size_t n)
+   {
+       ... your implementation ...
+   }
+   #endif
+*/
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_CUSTOM_RANDOMBYTES
+ *
+ * Description: mldsa-native does not provide a secure randombytes
+ *              implementation. Such an implementation has to provided by the
+ *              consumer.
+ *
+ *              If this option is not set, mldsa-native expects a function
+ *              void randombytes(uint8_t *out, size_t outlen).
+ *
+ *              Set this option and define `mld_randombytes` if you want to
+ *              use a custom method to sample randombytes with a different name
+ *              or signature.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_CUSTOM_RANDOMBYTES
+   #if !defined(__ASSEMBLER__)
+   #include <stdint.h>
+   #include "sys.h"
+   static MLD_INLINE void mld_randombytes(uint8_t *ptr, size_t len)
+   {
+       ... your implementation ...
+   }
+   #endif
+*/
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_KEYGEN_PCT
+ *
+ * Description: Compliance with @[FIPS140_3_IG, p.87] requires a
+ *              Pairwise Consistency Test (PCT) to be carried out on a freshly
+ *              generated keypair before it can be exported.
+ *
+ *              Set this option if such a check should be implemented.
+ *              In this case, crypto_sign_keypair_internal and
+ *              crypto_sign_keypair will return a non-zero error code if the
+ *              PCT failed.
+ *
+ *              NOTE: This feature will drastically lower the performance of
+ *              key generation.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_KEYGEN_PCT */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_KEYGEN_PCT_BREAKAGE_TEST
+ *
+ * Description: If this option is set, the user must provide a runtime
+ *              function `static inline int mld_break_pct() { ... }` to
+ *              indicate whether the PCT should be made fail.
+ *
+ *              This option only has an effect if MLD_CONFIG_KEYGEN_PCT is set.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_KEYGEN_PCT_BREAKAGE_TEST
+   #if !defined(__ASSEMBLER__)
+   #include "sys.h"
+   static MLD_INLINE int mld_break_pct(void)
+   {
+       ... return 0/1 depending on whether PCT should be broken ...
+   }
+   #endif
+*/
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_INTERNAL_API_QUALIFIER
+ *
+ * Description: If set, this option provides an additional function
+ *              qualifier to be added to declarations of internal API.
+ *
+ *              The primary use case for this option are single-CU builds,
+ *              in which case this option can be set to `static`.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_INTERNAL_API_QUALIFIER */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_EXTERNAL_API_QUALIFIER
+ *
+ * Description: If set, this option provides an additional function
+ *              qualifier to be added to declarations of mldsa-native's
+ *              public API.
+ *
+ *              The primary use case for this option are single-CU builds
+ *              where the public API exposed by mldsa-native is wrapped by
+ *              another API in the consuming application. In this case,
+ *              even mldsa-native's public API can be marked `static`.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_EXTERNAL_API_QUALIFIER */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_CT_TESTING_ENABLED
+ *
+ * Description: If set, mldsa-native annotates data as secret / public using
+ *              valgrind's annotations VALGRIND_MAKE_MEM_UNDEFINED and
+ *              VALGRIND_MAKE_MEM_DEFINED, enabling various checks for secret-
+ *              dependent control flow of variable time execution (depending
+ *              on the exact version of valgrind installed).
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_CT_TESTING_ENABLED */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_NO_ASM
+ *
+ * Description: If this option is set, mldsa-native will be built without
+ *              use of native code or inline assembly.
+ *
+ *              By default, inline assembly is used to implement value barriers.
+ *              Without inline assembly, mldsa-native will use a global volatile
+ *              'opt blocker' instead; see ct.h.
+ *
+ *              Inline assembly is also used to implement a secure zeroization
+ *              function on non-Windows platforms. If this option is set and
+ *              the target platform is not Windows, you MUST set
+ *              MLD_CONFIG_CUSTOM_ZEROIZE and provide a custom zeroization
+ *              function.
+ *
+ *              If this option is set, MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 and
+ *              and MLD_CONFIG_USE_NATIVE_BACKEND_ARITH will be ignored, and no
+ *              native backends will be used.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_NO_ASM */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_NO_ASM_VALUE_BARRIER
+ *
+ * Description: If this option is set, mldsa-native will be built without
+ *              use of native code or inline assembly for value barriers.
+ *
+ *              By default, inline assembly (if available) is used to implement
+ *              value barriers.
+ *              Without inline assembly, mldsa-native will use a global volatile
+ *              'opt blocker' instead; see ct.h.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_NO_ASM_VALUE_BARRIER */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_SERIAL_FIPS202_ONLY
+ *
+ * Description: Set this to use a FIPS202 implementation with global state
+ *              that supports only one active Keccak computation at a time
+ *              (e.g. some hardware accelerators).
+ *
+ *              If this option is set, ML-DSA will use FIPS202 operations
+ *              serially, ensuring that only one SHAKE context is active
+ *              at any given time.
+ *
+ *              This allows offloading Keccak computations to a hardware
+ *              accelerator that holds only a single Keccak state locally,
+ *              rather than requiring support for multiple concurrent
+ *              Keccak states.
+ *
+ *              NOTE: Depending on the target CPU, this may reduce
+ *              performance when using software FIPS202 implementations.
+ *              Only enable this when you have to.
+ *
+ *****************************************************************************/
+#define MLD_CONFIG_SERIAL_FIPS202_ONLY
+
+/*************************  Config internals  ********************************/
+
+/* Default namespace
+ *
+ * Don't change this. If you need a different namespace, re-define
+ * MLD_CONFIG_NAMESPACE_PREFIX above instead, and remove the following.
+ *
+ * The default MLDSA namespace is
+ *
+ *   PQCP_MLDSA_NATIVE_MLDSA<LEVEL>_
+ *
+ * e.g., PQCP_MLDSA_NATIVE_MLDSA44_
+ */
+
+#if MLD_CONFIG_PARAMETER_SET == 44
+#define MLD_DEFAULT_NAMESPACE_PREFIX PQCP_MLDSA_NATIVE_MLDSA44
+#elif MLD_CONFIG_PARAMETER_SET == 65
+#define MLD_DEFAULT_NAMESPACE_PREFIX PQCP_MLDSA_NATIVE_MLDSA65
+#elif MLD_CONFIG_PARAMETER_SET == 87
+#define MLD_DEFAULT_NAMESPACE_PREFIX PQCP_MLDSA_NATIVE_MLDSA87
+#endif
+
+#endif /* !MLD_CONFIG_H */