diff --git a/mlkem/poly.c b/mlkem/poly.c
index 8f62b1a82..e6f6e93a4 100644
--- a/mlkem/poly.c
+++ b/mlkem/poly.c
@@ -23,9 +23,24 @@
 #define fqmul MLKEM_NAMESPACE(fqmul)
 #define barrett_reduce MLKEM_NAMESPACE(barrett_reduce)
 #define scalar_signed_to_unsigned_q MLKEM_NAMESPACE(scalar_signed_to_unsigned_q)
-#define ntt_butterfly_block MLKEM_NAMESPACE(ntt_butterfly_block)
-#define ntt_layer MLKEM_NAMESPACE(ntt_layer)
-#define invntt_layer MLKEM_NAMESPACE(invntt_layer)
+
+/* Forward NTT Internal functions */
+#define ct_butterfly MLKEM_NAMESPACE(ct_butterfly)
+#define ntt_layer123 MLKEM_NAMESPACE(ntt_layer123)
+#define ntt_layer45_butterfly MLKEM_NAMESPACE(ntt_layer45_butterfly)
+#define ntt_layer45 MLKEM_NAMESPACE(ntt_layer45)
+#define ntt_layer6 MLKEM_NAMESPACE(ntt_layer6)
+#define ntt_layer7 MLKEM_NAMESPACE(ntt_layer7)
+
+/* Inverse NTT Internal functions */
+#define gs_butterfly_reduce MLKEM_NAMESPACE(gs_butterfly_reduce)
+#define gs_butterfly_defer MLKEM_NAMESPACE(gs_butterfly_defer)
+#define invntt_layer7_invert MLKEM_NAMESPACE(invntt_layer7_invert)
+#define invntt_layer6 MLKEM_NAMESPACE(invntt_layer6)
+#define invntt_layer54_butterfly MLKEM_NAMESPACE(invntt_layer54_butterfly)
+#define invntt_layer54 MLKEM_NAMESPACE(invntt_layer54)
+#define invntt_layer321 MLKEM_NAMESPACE(invntt_layer321)
+
 /* End of static namespacing */
 
 #if !defined(MLKEM_USE_NATIVE_POLY_TOMONT) ||           \
@@ -263,133 +278,278 @@ void poly_mulcache_compute(poly_mulcache *x, const poly *a)
 #endif /* MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE */
 
 #if !defined(MLKEM_USE_NATIVE_NTT)
-/*
- * Computes a block CT butterflies with a fixed twiddle factor,
- * using Montgomery multiplication.
- * Parameters:
- * - r: Pointer to base of polynomial (_not_ the base of butterfly block)
- * - root: Twiddle factor to use for the butterfly. This must be in
- *         Montgomery form and signed canonical.
- * - start: Offset to the beginning of the butterfly block
- * - len: Index difference between coefficients subject to a butterfly
- * - bound: Ghost variable describing coefficient bound: Prior to `start`,
- *          coefficients must be bound by `bound + MLKEM_Q`. Post `start`,
- *          they must be bound by `bound`.
- * When this function returns, output coefficients in the index range
- * [start, start+2*len) have bound bumped to `bound + MLKEM_Q`.
- * Example:
- * - start=8, len=4
- *   This would compute the following four butterflies
- *          8     --    12
- *             9    --     13
- *                10   --     14
- *                   11   --     15
- * - start=4, len=2
- *   This would compute the following two butterflies
- *          4 -- 6
- *             5 -- 7
+
+/* 1.1 Forward NTT - Optimized C implementation
+ * --------------------------------------------
+ *
+ * Overview: this implementation aims to strike a balance
+ * between readability, formal verifification of type-safety,
+ * and performance.
+ *
+ * Layer merging
+ * -------------
+ * In this implementation:
+ *  Layers 1,2,3 and merged in function ntt_layer123()
+ *  Layers 4 and 5 are merged in function ntt_layer45()
+ *  Layer 6 stands alone in function ntt_layer6()
+ *  Layer 7 stands alone in function ntt_layer7()
+ *
+ * This particular merging was determined by experimentation
+ * and measurement of performance.
+ *
+ * Coefficient Reduction
+ * ---------------------
+ * The code defers reduction of coefficients in the core
+ * "butterfly" functions in each layer, so that the coefficients
+ * grow in absolute magnitiude by MLKEM_Q after each layer.
+ * This growth is reflected and verification in the contracts
+ * and loop invariants of each layer and their inner functions.
+ *
+ * Auto-Vectorization
+ * ------------------
+ * The code is written in a style that is amenable to auto-vectorization
+ * on targets that can support it, and using comtemporary compilers - for
+ * example, Graviton/AArch64 or Intel/AVX2 using recent versions of GCC
+ * or CLANG.
+ *
+ * Merging 3 layers results in an inner loop that proceses 8
+ * coefficients at a time. Similarly, merging 2 layers results
+ * in an inner loop that processes 4 coefficients at a time.
+ * Compiler for particlar targets may choose to further unroll
+ * or transform these loops as they see fit.
+ *
+ * Inlining of the inner "butterfly" functions is selectively enabled
+ * to allow a compiler to inline, to perform partial application, and
+ * vectorization of the top-level layer functions.
  */
-static void ntt_butterfly_block(int16_t r[MLKEM_N], int16_t zeta,
-                                unsigned start, unsigned len, int bound)
+#define NTT_BOUND1 (MLKEM_Q)
+#define NTT_BOUND2 (2 * MLKEM_Q)
+#define NTT_BOUND4 (4 * MLKEM_Q)
+#define NTT_BOUND6 (6 * MLKEM_Q)
+#define NTT_BOUND7 (7 * MLKEM_Q)
+#define NTT_BOUND8 (8 * MLKEM_Q)
+
+/* ct_butterfly() performs a single CT Butterfly step   */
+/* in polynomial denoted by r, using the coefficients   */
+/* indexed by coeff1_index and coeff2_index, and the    */
+/* given value of zeta.                                 */
+/*                                                      */
+/* NOTE that this function is marked INLINE for         */
+/* compilation (for efficiency) and does not have       */
+/* contracts, so it is "inlined for proof" by CBMC      */
+/* This allows CBMC to keep track of the ranges of the  */
+/* modified coefficients in the calling functions.      */
+static INLINE void ct_butterfly(int16_t r[MLKEM_N], const unsigned coeff1_index,
+                                const unsigned coeff2_index, const int16_t zeta)
+{
+  int16_t t1 = r[coeff1_index];
+  int16_t t2 = fqmul(r[coeff2_index], zeta);
+  r[coeff1_index] = t1 + t2;
+  r[coeff2_index] = t1 - t2;
+}
+
+static void ntt_layer123(int16_t r[MLKEM_N])
 __contract__(
-  requires(start < MLKEM_N)
-  requires(1 <= len && len <= MLKEM_N / 2 && start + 2 * len <= MLKEM_N)
-  requires(0 <= bound && bound < INT16_MAX - MLKEM_Q)
-  requires(-MLKEM_Q_HALF < zeta && zeta < MLKEM_Q_HALF)
   requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
-  requires(array_abs_bound(r, 0, start, bound + MLKEM_Q))
-  requires(array_abs_bound(r, start, MLKEM_N, bound))
+  requires(array_abs_bound(r, 0, MLKEM_N, NTT_BOUND1))
   assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
-  ensures(array_abs_bound(r, 0, start + 2*len, bound + MLKEM_Q))
-  ensures(array_abs_bound(r, start + 2 * len, MLKEM_N, bound)))
+  ensures(array_abs_bound(r, 0, MLKEM_N, NTT_BOUND4)))
 {
-  /* `bound` is a ghost variable only needed in the CBMC specification */
   unsigned j;
-  ((void)bound);
-  for (j = start; j < start + len; j++)
+  for (j = 0; j < 32; j++)
   __loop__(
-    invariant(start <= j && j <= start + len)
-    /*
-     * Coefficients are updated in strided pairs, so the bounds for the
-     * intermediate states alternate twice between the old and new bound
-     */
-    invariant(array_abs_bound(r, 0,           j,           bound + MLKEM_Q))
-    invariant(array_abs_bound(r, j,           start + len, bound))
-    invariant(array_abs_bound(r, start + len, j + len,     bound + MLKEM_Q))
-    invariant(array_abs_bound(r, j + len,     MLKEM_N,     bound)))
+    /* A single iteration of this loop updates 8 coefficients 3 times each,
+     * meaning their bound jumps from NTT_BOUND1 to NTT_BOUND4. Other (as yet
+     * untouched) coefficients remain bounded by NTT_BOUND1. When this loop
+     * terminates with j == 32, ALL the coefficients have been updated
+     * exactly 3 times, so ALL are bounded by NTT_BOUND4, which establishes
+     * the post-condition */
+    invariant(j <= 32)
+    invariant(array_abs_bound(r,       0,       j, NTT_BOUND4))
+    invariant(array_abs_bound(r,       j,      32, NTT_BOUND1))
+    invariant(array_abs_bound(r,      32,  j + 32, NTT_BOUND4))
+    invariant(array_abs_bound(r,  j + 32,      64, NTT_BOUND1))
+    invariant(array_abs_bound(r,      64,  j + 64, NTT_BOUND4))
+    invariant(array_abs_bound(r,  j + 64,      96, NTT_BOUND1))
+    invariant(array_abs_bound(r,      96,  j + 96, NTT_BOUND4))
+    invariant(array_abs_bound(r,  j + 96,     128, NTT_BOUND1))
+    invariant(array_abs_bound(r,     128, j + 128, NTT_BOUND4))
+    invariant(array_abs_bound(r, j + 128,     160, NTT_BOUND1))
+    invariant(array_abs_bound(r,     160, j + 160, NTT_BOUND4))
+    invariant(array_abs_bound(r, j + 160,     192, NTT_BOUND1))
+    invariant(array_abs_bound(r,     192, j + 192, NTT_BOUND4))
+    invariant(array_abs_bound(r, j + 192,     224, NTT_BOUND1))
+    invariant(array_abs_bound(r,     224, j + 224, NTT_BOUND4))
+    invariant(array_abs_bound(r, j + 224, MLKEM_N, NTT_BOUND1)))
   {
-    int16_t t;
-    t = fqmul(r[j + len], zeta);
-    r[j + len] = r[j] - t;
-    r[j] = r[j] + t;
+    /* 8 coeffifient indexes, starting at element j */
+    /* and increasing in strides of 32              */
+    const unsigned ci0 = j;
+    const unsigned ci1 = ci0 + 32;
+    const unsigned ci2 = ci0 + 64;
+    const unsigned ci3 = ci0 + 96;
+    const unsigned ci4 = ci0 + 128;
+    const unsigned ci5 = ci0 + 160;
+    const unsigned ci6 = ci0 + 192;
+    const unsigned ci7 = ci0 + 224;
+
+    /* Layer 1 */
+    ct_butterfly(r, ci0, ci4, zetas[1]);
+    ct_butterfly(r, ci1, ci5, zetas[1]);
+    ct_butterfly(r, ci2, ci6, zetas[1]);
+    ct_butterfly(r, ci3, ci7, zetas[1]);
+    /* Layer 2 */
+    ct_butterfly(r, ci0, ci2, zetas[2]);
+    ct_butterfly(r, ci1, ci3, zetas[2]);
+    ct_butterfly(r, ci4, ci6, zetas[3]);
+    ct_butterfly(r, ci5, ci7, zetas[3]);
+    /* Layer 3 */
+    ct_butterfly(r, ci0, ci1, zetas[4]);
+    ct_butterfly(r, ci2, ci3, zetas[5]);
+    ct_butterfly(r, ci4, ci5, zetas[6]);
+    ct_butterfly(r, ci6, ci7, zetas[7]);
   }
 }
 
-/*
- *Compute one layer of forward NTT
- * Parameters:
- * - r: Pointer to base of polynomial
- * - len: Stride of butterflies in this layer.
- * - layer: Ghost variable indicating which layer is being applied.
- *          Must match `len` via `len == MLKEM_N >> layer`.
- * Note: `len` could be dropped and computed in the function, but
- *   we are following the structure of the reference NTT from the
- *   official Kyber implementation here, merely adding `layer` as
- *   a ghost variable for the specifications.
- */
-static void ntt_layer(int16_t r[MLKEM_N], unsigned len, unsigned layer)
+static INLINE void ntt_layer45_butterfly(int16_t r[MLKEM_N],
+                                         const unsigned zeta_subtree_index,
+                                         const unsigned start)
+__contract__(
+  requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
+  requires(zeta_subtree_index <= 7)
+  requires(start <= 224)
+  requires(array_abs_bound(r,          0,   start, NTT_BOUND6))
+  requires(array_abs_bound(r,      start, MLKEM_N, NTT_BOUND4))
+  assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+  ensures (array_abs_bound(r,          0, start + 32, NTT_BOUND6))
+  ensures (array_abs_bound(r, start + 32,    MLKEM_N, NTT_BOUND4)))
+{
+  const unsigned l4zi = 8 + zeta_subtree_index;
+  const unsigned l5zi1 = l4zi * 2;
+  const unsigned l5zi2 = l5zi1 + 1;
+
+  const int16_t z1 = zetas[l4zi];
+  const int16_t z2 = zetas[l5zi1];
+  const int16_t z3 = zetas[l5zi2];
+
+  unsigned j;
+  for (j = 0; j < 8; j++)
+  __loop__(
+    invariant(j <= 8)
+    invariant(array_abs_bound(r,              0,          start, NTT_BOUND6))
+    invariant(array_abs_bound(r,      start + 0,      start + j, NTT_BOUND6))
+    invariant(array_abs_bound(r,      start + j,      start + 8, NTT_BOUND4))
+    invariant(array_abs_bound(r,      start + 8,  start + j + 8, NTT_BOUND6))
+    invariant(array_abs_bound(r,  start + j + 8,     start + 16, NTT_BOUND4))
+    invariant(array_abs_bound(r,     start + 16, start + j + 16, NTT_BOUND6))
+    invariant(array_abs_bound(r, start + j + 16,     start + 24, NTT_BOUND4))
+    invariant(array_abs_bound(r,     start + 24, start + j + 24, NTT_BOUND6))
+    invariant(array_abs_bound(r, start + j + 24,        MLKEM_N, NTT_BOUND4)))
+  {
+    /* 4 coeffifient indexes, starting at element j + start */
+    /* and increasing in strides of 8                       */
+    const unsigned ci1 = j + start;
+    const unsigned ci2 = ci1 + 8;
+    const unsigned ci3 = ci1 + 16;
+    const unsigned ci4 = ci1 + 24;
+
+    /* Layer 4 */
+    ct_butterfly(r, ci1, ci3, z1);
+    ct_butterfly(r, ci2, ci4, z1);
+    /* Layer 5 */
+    ct_butterfly(r, ci1, ci2, z2);
+    ct_butterfly(r, ci3, ci4, z3);
+  }
+}
+
+
+static void ntt_layer45(int16_t r[MLKEM_N])
+__contract__(
+  requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
+  requires(array_abs_bound(r, 0, MLKEM_N, NTT_BOUND4))
+  assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+  ensures(array_abs_bound(r, 0, MLKEM_N, NTT_BOUND6)))
+{
+  /* Manual unroll here to maximize opportunity to inline and partially apply
+   * inner functions. Also avoids a complicated loop invariant
+   */
+  ntt_layer45_butterfly(r, 0, 0);
+  ntt_layer45_butterfly(r, 1, 32);
+  ntt_layer45_butterfly(r, 2, 64);
+  ntt_layer45_butterfly(r, 3, 96);
+  ntt_layer45_butterfly(r, 4, 128);
+  ntt_layer45_butterfly(r, 5, 160);
+  ntt_layer45_butterfly(r, 6, 192);
+  ntt_layer45_butterfly(r, 7, 224);
+}
+
+static void ntt_layer6(int16_t r[MLKEM_N])
+__contract__(
+  requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
+  requires(array_abs_bound(r, 0, MLKEM_N, NTT_BOUND6))
+  assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+  ensures(array_abs_bound(r, 0, MLKEM_N, NTT_BOUND7)))
+{
+  unsigned j;
+  for (j = 0; j < 32; j++)
+  __loop__(
+    invariant(j <= 32)
+    invariant(array_abs_bound(r,     0,   j * 8, NTT_BOUND7))
+    invariant(array_abs_bound(r, j * 8, MLKEM_N, NTT_BOUND6)))
+  {
+    const int16_t zeta = zetas[j + 32];
+    const unsigned ci0 = j * 8;
+
+    /* Process 8 coefficients here, all of which need the same Zeta value */
+    ct_butterfly(r, ci0, ci0 + 4, zeta);
+    ct_butterfly(r, ci0 + 1, ci0 + 5, zeta);
+    ct_butterfly(r, ci0 + 2, ci0 + 6, zeta);
+    ct_butterfly(r, ci0 + 3, ci0 + 7, zeta);
+  }
+}
+
+static void ntt_layer7(int16_t r[MLKEM_N])
 __contract__(
   requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
-  requires(1 <= layer && layer <= 7 && len == (MLKEM_N >> layer))
-  requires(array_abs_bound(r, 0, MLKEM_N, layer * MLKEM_Q))
+  requires(array_abs_bound(r, 0, MLKEM_N, NTT_BOUND7))
   assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
-  ensures(array_abs_bound(r, 0, MLKEM_N, (layer + 1) * MLKEM_Q)))
+  ensures(array_abs_bound(r, 0, MLKEM_N, NTT_BOUND8)))
 {
-  unsigned start, k;
-  /* `layer` is a ghost variable only needed in the CBMC specification */
-  ((void)layer);
-  /* Twiddle factors for layer n start at index 2^(layer-1) */
-  k = MLKEM_N / (2 * len);
-  for (start = 0; start < MLKEM_N; start += 2 * len)
+  unsigned j;
+  for (j = 0; j < 64; j++)
   __loop__(
-    invariant(start < MLKEM_N + 2 * len)
-    invariant(k <= MLKEM_N / 2 && 2 * len * k == start + MLKEM_N)
-    invariant(array_abs_bound(r, 0, start, layer * MLKEM_Q + MLKEM_Q))
-    invariant(array_abs_bound(r, start, MLKEM_N, layer * MLKEM_Q)))
+    invariant(j <= 64)
+    invariant(array_abs_bound(r,     0,   j * 4, NTT_BOUND8))
+    invariant(array_abs_bound(r, j * 4, MLKEM_N, NTT_BOUND7)))
   {
-    int16_t zeta = zetas[k++];
-    ntt_butterfly_block(r, zeta, start, len, layer * MLKEM_Q);
+    const int16_t zeta = zetas[j + 64];
+    const unsigned ci0 = j * 4;
+
+    /* Process 4 coefficients here, all of which need the same Zeta value */
+    ct_butterfly(r, ci0, ci0 + 2, zeta);
+    ct_butterfly(r, ci0 + 1, ci0 + 3, zeta);
   }
 }
 
 /*
- * Compute full forward NTT
- * NOTE: This particular implementation satisfies a much tighter
- * bound on the output coefficients (5*q) than the contractual one (8*q),
- * but this is not needed in the calling code. Should we change the
- * base multiplication strategy to require smaller NTT output bounds,
- * the proof may need strengthening.
+ * Compute full Forward NTT
  */
-
 MLKEM_NATIVE_INTERNAL_API
 void poly_ntt(poly *p)
 {
-  unsigned len, layer;
   int16_t *r;
   debug_assert_abs_bound(p, MLKEM_N, MLKEM_Q);
   r = p->coeffs;
 
-  for (len = 128, layer = 1; len >= 2; len >>= 1, layer++)
-  __loop__(
-    invariant(1 <= layer && layer <= 8 && len == (MLKEM_N >> layer))
-    invariant(array_abs_bound(r, 0, MLKEM_N, layer * MLKEM_Q)))
-  {
-    ntt_layer(r, len, layer);
-  }
+  ntt_layer123(r);
+  ntt_layer45(r);
+  ntt_layer6(r);
+  ntt_layer7(r);
 
   /* Check the stronger bound */
   debug_assert_abs_bound(p, MLKEM_N, NTT_BOUND);
 }
+
 #else  /* MLKEM_USE_NATIVE_NTT */
 
 MLKEM_NATIVE_INTERNAL_API
@@ -403,74 +563,291 @@ void poly_ntt(poly *p)
 
 #if !defined(MLKEM_USE_NATIVE_INTT)
 
-/* Compute one layer of inverse NTT */
-static void invntt_layer(int16_t *r, unsigned len, unsigned layer)
+/* 2.1 Inverse NTT - Optimized C implementation
+ * --------------------------------------------
+ *
+ * Layer merging
+ * -------------
+ * In this implementation:
+ *  Layer 7 stands alone in function invntt_layer7_invert()
+ *  Layer 6 stands alone in function invntt_layer6()
+ *  Layers 5 and 4 are merged in function invntt_layer45()
+ *  Layers 3,2,1 and merged in function invntt_layer123()
+ *
+ * Coefficient Reduction
+ * ---------------------
+ * In the Inverse NTT, using the GS-Butterfly, coefficients
+ * do not grow linearly with respect to the layer numbering.
+ * Instead, some coefficients _double_ in absolute magnitude
+ * after each layer, meaning that more reduction steps are
+ * required to keep coefficients at or below 8*MLKEM_Q, which
+ * is the upper limit that can be accomodated in an int16_t object.
+ *
+ * The basic approach in this implementation is as follows:
+ *
+ * Layer 7 can accept any int16_t value for all coefficients
+ * as inputs, but inverts and reduces all coefficients,
+ * meaning inputs to Layer 6 are bounded by NTT_BOUND1.
+ *
+ * Layer 6 defers reduction, meaning all coefficents
+ * are bounded by NTT_BOUND2.
+ *
+ * Layers 5 and 4 are merged. Layer 5 defers reduction, meaning
+ * inputs to layer 4 are bounded by NTT_BOUND4. Layer 4 reduces
+ * all coefficeints so that inputs to layer 3 are bounded by
+ * NTT_BOUND1.
+ *
+ * Layers 3, 2, and 1 are merged. These all defer reduction,
+ * resulting in outputs bounded by NTT_BOUND8.
+ *
+ * These bounds are all reflected and verified by the contracts
+ * and loop invariants below.
+ *
+ * This layer merging and reduction strategy is NOT optimal, but
+ * offers a reasonable balance between performance, readability
+ * and verifiability of the code.
+ *
+ * Auto-Vectorization
+ * ------------------
+ *
+ * As with the Forward NTT, code is wr itten to handle at most
+ * 8 coefficents at once, with selective inlining to maximize
+ * opportunity for auto-vectorization.
+ */
+
+/* gs_butterfly_reduce() performs a single GS Butterfly */
+/* step in polynomial denoted by r, using the           */
+/* coefficients indexes coeff1_index and coeff2_index   */
+/* and the given value of zeta.                         */
+/*                                                      */
+/* Like ct_butterfly(), this functions is inlined       */
+/* for both compilation and proof.                      */
+static INLINE void gs_butterfly_reduce(int16_t r[MLKEM_N],
+                                       const unsigned coeff1_index,
+                                       const unsigned coeff2_index,
+                                       const int16_t zeta)
+{
+  const int16_t t1 = r[coeff1_index];
+  const int16_t t2 = r[coeff2_index];
+  r[coeff1_index] = barrett_reduce(t1 + t2);
+  r[coeff2_index] = fqmul((t2 - t1), zeta);
+}
+
+/* As gs_butterfly_reduce(), but does not reduce the */
+/* coefficient denoted by coeff1_index               */
+static INLINE void gs_butterfly_defer(int16_t r[MLKEM_N],
+                                      const unsigned coeff1_index,
+                                      const unsigned coeff2_index,
+                                      const int16_t zeta)
+{
+  const int16_t t1 = r[coeff1_index];
+  const int16_t t2 = r[coeff2_index];
+  r[coeff1_index] = t1 + t2;
+  r[coeff2_index] = fqmul((t2 - t1), zeta);
+}
+
+/*  MONT_F = mont^2/128 = 1441.                                */
+/*  Used to invert and reduce coefficients in the Inverse NTT. */
+#define MONT_F 1441
+
+static void invntt_layer7_invert(int16_t r[MLKEM_N])
 __contract__(
   requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
-  requires(2 <= len && len <= 128 && 1 <= layer && layer <= 7)
-  requires(len == (1 << (8 - layer)))
-  requires(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q))
   assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
-  ensures(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q)))
+  ensures(array_abs_bound(r, 0, MLKEM_N, NTT_BOUND1))
+)
 {
-  unsigned start, k;
-  /* `layer` is a ghost variable used only in the specification */
-  ((void)layer);
-  k = MLKEM_N / len - 1;
-  for (start = 0; start < MLKEM_N; start += 2 * len)
+  unsigned i;
+  for (i = 0; i < 64; i++)
   __loop__(
-    invariant(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q))
-    invariant(start <= MLKEM_N && k <= 127)
-    /* Normalised form of k == MLKEM_N / len - 1 - start / (2 * len) */
-    invariant(2 * len * k + start == 2 * MLKEM_N - 2 * len))
+    invariant(i <= 64)
+    invariant(array_abs_bound(r, 0, i * 4, NTT_BOUND1))
+  )
   {
-    unsigned j;
-    int16_t zeta = zetas[k--];
-    for (j = start; j < start + len; j++)
-    __loop__(
-      invariant(start <= j && j <= start + len)
-      invariant(start <= MLKEM_N && k <= 127)
-      invariant(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q)))
-    {
-      int16_t t = r[j];
-      r[j] = barrett_reduce(t + r[j + len]);
-      r[j + len] = r[j + len] - t;
-      r[j + len] = fqmul(r[j + len], zeta);
-    }
+    /* Process 4 coefficients here, all of which need the same Zeta value */
+    const int16_t zeta = zetas[127 - i];
+    const unsigned ci0 = i * 4;
+    const unsigned ci1 = ci0 + 1;
+    const unsigned ci2 = ci0 + 2;
+    const unsigned ci3 = ci0 + 3;
+
+    /* Invert and reduce all coefficients here the first time they */
+    /* are read. This is efficient, and also means we can accept   */
+    /* any int16_t value for all coefficients as input.            */
+    r[ci0] = fqmul(r[ci0], MONT_F);
+    r[ci1] = fqmul(r[ci1], MONT_F);
+    r[ci2] = fqmul(r[ci2], MONT_F);
+    r[ci3] = fqmul(r[ci3], MONT_F);
+
+    /* Reduce all coefficients here to meet the precondition of Layer 6 */
+    gs_butterfly_reduce(r, ci0, ci2, zeta);
+    gs_butterfly_reduce(r, ci1, ci3, zeta);
   }
 }
 
-MLKEM_NATIVE_INTERNAL_API
-void poly_invntt_tomont(poly *p)
+static void invntt_layer6(int16_t r[MLKEM_N])
+__contract__(
+  requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
+  requires(array_abs_bound(r, 0, MLKEM_N, NTT_BOUND1))
+  assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+  ensures(array_abs_bound(r, 0, MLKEM_N, NTT_BOUND2))
+)
 {
-  /*
-   * Scale input polynomial to account for Montgomery factor
-   * and NTT twist. This also brings coefficients down to
-   * absolute value < MLKEM_Q.
-   */
-  unsigned j, len, layer;
-  const int16_t f = 1441;
-  int16_t *r = p->coeffs;
+  unsigned i;
+  for (i = 0; i < 32; i++)
+  __loop__(
+    invariant(i <= 32)
+    invariant(array_abs_bound(r, 0,       i * 8, NTT_BOUND2))
+    invariant(array_abs_bound(r, i * 8, MLKEM_N, NTT_BOUND1))
+  )
+  {
+    const int16_t zeta = zetas[63 - i];
+    const unsigned ci0 = i * 8;
+
+    /* Process 8 coefficients here, all of which need the same Zeta value */
+    /* Defer reduction of coefficients 0, 1, 2, and 3 here so they        */
+    /* are bounded to NTT_BOUND2 after Layer6                             */
+    gs_butterfly_defer(r, ci0, ci0 + 4, zeta);
+    gs_butterfly_defer(r, ci0 + 1, ci0 + 5, zeta);
+    gs_butterfly_defer(r, ci0 + 2, ci0 + 6, zeta);
+    gs_butterfly_defer(r, ci0 + 3, ci0 + 7, zeta);
+  }
+}
+
 
-  for (j = 0; j < MLKEM_N; j++)
+static INLINE void invntt_layer54_butterfly(int16_t r[MLKEM_N],
+                                            const unsigned zeta_index,
+                                            const unsigned start)
+__contract__(
+  requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
+  requires(zeta_index <= 7)
+  requires(start <= 224)
+  requires(start % 32 == 0)
+  requires(array_abs_bound(r, 0,       start, NTT_BOUND1))
+  requires(array_abs_bound(r, start, MLKEM_N, NTT_BOUND2))
+  assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+  ensures(array_abs_bound(r, 0,          start + 32, NTT_BOUND1))
+  ensures(array_abs_bound(r, start + 32,    MLKEM_N, NTT_BOUND2))
+)
+{
+  const unsigned l4zi = 8 + zeta_index;
+  const unsigned l5zi1 = l4zi * 2;
+  const unsigned l5zi2 = l5zi1 + 1;
+
+  const int16_t l4zeta = zetas[l4zi];
+  const int16_t l5zeta1 = zetas[l5zi1];
+  const int16_t l5zeta2 = zetas[l5zi2];
+
+  unsigned j;
+  for (j = 0; j < 8; j++)
   __loop__(
-    invariant(j <= MLKEM_N)
-    invariant(array_abs_bound(r, 0, j, MLKEM_Q)))
+    invariant(j <= 8)
+    invariant(array_abs_bound(r,              0,          start, NTT_BOUND1))
+    invariant(array_abs_bound(r,      start + 0,      start + j, NTT_BOUND1))
+    invariant(array_abs_bound(r,      start + j,      start + 8, NTT_BOUND2))
+    invariant(array_abs_bound(r,      start + 8,  start + j + 8, NTT_BOUND1))
+    invariant(array_abs_bound(r,  start + j + 8,     start + 16, NTT_BOUND2))
+    invariant(array_abs_bound(r,     start + 16, start + j + 16, NTT_BOUND1))
+    invariant(array_abs_bound(r, start + j + 16,     start + 24, NTT_BOUND2))
+    invariant(array_abs_bound(r,     start + 24, start + j + 24, NTT_BOUND1))
+    invariant(array_abs_bound(r, start + j + 24,        MLKEM_N, NTT_BOUND2)))
   {
-    r[j] = fqmul(r[j], f);
+    const unsigned ci0 = j + start;
+    const unsigned ci8 = ci0 + 8;
+    const unsigned ci16 = ci0 + 16;
+    const unsigned ci24 = ci0 + 24;
+
+    /* Layer 5 - Defer reduction of coeffs 0 and 16 here */
+    gs_butterfly_defer(r, ci0, ci8, l5zeta2);
+    gs_butterfly_defer(r, ci16, ci24, l5zeta1);
+    /* Layer 4 - reduce all coefficients to be in NTT_BOUND1 */
+    /* to meet the pre-condition of Layer321                 */
+    gs_butterfly_reduce(r, ci0, ci16, l4zeta);
+    gs_butterfly_reduce(r, ci8, ci24, l4zeta);
   }
+}
 
-  /* Run the invNTT layers */
-  for (len = 2, layer = 7; len <= 128; len <<= 1, layer--)
+static void invntt_layer54(int16_t r[MLKEM_N])
+__contract__(
+  requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
+  requires(array_abs_bound(r, 0, MLKEM_N, NTT_BOUND2))
+  assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+  ensures(array_abs_bound(r, 0, MLKEM_N, NTT_BOUND1))
+)
+{
+  /* Manual unroll here to maximize opportunity to inline and partially apply
+   * inner functions. Also avoids a complicated loop invariant
+   */
+  invntt_layer54_butterfly(r, 7, 0);
+  invntt_layer54_butterfly(r, 6, 32);
+  invntt_layer54_butterfly(r, 5, 64);
+  invntt_layer54_butterfly(r, 4, 96);
+  invntt_layer54_butterfly(r, 3, 128);
+  invntt_layer54_butterfly(r, 2, 160);
+  invntt_layer54_butterfly(r, 1, 192);
+  invntt_layer54_butterfly(r, 0, 224);
+}
+
+static void invntt_layer321(int16_t r[MLKEM_N])
+__contract__(
+  requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
+  requires(array_abs_bound(r, 0, MLKEM_N, NTT_BOUND1))
+  assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+  ensures(array_abs_bound(r, 0, MLKEM_N, NTT_BOUND8)))
+{
+  unsigned j;
+  for (j = 0; j < 32; j++)
   __loop__(
-    invariant(2 <= len && len <= 256 && layer <= 7 && len == (1 << (8 - layer)))
-    invariant(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q)))
+    invariant(j <= 32)
+    invariant(array_abs_bound(r,       0,       j, NTT_BOUND8))
+    invariant(array_abs_bound(r,       j,      32, NTT_BOUND1))
+    invariant(array_abs_bound(r,      32,  j + 32, NTT_BOUND4))
+    invariant(array_abs_bound(r,  j + 32,      64, NTT_BOUND1))
+    invariant(array_abs_bound(r,      64,  j + 64, NTT_BOUND2))
+    invariant(array_abs_bound(r,  j + 64,      96, NTT_BOUND1))
+    invariant(array_abs_bound(r,      96,  j + 96, NTT_BOUND2))
+    invariant(array_abs_bound(r,  j + 96,     128, NTT_BOUND1))
+    invariant(array_abs_bound(r,     128, MLKEM_N, NTT_BOUND1)))
   {
-    invntt_layer(p->coeffs, len, layer);
+    const unsigned ci0 = j + 0;
+    const unsigned ci32 = j + 32;
+    const unsigned ci64 = j + 64;
+    const unsigned ci96 = j + 96;
+    const unsigned ci128 = j + 128;
+    const unsigned ci160 = j + 160;
+    const unsigned ci192 = j + 192;
+    const unsigned ci224 = j + 224;
+
+    /* Layer 3 */
+    gs_butterfly_defer(r, ci0, ci32, zetas[7]);
+    gs_butterfly_defer(r, ci64, ci96, zetas[6]);
+    gs_butterfly_defer(r, ci128, ci160, zetas[5]);
+    gs_butterfly_defer(r, ci192, ci224, zetas[4]);
+    /* Layer 2 */
+    gs_butterfly_defer(r, ci0, ci64, zetas[3]);
+    gs_butterfly_defer(r, ci32, ci96, zetas[3]);
+    gs_butterfly_defer(r, ci128, ci192, zetas[2]);
+    gs_butterfly_defer(r, ci160, ci224, zetas[2]);
+    /* Layer 1 */
+    gs_butterfly_defer(r, ci0, ci128, zetas[1]);
+    gs_butterfly_defer(r, ci32, ci160, zetas[1]);
+    gs_butterfly_defer(r, ci64, ci192, zetas[1]);
+    gs_butterfly_defer(r, ci96, ci224, zetas[1]);
   }
+}
+
+MLKEM_NATIVE_INTERNAL_API
+void poly_invntt_tomont(poly *p)
+{
+  int16_t *r = p->coeffs;
+  invntt_layer7_invert(r);
+  invntt_layer6(r);
+  invntt_layer54(r);
+  invntt_layer321(r);
 
   debug_assert_abs_bound(p, MLKEM_N, INVNTT_BOUND);
 }
+
 #else  /* MLKEM_USE_NATIVE_INTT */
 
 MLKEM_NATIVE_INTERNAL_API
@@ -492,6 +869,23 @@ MLKEM_NATIVE_EMPTY_CU(poly)
 #undef fqmul
 #undef barrett_reduce
 #undef scalar_signed_to_unsigned_q
-#undef ntt_butterfly_block
-#undef ntt_layer
-#undef invntt_layer
+#undef ct_butterfly
+#undef ntt_layer123
+#undef ntt_layer45_butterfly
+#undef ntt_layer45
+#undef ntt_layer6
+#undef ntt_layer7
+#undef gs_butterfly_reduce
+#undef gs_butterfly_defer
+#undef invntt_layer7_invert
+#undef invntt_layer6
+#undef invntt_layer54_butterfly
+#undef invntt_layer54
+#undef invntt_layer321
+#undef NTT_BOUND1
+#undef NTT_BOUND2
+#undef NTT_BOUND4
+#undef NTT_BOUND6
+#undef NTT_BOUND7
+#undef NTT_BOUND8
+#undef MONT_F
diff --git a/proofs/cbmc/invntt_layer/invntt_layer_harness.c b/proofs/cbmc/invntt_layer/invntt_layer_harness.c
deleted file mode 100644
index 053d33f51..000000000
--- a/proofs/cbmc/invntt_layer/invntt_layer_harness.c
+++ /dev/null
@@ -1,16 +0,0 @@
-// Copyright (c) 2024-2025 The mlkem-native project authors
-// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-// SPDX-License-Identifier: MIT-0
-
-#include <stdint.h>
-#include "common.h"
-
-#define invntt_layer MLKEM_NAMESPACE(invntt_layer)
-void invntt_layer(int16_t *p, unsigned len, unsigned layer);
-
-void harness(void)
-{
-  int16_t *a;
-  unsigned len, layer;
-  invntt_layer(a, len, layer);
-}
diff --git a/proofs/cbmc/invntt_layer321/Makefile b/proofs/cbmc/invntt_layer321/Makefile
new file mode 100644
index 000000000..f025d1f9f
--- /dev/null
+++ b/proofs/cbmc/invntt_layer321/Makefile
@@ -0,0 +1,55 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = invntt_layer321_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 = invntt_layer321
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer321
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--bitwuzla
+
+FUNCTION_NAME = $(MLKEM_NAMESPACE)invntt_layer321
+
+# 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
+# ("mlkem/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/invntt_layer/cbmc-proof.txt b/proofs/cbmc/invntt_layer321/cbmc-proof.txt
similarity index 100%
rename from proofs/cbmc/invntt_layer/cbmc-proof.txt
rename to proofs/cbmc/invntt_layer321/cbmc-proof.txt
diff --git a/proofs/cbmc/invntt_layer321/invntt_layer321_harness.c b/proofs/cbmc/invntt_layer321/invntt_layer321_harness.c
new file mode 100644
index 000000000..aa6b25f93
--- /dev/null
+++ b/proofs/cbmc/invntt_layer321/invntt_layer321_harness.c
@@ -0,0 +1,18 @@
+// Copyright (c) 2024-2025 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <poly.h>
+
+#define invntt_layer321 MLKEM_NAMESPACE(invntt_layer321)
+void invntt_layer321(int16_t *r);
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void)
+{
+  int16_t *a;
+  invntt_layer321(a);
+}
diff --git a/proofs/cbmc/invntt_layer54/Makefile b/proofs/cbmc/invntt_layer54/Makefile
new file mode 100644
index 000000000..34bd1006e
--- /dev/null
+++ b/proofs/cbmc/invntt_layer54/Makefile
@@ -0,0 +1,54 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = invntt_layer54_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 = invntt_layer54
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer54
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer54_butterfly
+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 = $(MLKEM_NAMESPACE)invntt_layer54
+
+# 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
+# ("mlkem/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/ntt_butterfly_block/cbmc-proof.txt b/proofs/cbmc/invntt_layer54/cbmc-proof.txt
similarity index 100%
rename from proofs/cbmc/ntt_butterfly_block/cbmc-proof.txt
rename to proofs/cbmc/invntt_layer54/cbmc-proof.txt
diff --git a/proofs/cbmc/invntt_layer54/invntt_layer54_harness.c b/proofs/cbmc/invntt_layer54/invntt_layer54_harness.c
new file mode 100644
index 000000000..ba97cd397
--- /dev/null
+++ b/proofs/cbmc/invntt_layer54/invntt_layer54_harness.c
@@ -0,0 +1,18 @@
+// Copyright (c) 2024-2025 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <poly.h>
+
+#define invntt_layer54 MLKEM_NAMESPACE(invntt_layer54)
+void invntt_layer54(int16_t *r);
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void)
+{
+  int16_t *a;
+  invntt_layer54(a);
+}
diff --git a/proofs/cbmc/invntt_layer54_butterfly/Makefile b/proofs/cbmc/invntt_layer54_butterfly/Makefile
new file mode 100644
index 000000000..f8a0aaedf
--- /dev/null
+++ b/proofs/cbmc/invntt_layer54_butterfly/Makefile
@@ -0,0 +1,55 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = invntt_layer54_butterfly_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 = invntt_layer54_butterfly
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer54_butterfly
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul $(MLKEM_NAMESPACE)barrett_reduce
+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 = $(MLKEM_NAMESPACE)invntt_layer54_butterfly
+
+# 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
+# ("mlkem/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/ntt_layer/cbmc-proof.txt b/proofs/cbmc/invntt_layer54_butterfly/cbmc-proof.txt
similarity index 100%
rename from proofs/cbmc/ntt_layer/cbmc-proof.txt
rename to proofs/cbmc/invntt_layer54_butterfly/cbmc-proof.txt
diff --git a/proofs/cbmc/invntt_layer54_butterfly/invntt_layer54_butterfly_harness.c b/proofs/cbmc/invntt_layer54_butterfly/invntt_layer54_butterfly_harness.c
new file mode 100644
index 000000000..9aeca0ab3
--- /dev/null
+++ b/proofs/cbmc/invntt_layer54_butterfly/invntt_layer54_butterfly_harness.c
@@ -0,0 +1,21 @@
+// Copyright (c) 2024-2025 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <poly.h>
+
+#define invntt_layer54_butterfly MLKEM_NAMESPACE(invntt_layer54_butterfly)
+void invntt_layer54_butterfly(int16_t r[MLKEM_N], const unsigned zeta_index,
+                              const unsigned start);
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void)
+{
+  int16_t *a;
+  unsigned zi;
+  unsigned start;
+  invntt_layer54_butterfly(a, zi, start);
+}
diff --git a/proofs/cbmc/invntt_layer6/Makefile b/proofs/cbmc/invntt_layer6/Makefile
new file mode 100644
index 000000000..ad3f84316
--- /dev/null
+++ b/proofs/cbmc/invntt_layer6/Makefile
@@ -0,0 +1,55 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = invntt_layer6_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 = invntt_layer6
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer6
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul
+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 = $(MLKEM_NAMESPACE)invntt_layer6
+
+# 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
+# ("mlkem/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/invntt_layer6/cbmc-proof.txt b/proofs/cbmc/invntt_layer6/cbmc-proof.txt
new file mode 100644
index 000000000..3d1913ebf
--- /dev/null
+++ b/proofs/cbmc/invntt_layer6/cbmc-proof.txt
@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.
diff --git a/proofs/cbmc/invntt_layer6/invntt_layer6_harness.c b/proofs/cbmc/invntt_layer6/invntt_layer6_harness.c
new file mode 100644
index 000000000..95d7a2861
--- /dev/null
+++ b/proofs/cbmc/invntt_layer6/invntt_layer6_harness.c
@@ -0,0 +1,18 @@
+// Copyright (c) 2024-2025 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <poly.h>
+
+#define invntt_layer6 MLKEM_NAMESPACE(invntt_layer6)
+void invntt_layer6(int16_t *r);
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void)
+{
+  int16_t *a;
+  invntt_layer6(a);
+}
diff --git a/proofs/cbmc/invntt_layer/Makefile b/proofs/cbmc/invntt_layer7_invert/Makefile
similarity index 87%
rename from proofs/cbmc/invntt_layer/Makefile
rename to proofs/cbmc/invntt_layer7_invert/Makefile
index fde0e1370..cfb18d7b5 100644
--- a/proofs/cbmc/invntt_layer/Makefile
+++ b/proofs/cbmc/invntt_layer7_invert/Makefile
@@ -3,11 +3,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = invntt_layer_harness
+HARNESS_FILE = invntt_layer7_invert_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 = invntt_layer
+PROOF_UID = invntt_layer7_invert
 
 DEFINES +=
 INCLUDES +=
@@ -16,9 +16,10 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c $(SRCDIR)/mlkem/zetas.c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer7_invert
 USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul $(MLKEM_NAMESPACE)barrett_reduce
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
@@ -27,7 +28,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-FUNCTION_NAME = invntt_layer
+FUNCTION_NAME = invntt_layer7_invert
 
 # 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
diff --git a/proofs/cbmc/invntt_layer7_invert/cbmc-proof.txt b/proofs/cbmc/invntt_layer7_invert/cbmc-proof.txt
new file mode 100644
index 000000000..3d1913ebf
--- /dev/null
+++ b/proofs/cbmc/invntt_layer7_invert/cbmc-proof.txt
@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.
diff --git a/proofs/cbmc/invntt_layer7_invert/invntt_layer7_invert_harness.c b/proofs/cbmc/invntt_layer7_invert/invntt_layer7_invert_harness.c
new file mode 100644
index 000000000..93c1b8735
--- /dev/null
+++ b/proofs/cbmc/invntt_layer7_invert/invntt_layer7_invert_harness.c
@@ -0,0 +1,18 @@
+// Copyright (c) 2024-2025 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <poly.h>
+
+#define invntt_layer7_invert MLKEM_NAMESPACE(invntt_layer7_invert)
+void invntt_layer7_invert(int16_t *r);
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void)
+{
+  int16_t *a;
+  invntt_layer7_invert(a);
+}
diff --git a/proofs/cbmc/ntt_butterfly_block/ntt_butterfly_block_harness.c b/proofs/cbmc/ntt_butterfly_block/ntt_butterfly_block_harness.c
deleted file mode 100644
index 129f49141..000000000
--- a/proofs/cbmc/ntt_butterfly_block/ntt_butterfly_block_harness.c
+++ /dev/null
@@ -1,18 +0,0 @@
-// Copyright (c) 2024-2025 The mlkem-native project authors
-// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-// SPDX-License-Identifier: MIT-0
-
-#include <stdint.h>
-#include "common.h"
-
-#define ntt_butterfly_block MLKEM_NAMESPACE(ntt_butterfly_block)
-void ntt_butterfly_block(int16_t *r, int16_t root, unsigned start, unsigned len,
-                         int bound);
-
-void harness(void)
-{
-  int16_t *r, root;
-  unsigned start, stride;
-  int bound;
-  ntt_butterfly_block(r, root, start, stride, bound);
-}
diff --git a/proofs/cbmc/ntt_layer123/Makefile b/proofs/cbmc/ntt_layer123/Makefile
new file mode 100644
index 000000000..b35f575e7
--- /dev/null
+++ b/proofs/cbmc/ntt_layer123/Makefile
@@ -0,0 +1,55 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = ntt_layer123_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 = ntt_layer123
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_layer123
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul
+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 = $(MLKEM_NAMESPACE)ntt_layer123
+
+# 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
+# ("mlkem/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/ntt_layer123/cbmc-proof.txt b/proofs/cbmc/ntt_layer123/cbmc-proof.txt
new file mode 100644
index 000000000..3d1913ebf
--- /dev/null
+++ b/proofs/cbmc/ntt_layer123/cbmc-proof.txt
@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.
diff --git a/proofs/cbmc/ntt_layer123/ntt_layer123_harness.c b/proofs/cbmc/ntt_layer123/ntt_layer123_harness.c
new file mode 100644
index 000000000..b75825f00
--- /dev/null
+++ b/proofs/cbmc/ntt_layer123/ntt_layer123_harness.c
@@ -0,0 +1,18 @@
+// Copyright (c) 2024-2025 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <poly.h>
+
+#define ntt_layer123 MLKEM_NAMESPACE(ntt_layer123)
+void ntt_layer123(int16_t *r);
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void)
+{
+  int16_t *a;
+  ntt_layer123(a);
+}
diff --git a/proofs/cbmc/ntt_layer/Makefile b/proofs/cbmc/ntt_layer45/Makefile
similarity index 85%
rename from proofs/cbmc/ntt_layer/Makefile
rename to proofs/cbmc/ntt_layer45/Makefile
index 86632eabb..c465d4e2c 100644
--- a/proofs/cbmc/ntt_layer/Makefile
+++ b/proofs/cbmc/ntt_layer45/Makefile
@@ -3,11 +3,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = ntt_layer_harness
+HARNESS_FILE = ntt_layer45_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 = ntt_layer
+PROOF_UID = ntt_layer45
 
 DEFINES +=
 INCLUDES +=
@@ -16,10 +16,10 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c $(SRCDIR)/mlkem/zetas.c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_layer
-USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_butterfly_block
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_layer45
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_layer45_butterfly
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
@@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-FUNCTION_NAME = ntt_layer
+FUNCTION_NAME = $(MLKEM_NAMESPACE)ntt_layer45
 
 # 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
@@ -36,7 +36,7 @@ FUNCTION_NAME = ntt_layer
 # 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/ntt_layer45/cbmc-proof.txt b/proofs/cbmc/ntt_layer45/cbmc-proof.txt
new file mode 100644
index 000000000..3d1913ebf
--- /dev/null
+++ b/proofs/cbmc/ntt_layer45/cbmc-proof.txt
@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.
diff --git a/proofs/cbmc/ntt_layer/ntt_layer_harness.c b/proofs/cbmc/ntt_layer45/ntt_layer45_harness.c
similarity index 54%
rename from proofs/cbmc/ntt_layer/ntt_layer_harness.c
rename to proofs/cbmc/ntt_layer45/ntt_layer45_harness.c
index 8e6b0bc0e..fb76f2dd7 100644
--- a/proofs/cbmc/ntt_layer/ntt_layer_harness.c
+++ b/proofs/cbmc/ntt_layer45/ntt_layer45_harness.c
@@ -2,14 +2,17 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: MIT-0
 
-#include "poly.h"
+#include <poly.h>
 
-#define ntt_layer MLKEM_NAMESPACE(ntt_layer)
-void ntt_layer(int16_t *p, unsigned len, unsigned layer);
+#define ntt_layer45 MLKEM_NAMESPACE(ntt_layer45)
+void ntt_layer45(int16_t *r);
 
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
 void harness(void)
 {
   int16_t *a;
-  unsigned len, layer;
-  ntt_layer(a, len, layer);
+  ntt_layer45(a);
 }
diff --git a/proofs/cbmc/ntt_layer45_butterfly/Makefile b/proofs/cbmc/ntt_layer45_butterfly/Makefile
new file mode 100644
index 000000000..e88619b3d
--- /dev/null
+++ b/proofs/cbmc/ntt_layer45_butterfly/Makefile
@@ -0,0 +1,55 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = ntt_layer45_butterfly_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 = ntt_layer45_butterfly
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_layer45_butterfly
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--bitwuzla
+
+FUNCTION_NAME = $(MLKEM_NAMESPACE)ntt_layer45_butterfly
+
+# 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
+# ("mlkem/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/ntt_layer45_butterfly/cbmc-proof.txt b/proofs/cbmc/ntt_layer45_butterfly/cbmc-proof.txt
new file mode 100644
index 000000000..3d1913ebf
--- /dev/null
+++ b/proofs/cbmc/ntt_layer45_butterfly/cbmc-proof.txt
@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.
diff --git a/proofs/cbmc/ntt_layer45_butterfly/ntt_layer45_butterfly_harness.c b/proofs/cbmc/ntt_layer45_butterfly/ntt_layer45_butterfly_harness.c
new file mode 100644
index 000000000..62f42e2b4
--- /dev/null
+++ b/proofs/cbmc/ntt_layer45_butterfly/ntt_layer45_butterfly_harness.c
@@ -0,0 +1,22 @@
+// Copyright (c) 2024-2025 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <poly.h>
+
+#define ntt_layer45_butterfly MLKEM_NAMESPACE(ntt_layer45_butterfly)
+void ntt_layer45_butterfly(int16_t r[MLKEM_N],
+                           const unsigned zeta_subtree_index,
+                           const unsigned start);
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void)
+{
+  int16_t *a;
+  unsigned zi;
+  unsigned start;
+  ntt_layer45_butterfly(a, zi, start);
+}
diff --git a/proofs/cbmc/ntt_butterfly_block/Makefile b/proofs/cbmc/ntt_layer6/Makefile
similarity index 88%
rename from proofs/cbmc/ntt_butterfly_block/Makefile
rename to proofs/cbmc/ntt_layer6/Makefile
index aa1fadd8a..224f3fe3b 100644
--- a/proofs/cbmc/ntt_butterfly_block/Makefile
+++ b/proofs/cbmc/ntt_layer6/Makefile
@@ -3,11 +3,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = ntt_butterfly_block_harness
+HARNESS_FILE = ntt_layer6_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 = ntt_butterfly_block
+PROOF_UID = ntt_layer6
 
 DEFINES +=
 INCLUDES +=
@@ -16,9 +16,10 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_butterfly_block
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_layer6
 USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
@@ -27,7 +28,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-FUNCTION_NAME = ntt_butterfly_block
+FUNCTION_NAME = $(MLKEM_NAMESPACE)ntt_layer6
 
 # 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
@@ -36,7 +37,7 @@ FUNCTION_NAME = ntt_butterfly_block
 # EXPENSIVE = true
 
 # This function is large enough to need...
-CBMC_OBJECT_BITS = 9
+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/ntt_layer6/cbmc-proof.txt b/proofs/cbmc/ntt_layer6/cbmc-proof.txt
new file mode 100644
index 000000000..3d1913ebf
--- /dev/null
+++ b/proofs/cbmc/ntt_layer6/cbmc-proof.txt
@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.
diff --git a/proofs/cbmc/ntt_layer6/ntt_layer6_harness.c b/proofs/cbmc/ntt_layer6/ntt_layer6_harness.c
new file mode 100644
index 000000000..380766ed7
--- /dev/null
+++ b/proofs/cbmc/ntt_layer6/ntt_layer6_harness.c
@@ -0,0 +1,18 @@
+// Copyright (c) 2024-2025 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <poly.h>
+
+#define ntt_layer6 MLKEM_NAMESPACE(ntt_layer6)
+void ntt_layer6(int16_t *r);
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void)
+{
+  int16_t *a;
+  ntt_layer6(a);
+}
diff --git a/proofs/cbmc/ntt_layer7/Makefile b/proofs/cbmc/ntt_layer7/Makefile
new file mode 100644
index 000000000..1478ab70a
--- /dev/null
+++ b/proofs/cbmc/ntt_layer7/Makefile
@@ -0,0 +1,55 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = ntt_layer7_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 = ntt_layer7
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_layer7
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--bitwuzla
+
+FUNCTION_NAME = $(MLKEM_NAMESPACE)ntt_layer7
+
+# 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
+# ("mlkem/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/ntt_layer7/cbmc-proof.txt b/proofs/cbmc/ntt_layer7/cbmc-proof.txt
new file mode 100644
index 000000000..3d1913ebf
--- /dev/null
+++ b/proofs/cbmc/ntt_layer7/cbmc-proof.txt
@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.
diff --git a/proofs/cbmc/ntt_layer7/ntt_layer7_harness.c b/proofs/cbmc/ntt_layer7/ntt_layer7_harness.c
new file mode 100644
index 000000000..c5f0acf20
--- /dev/null
+++ b/proofs/cbmc/ntt_layer7/ntt_layer7_harness.c
@@ -0,0 +1,18 @@
+// Copyright (c) 2024-2025 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <poly.h>
+
+#define ntt_layer7 MLKEM_NAMESPACE(ntt_layer7)
+void ntt_layer7(int16_t *r);
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void)
+{
+  int16_t *a;
+  ntt_layer7(a);
+}
diff --git a/proofs/cbmc/poly_invntt_tomont/Makefile b/proofs/cbmc/poly_invntt_tomont/Makefile
index 6772c2112..9ae1a0f9b 100644
--- a/proofs/cbmc/poly_invntt_tomont/Makefile
+++ b/proofs/cbmc/poly_invntt_tomont/Makefile
@@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_invntt_tomont
-USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer $(MLKEM_NAMESPACE)fqmul
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer321 $(MLKEM_NAMESPACE)invntt_layer54 $(MLKEM_NAMESPACE)invntt_layer6 $(MLKEM_NAMESPACE)invntt_layer7_invert
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
diff --git a/proofs/cbmc/poly_ntt/Makefile b/proofs/cbmc/poly_ntt/Makefile
index 1ee5f2742..874e57191 100644
--- a/proofs/cbmc/poly_ntt/Makefile
+++ b/proofs/cbmc/poly_ntt/Makefile
@@ -18,8 +18,8 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
- CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_ntt
-USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_layer
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_ntt
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_layer123 $(MLKEM_NAMESPACE)ntt_layer45 $(MLKEM_NAMESPACE)ntt_layer6 $(MLKEM_NAMESPACE)ntt_layer7
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1