diff --git a/crypto/stark/benches/profile_prover.rs b/crypto/stark/benches/profile_prover.rs
index dbff24440..f5438877e 100644
--- a/crypto/stark/benches/profile_prover.rs
+++ b/crypto/stark/benches/profile_prover.rs
@@ -21,6 +21,7 @@ fn main() {
         fri_number_of_queries: 100,
         coset_offset: 3,
         grinding_factor: 0,
+        fri_final_poly_log_degree: 7,
     };
 
     let num_columns = 16;
diff --git a/crypto/stark/benches/prover_benchmark.rs b/crypto/stark/benches/prover_benchmark.rs
index 2729fff29..c152e7dbb 100644
--- a/crypto/stark/benches/prover_benchmark.rs
+++ b/crypto/stark/benches/prover_benchmark.rs
@@ -61,6 +61,7 @@ fn benchmark_proof_options() -> ProofOptions {
         fri_number_of_queries: 30,
         coset_offset: 3,
         grinding_factor: 0,
+        fri_final_poly_log_degree: 7,
     }
 }
 
diff --git a/crypto/stark/src/fri/mod.rs b/crypto/stark/src/fri/mod.rs
index 60ad2a398..d5314b71d 100644
--- a/crypto/stark/src/fri/mod.rs
+++ b/crypto/stark/src/fri/mod.rs
@@ -1,6 +1,7 @@
 pub mod fri_commitment;
 pub mod fri_decommit;
 pub(crate) mod fri_functions;
+pub(crate) mod terminal;
 
 use crypto::fiat_shamir::is_transcript::IsStarkTranscript;
 use math::field::element::FieldElement;
@@ -16,8 +17,9 @@ use self::fri_functions::{
 };
 
 /// FRI commit phase from pre-computed bit-reversed evaluations, skipping the
-/// initial FFT. Use this when the caller already has the evaluation vector
-/// (e.g. from a fused LDE pipeline).
+/// initial FFT. Stops folding when the remaining codeword encodes a polynomial
+/// of degree < 2^`final_poly_log_degree` with blowup 2^`blowup_log`, and
+/// returns the coefficient vector of that terminal polynomial.
 ///
 /// The `T: Clone` and `F/E: 'static` bounds are required by the cuda GPU
 /// fast path (`try_fri_commit_gpu` snapshots the transcript and TypeId-
@@ -25,16 +27,19 @@ use self::fri_functions::{
 /// in builds without the `cuda` feature) to keep one stable signature.
 pub fn commit_phase_from_evaluations<
     F: IsFFTField + IsSubFieldOf<E> + 'static,
-    E: IsField + 'static,
+    E: IsField + 'static + Send + Sync,
     T: IsStarkTranscript<E, F> + Clone,
 >(
-    number_layers: usize,
+    // `_number_layers`: retained for signature stability with the cuda fast path; termination is now driven by blowup_log + final_poly_log_degree.
+    _number_layers: usize,
     mut evals: Vec<FieldElement<E>>,
     transcript: &mut T,
     coset_offset: &FieldElement<F>,
     domain_size: usize,
+    blowup_log: u32,
+    final_poly_log_degree: u32,
 ) -> (
-    FieldElement<E>,
+    Vec<FieldElement<E>>,
     Vec<FriLayer<E, FriLayerMerkleTreeBackend<E>>>,
 )
 where
@@ -50,27 +55,39 @@ where
     // had never been tried.
     #[cfg(feature = "cuda")]
     {
+        // GPU FRI commit is disabled unconditionally (see `try_fri_commit_gpu`
+        // in gpu_lde.rs for the full explanation). The CPU fallback below
+        // handles all cases correctly, including early termination.
         if let Some(result) = crate::gpu_lde::try_fri_commit_gpu::<F, E, T>(
-            number_layers,
+            _number_layers,
             &evals,
             transcript,
             coset_offset,
             domain_size,
+            blowup_log,
+            final_poly_log_degree,
         ) {
             return result;
         }
     }
 
+    // Determine how many total folds are needed to reach the terminal codeword.
+    // terminal_len = 2^(blowup_log + k), clamped to initial_len for tiny inputs.
+    let initial_len = evals.len();
+    let k = final_poly_log_degree as usize;
+    let terminal_len = ((1usize << blowup_log) << k).min(initial_len);
+    let total_folds = (initial_len / terminal_len).trailing_zeros() as usize;
+    let num_committed = total_folds.saturating_sub(1);
+
     // Inverse twiddle factors for evaluation-form folding.
     let mut inv_twiddles = compute_coset_twiddles_inv(coset_offset, domain_size);
+    let mut fri_layer_list = Vec::with_capacity(num_committed);
+    // Track the coset offset as it squares with each fold (needed for iFFT in terminal).
+    let mut terminal_offset = coset_offset.clone();
 
-    // The loop commits `number_layers - 1` folded layers; the final fold below
-    // produces the (uncommitted) last value.
-    let num_committed_layers = number_layers.saturating_sub(1);
-    let mut fri_layer_list = Vec::with_capacity(num_committed_layers);
-
-    for _ in 0..num_committed_layers {
-        // <<<< Receive challenge 𝜁ₖ₋₁
+    // Commit `num_committed` folded layers to the transcript.
+    for _ in 0..num_committed {
+        // <<<< Receive challenge 𝜁ₖ
         let zeta = transcript.sample_field_element();
 
         // Fold evaluations in-place (no FFT needed).
@@ -89,25 +106,42 @@ where
         // >>>> Send commitment: [pₖ]
         transcript.append_bytes(&root);
 
-        // Update twiddles for the next level.
+        // Update twiddles and offset for the next level.
         update_twiddles_in_place(&mut inv_twiddles);
+        terminal_offset = terminal_offset.square();
     }
 
-    // <<<< Receive challenge: 𝜁ₙ₋₁
-    let zeta = transcript.sample_field_element();
-
-    // Final fold.
-    fold_evaluations_in_place(&mut evals, &zeta, &inv_twiddles);
-
-    let last_value = evals
-        .first()
-        .expect("FRI evals are non-empty after folding")
-        .clone();
-
-    // >>>> Send value: pₙ
-    transcript.append_field_element(&last_value);
+    // One final fold to reach the terminal codeword (size terminal_len), unless
+    // already there (total_folds == 0 means initial_len == terminal_len).
+    if total_folds > 0 {
+        // <<<< Receive challenge: 𝜁_final
+        let zeta = transcript.sample_field_element();
+        fold_evaluations_in_place(&mut evals, &zeta, &inv_twiddles);
+        terminal_offset = terminal_offset.square();
+    }
+    debug_assert_eq!(evals.len(), terminal_len, "terminal codeword size mismatch");
+
+    // Recover the low-degree polynomial coefficients from the terminal codeword
+    // and send them to the verifier.
+    //
+    // The number of coefficients is determined by the *actual* terminal codeword,
+    // not the requested `final_poly_log_degree`: for tiny inputs `terminal_len`
+    // is clamped to `initial_len`, so the terminal polynomial has degree
+    // < terminal_len / 2^blowup_log = 2^(log2(terminal_len) - blowup_log). Using
+    // this clamped exponent keeps the coefficient count in lockstep with what the
+    // verifier reconstructs (`expected_k = min(k, trace_bits)`); passing the raw
+    // `final_poly_log_degree` would over-pad with zeros and break the round-trip.
+    let effective_log_degree = terminal_len.trailing_zeros() - blowup_log;
+    let final_poly_coeffs = crate::fri::terminal::coeffs_from_terminal_codeword::<F, E>(
+        &evals,
+        &terminal_offset,
+        effective_log_degree,
+    );
+    for c in &final_poly_coeffs {
+        transcript.append_field_element(c);
+    }
 
-    (last_value, fri_layer_list)
+    (final_poly_coeffs, fri_layer_list)
 }
 
 pub fn query_phase<F: IsField>(
diff --git a/crypto/stark/src/fri/terminal.rs b/crypto/stark/src/fri/terminal.rs
new file mode 100644
index 000000000..650f23dc5
--- /dev/null
+++ b/crypto/stark/src/fri/terminal.rs
@@ -0,0 +1,109 @@
+//! Conversion helpers between a FRI terminal codeword and the coefficients of
+//! the low-degree polynomial it encodes.
+//!
+//! These are pure, self-contained helpers — no transcript, no FRI logic.
+//! They are used by the prover (`commit_phase_from_evaluations`) and verifier FRI step.
+
+use math::fft::bit_reversing::in_place_bit_reverse_permute;
+use math::field::element::FieldElement;
+use math::field::traits::{IsFFTField, IsField, IsSubFieldOf};
+use math::polynomial::Polynomial;
+
+/// Prover side: given a FRI terminal codeword in **bit-reversed** order,
+/// recover the `2^final_poly_log_degree` coefficients of the underlying
+/// low-degree polynomial.
+///
+/// The codeword is a coset evaluation of a polynomial of degree less than
+/// `2^final_poly_log_degree` on the coset `terminal_offset·⟨ω⟩` of size
+/// `blowup·2^k`.
+///
+/// Algorithm:
+/// 1. Bit-reverse permute to convert from FRI order to natural (DFT) order.
+/// 2. Decimate: extract the size-`2^k` sub-coset
+///    `terminal_offset·⟨ω^blowup⟩` = every `blowup`-th natural-order point.
+/// 3. Coset iFFT on the small (`2^k`-point) sub-domain — a `blowup×`-smaller
+///    transform that recovers the `2^k` coefficients directly (no oversized
+///    transform and no wasteful truncation).
+pub(crate) fn coeffs_from_terminal_codeword<F, E>(
+    codeword_bitrev: &[FieldElement<E>],
+    terminal_offset: &FieldElement<F>,
+    final_poly_log_degree: u32,
+) -> Vec<FieldElement<E>>
+where
+    F: IsFFTField + IsSubFieldOf<E>,
+    E: IsField + Send + Sync,
+{
+    // Bit-reversed -> natural order.
+    let mut natural = codeword_bitrev.to_vec();
+    in_place_bit_reverse_permute(&mut natural);
+
+    // A degree-<2^k poly is determined by 2^k points: take the size-2^k sub-coset
+    // terminal_offset*<w^blowup> = every `blowup`-th natural-order evaluation.
+    let keep = 1usize << final_poly_log_degree;
+    let blowup = natural.len() / keep;
+    let sub_coset: Vec<FieldElement<E>> = natural.into_iter().step_by(blowup).collect();
+    debug_assert_eq!(sub_coset.len(), keep);
+
+    // Coset iFFT on the small domain -> the 2^k coefficients directly (no oversized trim).
+    let poly = Polynomial::interpolate_offset_fft::<F>(&sub_coset, terminal_offset)
+        .expect("terminal sub-coset must have power-of-two length and non-zero offset");
+
+    // Pad with zeros only if interpolation dropped trailing-zero coeffs, so the
+    // proof always carries exactly 2^k coefficients (the verifier length-checks).
+    let mut coeffs = poly.coefficients().to_vec();
+    coeffs.resize(keep, FieldElement::<E>::zero());
+    coeffs
+}
+
+/// Verifier side: given `2^k` coefficients of the low-degree polynomial,
+/// reconstruct the full FRI terminal codeword in **bit-reversed** order.
+///
+/// Algorithm:
+/// 1. FFT (coset): evaluate the polynomial on the full coset of size
+///    `codeword_len` with shift `terminal_offset` to get natural order.
+/// 2. Bit-reverse permute to convert natural order to FRI order.
+///
+/// # Panics
+///
+/// Panics if any of the following preconditions are violated:
+/// - `coeffs` is non-empty,
+/// - `coeffs.len()` is a power of two,
+/// - `codeword_len` is a power of two,
+/// - `coeffs.len() <= codeword_len`, and
+/// - `codeword_len` is divisible by `coeffs.len()`.
+///
+/// In the normal verifier flow these conditions are guaranteed by the
+/// final-polynomial length check that the verifier performs before calling
+/// this helper, so the assert should never fire in production.
+pub(crate) fn terminal_codeword_from_coeffs<F, E>(
+    coeffs: &[FieldElement<E>],
+    terminal_offset: &FieldElement<F>,
+    codeword_len: usize,
+) -> Vec<FieldElement<E>>
+where
+    F: IsFFTField + IsSubFieldOf<E>,
+    E: IsField + Send + Sync,
+{
+    assert!(
+        !coeffs.is_empty()
+            && coeffs.len().is_power_of_two()
+            && codeword_len.is_power_of_two()
+            && coeffs.len() <= codeword_len
+            && codeword_len % coeffs.len() == 0,
+        "terminal_codeword_from_coeffs: coeffs.len() ({}) must be a non-zero power of two dividing codeword_len ({}); the verifier must length-check coeffs before calling",
+        coeffs.len(),
+        codeword_len,
+    );
+
+    let poly = Polynomial::new(coeffs);
+    let blowup = codeword_len / coeffs.len();
+
+    // Step 1: coset FFT to get natural-order evaluations.
+    let mut natural =
+        Polynomial::evaluate_offset_fft::<F>(&poly, blowup, Some(coeffs.len()), terminal_offset)
+            .expect("terminal coset size must be a power of two within the field's two-adicity");
+
+    // Step 2: convert natural order to bit-reversed (FRI) order.
+    in_place_bit_reverse_permute(&mut natural);
+    natural
+}
diff --git a/crypto/stark/src/gpu_lde.rs b/crypto/stark/src/gpu_lde.rs
index 36756b40b..c83682d66 100644
--- a/crypto/stark/src/gpu_lde.rs
+++ b/crypto/stark/src/gpu_lde.rs
@@ -1518,14 +1518,17 @@ where
 /// it would have produced had the GPU never been tried. This requires the
 /// concrete transcript type to support snapshot semantics via `Clone`.
 #[allow(clippy::type_complexity)]
+#[allow(unreachable_code)]
 pub(crate) fn try_fri_commit_gpu<F, E, T>(
     number_layers: usize,
     evals: &[FieldElement<E>],
     transcript: &mut T,
     coset_offset: &FieldElement<F>,
     domain_size: usize,
+    _blowup_log: u32,
+    _final_poly_log_degree: u32,
 ) -> Option<(
-    FieldElement<E>,
+    Vec<FieldElement<E>>,
     Vec<FriLayer<E, FriLayerMerkleTreeBackend<E>>>,
 )>
 where
@@ -1535,6 +1538,36 @@ where
     FieldElement<E>: AsBytes,
     T: IsStarkTranscript<E, F> + Clone,
 {
+    // GPU FRI commit is disabled unconditionally; the CPU loop in
+    // `commit_phase_from_evaluations` handles all cases correctly.
+    //
+    // Re-enabling the GPU path requires non-trivial changes that cannot be
+    // tested without a CUDA build -- keeping an incorrect GPU path would
+    // silently produce wrong proofs. The three specific mismatches are:
+    //
+    //   1. Fold-count mismatch: the old GPU body derives the number of committed
+    //      layers from `number_layers` (the superseded parameter, passed in as
+    //      `_number_layers` by the caller). The new protocol computes fold count
+    //      from `_blowup_log` + `_final_poly_log_degree`, as the CPU path does;
+    //      `_number_layers` is no longer authoritative.
+    //
+    //   2. Terminal extraction mismatch: the old body calls `state.fold_final()`
+    //      and takes the FIRST element of the result. The CPU path calls
+    //      `coeffs_from_terminal_codeword`, which runs a proper iFFT on the full
+    //      terminal codeword and returns all polynomial coefficients. This
+    //      mismatch would produce a wrong transcript even for K==0
+    //      (`_final_poly_log_degree == 0`).
+    //
+    //   3. Early termination (K>0): the GPU kernel folds all the way to a single
+    //      element; it does not know how to stop at a codeword of length
+    //      2^(`_blowup_log` + `_final_poly_log_degree`). Adding this requires
+    //      new math-cuda API surface.
+    //
+    // The old body is preserved below as a template for a future task that
+    // implements proper CUDA early-termination and validates it with a full
+    // cuda build + byte-identical proof test.
+    return None;
+
     if TypeId::of::<F>() != TypeId::of::<GoldilocksField>() {
         return None;
     }
@@ -1636,5 +1669,8 @@ where
     transcript.append_field_element(&last_value);
 
     GPU_FRI_CALLS.fetch_add(1, Ordering::Relaxed);
-    Some((last_value, fri_layer_list))
+    // TODO(task7): emit real final-polynomial coefficients here. This wrapping
+    // is only to satisfy the new return type; the path is unreachable (disabled
+    // by the early `return None` above).
+    Some((vec![last_value], fri_layer_list))
 }
diff --git a/crypto/stark/src/proof/options.rs b/crypto/stark/src/proof/options.rs
index 70976b993..4624943e8 100644
--- a/crypto/stark/src/proof/options.rs
+++ b/crypto/stark/src/proof/options.rs
@@ -38,6 +38,7 @@ impl fmt::Display for ProofOptionsError {
 /// - `fri_number_of_queries`: the number of queries for the FRI layer
 /// - `coset_offset`: the offset for the coset
 /// - `grinding_factor`: the number of leading zeros that we want for the Hash(hash || nonce)
+/// - `fri_final_poly_log_degree`: log2 degree bound at which FRI terminates folding
 #[cfg_attr(feature = "wasm", wasm_bindgen)]
 #[derive(Clone, Debug, serde::Serialize, serde::Deserialize)]
 pub struct ProofOptions {
@@ -45,6 +46,10 @@ pub struct ProofOptions {
     pub fri_number_of_queries: usize,
     pub coset_offset: u64,
     pub grinding_factor: u8,
+    /// Log2 of the FRI final-polynomial degree bound. FRI stops folding when the
+    /// polynomial has degree < 2^fri_final_poly_log_degree; the prover sends those
+    /// 2^k coefficients instead of folding to a constant.
+    pub fri_final_poly_log_degree: u8,
 }
 
 impl ProofOptions {
@@ -56,6 +61,7 @@ impl ProofOptions {
             fri_number_of_queries: 3,
             coset_offset: 3,
             grinding_factor: 1,
+            fri_final_poly_log_degree: DEFAULT_FRI_FINAL_POLY_LOG_DEGREE,
         }
     }
 }
@@ -75,6 +81,9 @@ impl ProofOptions {
 /// security bottleneck — field size is not.
 pub struct GoldilocksCubicProofOptions;
 
+// Shared by both ProofOptions::default_test_options and GoldilocksCubicProofOptions::with_params.
+const DEFAULT_FRI_FINAL_POLY_LOG_DEGREE: u8 = 7;
+
 impl GoldilocksCubicProofOptions {
     const DEFAULT_GRINDING: u8 = 20;
 
@@ -112,6 +121,7 @@ impl GoldilocksCubicProofOptions {
             fri_number_of_queries,
             coset_offset: 3,
             grinding_factor,
+            fri_final_poly_log_degree: DEFAULT_FRI_FINAL_POLY_LOG_DEGREE,
         })
     }
 }
diff --git a/crypto/stark/src/proof/stark.rs b/crypto/stark/src/proof/stark.rs
index 1751d60fe..0271bd918 100644
--- a/crypto/stark/src/proof/stark.rs
+++ b/crypto/stark/src/proof/stark.rs
@@ -52,8 +52,8 @@ pub struct StarkProof<F: IsSubFieldOf<E>, E: IsField, PI> {
     pub composition_poly_parts_ood_evaluation: Vec<FieldElement<E>>,
     // [pₖ]
     pub fri_layers_merkle_roots: Vec<Commitment>,
-    // pₙ
-    pub fri_last_value: FieldElement<E>,
+    /// Coefficients of the FRI final polynomial (degree < 2^k).
+    pub fri_final_poly_coeffs: Vec<FieldElement<E>>,
     // Open(pₖ(Dₖ), −𝜐ₛ^(2ᵏ))
     pub query_list: Vec<FriDecommitment<E>>,
     // Open(H₁(D_LDE, 𝜐ᵢ), Open(H₂(D_LDE, 𝜐ᵢ), Open(tⱼ(D_LDE), 𝜐ᵢ)
diff --git a/crypto/stark/src/prover.rs b/crypto/stark/src/prover.rs
index 4da57559c..64e2079a5 100644
--- a/crypto/stark/src/prover.rs
+++ b/crypto/stark/src/prover.rs
@@ -354,8 +354,9 @@ pub(crate) struct Round3<F: IsField> {
 
 /// A container for the results of the fourth round of the STARK Prove protocol.
 pub(crate) struct Round4<F: IsSubFieldOf<E>, E: IsField> {
-    /// The final value resulting from folding the Deep composition polynomial all the way down to a constant value.
-    fri_last_value: FieldElement<E>,
+    /// Coefficients of the FRI final polynomial (degree < 2^k), emitted once
+    /// folding reaches the terminal codeword.
+    fri_final_poly_coeffs: Vec<FieldElement<E>>,
     /// The commitments to the fold polynomials of the inner layers of FRI.
     fri_layers_merkle_roots: Vec<Commitment>,
     /// The values and proofs of validity of the evaluations of the trace polynomials and the composition polynomials
@@ -1244,12 +1245,14 @@ pub trait IsStarkProver<
         // FRI commit phase from pre-computed evaluations
         #[cfg(feature = "instruments")]
         let t_sub = Instant::now();
-        let (fri_last_value, fri_layers) = fri::commit_phase_from_evaluations(
+        let (fri_final_poly_coeffs, fri_layers) = fri::commit_phase_from_evaluations(
             domain.root_order as usize,
             lde_evals,
             transcript,
             &coset_offset,
             domain_size,
+            (domain.blowup_factor as usize).trailing_zeros(),
+            air.options().fri_final_poly_log_degree as u32,
         );
         #[cfg(feature = "instruments")]
         let r4_merkle_dur = t_sub.elapsed();
@@ -1286,7 +1289,7 @@ pub trait IsStarkProver<
         }
 
         Round4 {
-            fri_last_value,
+            fri_final_poly_coeffs,
             fri_layers_merkle_roots,
             deep_poly_openings,
             query_list,
@@ -2365,8 +2368,8 @@ pub trait IsStarkProver<
                 .composition_poly_parts_ood_evaluation,
             // [pₖ]
             fri_layers_merkle_roots: round_4_result.fri_layers_merkle_roots,
-            // pₙ
-            fri_last_value: round_4_result.fri_last_value,
+            // FRI final polynomial coefficients
+            fri_final_poly_coeffs: round_4_result.fri_final_poly_coeffs,
             // Open(p₀(D₀), 𝜐ₛ), Open(pₖ(Dₖ), −𝜐ₛ^(2ᵏ))
             query_list: round_4_result.query_list,
             // Open(H₁(D_LDE, 𝜐₀), Open(H₂(D_LDE, 𝜐₀), Open(tⱼ(D_LDE), 𝜐₀)
diff --git a/crypto/stark/src/tests/fri_tests.rs b/crypto/stark/src/tests/fri_tests.rs
index 503d0946a..7ef1f5910 100644
--- a/crypto/stark/src/tests/fri_tests.rs
+++ b/crypto/stark/src/tests/fri_tests.rs
@@ -131,3 +131,128 @@ fn test_eval_fold_matches_coeff_fold() {
 
     assert_eq!(path_a_evals, path_b_evals);
 }
+
+/// FRI commit-phase early-termination roundtrip.
+///
+/// Builds a known low-degree FRI codeword, runs `commit_phase_from_evaluations`
+/// with `blowup_log = 1`, `final_poly_log_degree = 2`, and checks:
+///   * the emitted final polynomial has exactly `2^final_poly_log_degree` coeffs,
+///   * the number of committed FRI layers equals `total_folds - 1`,
+///   * folding each queried evaluation through the committed layers reaches the
+///     reconstructed terminal codeword at the query's terminal-layer position.
+#[test]
+fn test_commit_phase_early_termination_roundtrip() {
+    use crate::fri::fri_functions::update_twiddles_in_place;
+    use crate::fri::terminal::terminal_codeword_from_coeffs;
+    use crate::fri::{commit_phase_from_evaluations, query_phase};
+    use crypto::fiat_shamir::default_transcript::DefaultTranscript;
+    use crypto::fiat_shamir::is_transcript::IsTranscript;
+    use math::fft::bit_reversing::reverse_index;
+    use math::field::traits::IsFFTField;
+
+    type F = GoldilocksField;
+
+    let blowup_log: u32 = 1;
+    let final_poly_log_degree: u32 = 2;
+    let initial_len = 64usize;
+    let root_order = initial_len.trailing_zeros(); // 6
+    let total_folds = (root_order - (blowup_log + final_poly_log_degree)) as usize; // 3
+    let num_committed = total_folds - 1; // 2
+
+    let offset = FE::from(3u64);
+
+    // Degree-<32 polynomial; with blowup 2 its terminal poly has degree < 2^2 = 4,
+    // so the emitted 2^2 coefficients capture it exactly.
+    let coeffs_in: Vec<FE> = (1u64..=32).map(FE::new).collect();
+    let poly = Polynomial::new(&coeffs_in);
+
+    // Coset LDE (blowup 2) -> natural order -> bit-reverse -> FRI-order codeword.
+    let mut codeword =
+        Polynomial::evaluate_offset_fft::<F>(&poly, 2, Some(32), &offset).expect("LDE FFT");
+    in_place_bit_reverse_permute(&mut codeword);
+    assert_eq!(codeword.len(), initial_len);
+
+    // ---- Commit phase with early termination ----
+    let mut transcript = DefaultTranscript::<F>::new(&[]);
+    let (final_poly_coeffs, fri_layers) = commit_phase_from_evaluations::<F, F, _>(
+        root_order as usize,
+        codeword.clone(),
+        &mut transcript,
+        &offset,
+        initial_len,
+        blowup_log,
+        final_poly_log_degree,
+    );
+
+    assert_eq!(
+        final_poly_coeffs.len(),
+        1 << final_poly_log_degree,
+        "final poly must have 2^k coefficients"
+    );
+    assert_eq!(
+        fri_layers.len(),
+        num_committed,
+        "committed layers must equal total_folds - 1"
+    );
+
+    // query_phase must still work against the committed layers.
+    let iotas = vec![0usize, 1, 5, 17, 30];
+    let _decommitments = query_phase(&fri_layers, &iotas);
+
+    // ---- Reconstruct terminal codeword from the emitted coefficients ----
+    let terminal_len = (1usize << blowup_log) << final_poly_log_degree; // 8
+    let terminal_offset = offset.pow(1u64 << total_folds); // offset^(2^3)
+    let terminal_codeword =
+        terminal_codeword_from_coeffs::<F, F>(&final_poly_coeffs, &terminal_offset, terminal_len);
+    assert_eq!(terminal_codeword.len(), terminal_len);
+
+    // Re-derive the prover's folding challenges by replaying the transcript.
+    let mut replay = DefaultTranscript::<F>::new(&[]);
+    let mut zetas: Vec<FE> = Vec::with_capacity(total_folds);
+    for layer in &fri_layers {
+        zetas.push(replay.sample_field_element());
+        replay.append_bytes(&layer.merkle_tree.root);
+    }
+    zetas.push(replay.sample_field_element()); // final-fold challenge
+    assert_eq!(zetas.len(), total_folds);
+
+    // Strong check: folding the whole codeword with those challenges reproduces
+    // the reconstructed terminal codeword.
+    let mut refold = codeword.clone();
+    let mut inv_tw = compute_coset_twiddles_inv::<F>(&offset, initial_len);
+    for zeta in zetas.iter().take(total_folds) {
+        fold_evaluations_in_place(&mut refold, zeta, &inv_tw);
+        update_twiddles_in_place(&mut inv_tw);
+    }
+    assert_eq!(
+        refold, terminal_codeword,
+        "full re-fold must match reconstructed terminal codeword"
+    );
+
+    // Per-query check: replicate the verifier's fold path and land on
+    // terminal_codeword[index] at the terminal-layer position.
+    let omega = F::get_primitive_root_of_unity(root_order as u64).expect("root of unity");
+    for &iota in &iotas {
+        // p0(nu) and p0(-nu) live at FRI-order positions 2*iota and 2*iota+1.
+        let p0 = codeword[2 * iota].clone();
+        let p0_sym = codeword[2 * iota + 1].clone();
+        // nu = offset * omega^reverse_index(2*iota, initial_len)
+        let nu = &offset * omega.pow(reverse_index(2 * iota, initial_len as u64) as u64);
+        let nu_inv = nu.inv().expect("evaluation point is non-zero");
+
+        // Fold layer 0 -> 1 using the first challenge.
+        let mut v = (&p0 + &p0_sym) + &nu_inv * &zetas[0] * (&p0 - &p0_sym);
+        let mut index = iota;
+        let mut ep_inv = nu_inv.square(); // nu^{-2} for the first committed layer
+        for (i, layer) in fri_layers.iter().enumerate() {
+            let sym = layer.evaluation[index ^ 1].clone();
+            v = (&v + &sym) + &ep_inv * &zetas[i + 1] * (&v - &sym);
+            index >>= 1;
+            ep_inv = ep_inv.square();
+        }
+        assert_eq!(
+            v, terminal_codeword[index],
+            "query {iota}: folded value must equal terminal_codeword[{index}]"
+        );
+    }
+}
diff --git a/crypto/stark/src/tests/mod.rs b/crypto/stark/src/tests/mod.rs
index 8c0897ac1..60241fd02 100644
--- a/crypto/stark/src/tests/mod.rs
+++ b/crypto/stark/src/tests/mod.rs
@@ -11,5 +11,6 @@ pub mod prover_tests;
 pub mod small_trace_tests;
 #[cfg(feature = "disk-spill")]
 pub mod table_disk_spill_tests;
+pub mod terminal_tests;
 pub mod trace_test_helpers;
 pub mod transition_tests;
diff --git a/crypto/stark/src/tests/proof_options_tests.rs b/crypto/stark/src/tests/proof_options_tests.rs
index ff7c7cc87..e898f9b05 100644
--- a/crypto/stark/src/tests/proof_options_tests.rs
+++ b/crypto/stark/src/tests/proof_options_tests.rs
@@ -122,4 +122,16 @@ fn test_options_unchanged() {
     assert_eq!(opts.blowup_factor, 2);
     assert_eq!(opts.fri_number_of_queries, 3);
     assert_eq!(opts.grinding_factor, 1);
+    assert_eq!(opts.fri_final_poly_log_degree, 7);
+}
+
+#[test]
+fn with_blowup_sets_default_final_poly_log_degree() {
+    let opts = GoldilocksCubicProofOptions::with_blowup(2).expect("valid blowup");
+    assert_eq!(opts.fri_final_poly_log_degree, 7);
+}
+
+#[test]
+fn default_test_options_sets_final_poly_log_degree() {
+    assert_eq!(ProofOptions::default_test_options().fri_final_poly_log_degree, 7);
 }
diff --git a/crypto/stark/src/tests/prover_tests.rs b/crypto/stark/src/tests/prover_tests.rs
index 7c8972eeb..4cda3a7b7 100644
--- a/crypto/stark/src/tests/prover_tests.rs
+++ b/crypto/stark/src/tests/prover_tests.rs
@@ -35,6 +35,7 @@ fn test_domain_constructor() {
         fri_number_of_queries: 1,
         coset_offset,
         grinding_factor,
+        fri_final_poly_log_degree: 7,
     };
 
     let domain = Domain::new(
@@ -126,6 +127,7 @@ fn barycentric_trace_eval_matches_horner_trace_eval() {
         fri_number_of_queries: 1,
         coset_offset,
         grinding_factor: 0,
+        fri_final_poly_log_degree: 7,
     };
 
     let air = simple_fibonacci::FibonacciAIR::<GoldilocksField>::new(&proof_options);
@@ -197,6 +199,7 @@ fn test_decompose_and_extend_d2_matches_original() {
         fri_number_of_queries: 1,
         coset_offset: 3,
         grinding_factor: 0,
+        fri_final_poly_log_degree: 7,
     };
 
     // We need an AIR with composition_poly_degree_bound = 2 * trace_length.
@@ -257,12 +260,14 @@ fn test_multi_prove_mixed_coset_offsets() {
         fri_number_of_queries: 3,
         coset_offset: 3,
         grinding_factor: 1,
+        fri_final_poly_log_degree: 7,
     };
     let proof_options_7 = ProofOptions {
         blowup_factor: 2,
         fri_number_of_queries: 3,
         coset_offset: 7,
         grinding_factor: 1,
+        fri_final_poly_log_degree: 7,
     };
 
     // Both AIRs have the same trace length and blowup, but different coset offsets.
@@ -327,6 +332,7 @@ fn test_multi_prove_dedups_shared_domain_params() {
         fri_number_of_queries: 3,
         coset_offset: 3,
         grinding_factor: 1,
+        fri_final_poly_log_degree: 7,
     };
 
     let mut trace_1 = simple_fibonacci::fibonacci_trace([Felt::from(1), Felt::from(1)], 8);
@@ -417,6 +423,7 @@ fn test_deep_poly_direct_2n_matches_interpolate_fft_extend() {
         fri_number_of_queries: 1,
         coset_offset: 3,
         grinding_factor: 0,
+        fri_final_poly_log_degree: 7,
     };
 
     let air = QuadraticAIR::<GoldilocksField>::new(&proof_options);
diff --git a/crypto/stark/src/tests/small_trace_tests.rs b/crypto/stark/src/tests/small_trace_tests.rs
index 8373ae9d6..1a25fd507 100644
--- a/crypto/stark/src/tests/small_trace_tests.rs
+++ b/crypto/stark/src/tests/small_trace_tests.rs
@@ -92,6 +92,104 @@ fn test_prove_verify_two_rows() {
     );
 }
 
+/// Prove + verify with DEFAULT options (K=7) and a trace large enough that FRI
+/// actually folds (trace_bits = 10 > 7). This exercises the full early-termination
+/// path: committed FRI layers, a final fold, and terminal-codeword reconstruction
+/// from the emitted final-polynomial coefficients.
+#[test_log::test]
+fn test_prove_verify_folding_default_options() {
+    let mut trace = simple_addition_trace::<GoldilocksField>(1024);
+    let proof_options = ProofOptions::default_test_options();
+    let pub_inputs = SimpleAdditionPublicInputs {
+        a: Felt::from(1u64),
+        b: Felt::from(2u64),
+    };
+    let air = SimpleAdditionAIR::<GoldilocksField>::new(&proof_options);
+
+    let proof = Prover::prove(
+        &air,
+        &mut trace,
+        &pub_inputs,
+        &mut DefaultTranscript::<GoldilocksField>::new(&[]),
+    )
+    .unwrap();
+
+    assert!(
+        Verifier::verify(
+            &proof,
+            &air,
+            &mut DefaultTranscript::<GoldilocksField>::new(&[])
+        ),
+        "Verification failed for a folding trace under default options (K=7)"
+    );
+}
+
+/// Prove + verify with DEFAULT options (K=7) and a tiny trace (trace_bits = 3 <= 7)
+/// so the FRI final-polynomial degree is clamped (`expected_k = min(k, trace_bits)`)
+/// and no folding happens (`total_folds == 0`). The terminal codeword is the deep
+/// composition codeword itself and the verifier checks the deep evaluations against
+/// it directly.
+#[test_log::test]
+fn test_prove_verify_tiny_trace_clamp() {
+    let mut trace = simple_addition_trace::<GoldilocksField>(8);
+    let proof_options = ProofOptions::default_test_options();
+    let pub_inputs = SimpleAdditionPublicInputs {
+        a: Felt::from(1u64),
+        b: Felt::from(2u64),
+    };
+    let air = SimpleAdditionAIR::<GoldilocksField>::new(&proof_options);
+
+    let proof = Prover::prove(
+        &air,
+        &mut trace,
+        &pub_inputs,
+        &mut DefaultTranscript::<GoldilocksField>::new(&[]),
+    )
+    .unwrap();
+
+    assert!(
+        Verifier::verify(
+            &proof,
+            &air,
+            &mut DefaultTranscript::<GoldilocksField>::new(&[])
+        ),
+        "Verification failed for a clamped tiny trace under default options (K=7)"
+    );
+}
+
+/// Prove + verify with DEFAULT options (K=7) and a 256-row trace (trace_bits=8).
+/// With blowup=2 (blowup_log=1): expected_k = min(7,8) = 7, total_folds = 8-7 = 1.
+/// This exercises the single-fold path: zero committed FRI layers, one final fold,
+/// and the `fri_layers_merkle_roots.is_empty() && !zetas.is_empty()` branch in
+/// `verify_query_and_sym_openings`.
+#[test_log::test]
+fn test_prove_verify_single_fold() {
+    let mut trace = simple_addition_trace::<GoldilocksField>(256);
+    let proof_options = ProofOptions::default_test_options();
+    let pub_inputs = SimpleAdditionPublicInputs {
+        a: Felt::from(1u64),
+        b: Felt::from(2u64),
+    };
+    let air = SimpleAdditionAIR::<GoldilocksField>::new(&proof_options);
+
+    let proof = Prover::prove(
+        &air,
+        &mut trace,
+        &pub_inputs,
+        &mut DefaultTranscript::<GoldilocksField>::new(&[]),
+    )
+    .expect("Failed to generate proof for single-fold trace");
+
+    assert!(
+        Verifier::verify(
+            &proof,
+            &air,
+            &mut DefaultTranscript::<GoldilocksField>::new(&[])
+        ),
+        "Verification failed for single-fold trace (256 rows, total_folds=1)"
+    );
+}
+
 /// Test that verification fails when using wrong public inputs.
 /// This ensures the boundary constraints are actually enforced.
 #[test_log::test]
@@ -172,3 +270,176 @@ fn test_verify_rejects_opening_column_count_mismatch() {
         "Verifier must reject when an opening's column count does not match the OOD table width"
     );
 }
+
+// ---------------------------------------------------------------------------
+// Helpers shared by the FRI early-termination soundness tests below.
+// ---------------------------------------------------------------------------
+
+/// Build a valid proof over a 1024-row trace (trace_bits=10) using the
+/// default options (k=7, blowup=2).  With these parameters:
+///   expected_k  = min(7, 10) = 7
+///   total_folds = 10 - 7    = 3
+///   fri_final_poly_coeffs.len() = 2^7 = 128
+///   fri_layers_merkle_roots.len() = total_folds - 1 = 2
+fn make_valid_folding_proof() -> (
+    SimpleAdditionAIR<GoldilocksField>,
+    crate::proof::stark::StarkProof<
+        GoldilocksField,
+        GoldilocksField,
+        SimpleAdditionPublicInputs<GoldilocksField>,
+    >,
+) {
+    let mut trace = simple_addition_trace::<GoldilocksField>(1024);
+    let proof_options = ProofOptions::default_test_options();
+    let pub_inputs = SimpleAdditionPublicInputs {
+        a: Felt::from(1u64),
+        b: Felt::from(2u64),
+    };
+    let air = SimpleAdditionAIR::<GoldilocksField>::new(&proof_options);
+    let proof = Prover::prove(
+        &air,
+        &mut trace,
+        &pub_inputs,
+        &mut DefaultTranscript::<GoldilocksField>::new(&[]),
+    )
+    .expect("Prover failed to generate 1024-row folding proof");
+    (air, proof)
+}
+
+// ---------------------------------------------------------------------------
+// FRI early-termination soundness negative tests (Task 9)
+// ---------------------------------------------------------------------------
+
+/// Soundness: mutating one element of `fri_final_poly_coeffs` must cause
+/// verification to fail.  The verifier absorbs every coefficient into the
+/// Fiat-Shamir transcript before sampling query indices, so any modification
+/// shifts all query challenges and invalidates the FRI openings.
+#[test_log::test]
+fn tampered_final_coeff_is_rejected() {
+    let (air, mut proof) = make_valid_folding_proof();
+
+    // Sanity: the unmodified proof must verify first.
+    assert!(
+        Verifier::verify(
+            &proof,
+            &air,
+            &mut DefaultTranscript::<GoldilocksField>::new(&[])
+        ),
+        "precondition: valid folding proof must verify"
+    );
+
+    // Corrupt the first coefficient by adding 1.
+    proof.fri_final_poly_coeffs[0] =
+        proof.fri_final_poly_coeffs[0].clone() + Felt::one();
+
+    assert!(
+        !Verifier::verify(
+            &proof,
+            &air,
+            &mut DefaultTranscript::<GoldilocksField>::new(&[])
+        ),
+        "Verifier must reject a proof with a tampered FRI final-poly coefficient"
+    );
+}
+
+/// Soundness: pushing an extra element so `fri_final_poly_coeffs.len() > 2^k`
+/// must be rejected by the structural degree check and must NOT panic.
+/// The length check `len != 1 << expected_k` fires before the helper that
+/// asserts a power-of-two length, so no assert is reachable.
+#[test_log::test]
+fn over_length_final_poly_is_rejected() {
+    let (air, mut proof) = make_valid_folding_proof();
+
+    // Sanity: the unmodified proof must verify first.
+    assert!(
+        Verifier::verify(
+            &proof,
+            &air,
+            &mut DefaultTranscript::<GoldilocksField>::new(&[])
+        ),
+        "precondition: valid folding proof must verify"
+    );
+
+    // Extend to length 129 (not equal to 128 = 2^7).
+    proof.fri_final_poly_coeffs.push(Felt::zero());
+
+    assert!(
+        !Verifier::verify(
+            &proof,
+            &air,
+            &mut DefaultTranscript::<GoldilocksField>::new(&[])
+        ),
+        "Verifier must reject when fri_final_poly_coeffs is longer than 2^k (over-length)"
+    );
+}
+
+/// Soundness: removing one element so `fri_final_poly_coeffs.len() < 2^k`
+/// must be rejected and must NOT panic.  The verifier's length check
+/// (`len != 1 << expected_k`) fires before `terminal_codeword_from_coeffs`
+/// (which asserts power-of-two length), so no assert is triggered.
+/// If this test panics instead of returning false, that is a real verifier bug.
+#[test_log::test]
+fn truncated_final_poly_is_rejected() {
+    let (air, mut proof) = make_valid_folding_proof();
+
+    // Sanity: the unmodified proof must verify first.
+    assert!(
+        Verifier::verify(
+            &proof,
+            &air,
+            &mut DefaultTranscript::<GoldilocksField>::new(&[])
+        ),
+        "precondition: valid folding proof must verify"
+    );
+
+    // Shorten to length 127 (not equal to 128 = 2^7).
+    proof.fri_final_poly_coeffs.pop();
+
+    assert!(
+        !Verifier::verify(
+            &proof,
+            &air,
+            &mut DefaultTranscript::<GoldilocksField>::new(&[])
+        ),
+        "Verifier must reject when fri_final_poly_coeffs is shorter than 2^k (truncated)"
+    );
+}
+
+/// Soundness: a proof generated under k=7 must NOT verify when the verifier
+/// uses k=6.  The verifier reads `fri_final_poly_log_degree` from the AIR it
+/// is given, so constructing a fresh AIR with k=6 is sufficient to switch the
+/// expected degree.
+///
+/// With a 1024-row trace (trace_bits=10):
+///   Prover   (k=7): expected_k=7, total_folds=3, merkle_roots.len()=2
+///   Verifier (k=6): expected_k=6, total_folds=4, expects merkle_roots.len()=3
+/// The committed-layer count mismatch (2 vs 3) causes `step_3_verify_fri` to
+/// return false immediately, before any transcript-dependent checks.
+#[test_log::test]
+fn cross_k_proof_does_not_verify() {
+    let (air_k7, proof) = make_valid_folding_proof();
+
+    // Sanity: the proof verifies under the matching k=7 AIR.
+    assert!(
+        Verifier::verify(
+            &proof,
+            &air_k7,
+            &mut DefaultTranscript::<GoldilocksField>::new(&[])
+        ),
+        "precondition: valid folding proof must verify with k=7"
+    );
+
+    // Build a verifier AIR that expects k=6.
+    let mut options_k6 = ProofOptions::default_test_options();
+    options_k6.fri_final_poly_log_degree = 6;
+    let air_k6 = SimpleAdditionAIR::<GoldilocksField>::new(&options_k6);
+
+    assert!(
+        !Verifier::verify(
+            &proof,
+            &air_k6,
+            &mut DefaultTranscript::<GoldilocksField>::new(&[])
+        ),
+        "Verifier with k=6 must reject a proof generated with k=7 (cross-k mismatch)"
+    );
+}
diff --git a/crypto/stark/src/tests/terminal_tests.rs b/crypto/stark/src/tests/terminal_tests.rs
new file mode 100644
index 000000000..e48e81b20
--- /dev/null
+++ b/crypto/stark/src/tests/terminal_tests.rs
@@ -0,0 +1,46 @@
+use math::fft::bit_reversing::in_place_bit_reverse_permute;
+use math::field::element::FieldElement;
+use math::field::goldilocks::GoldilocksField;
+use math::polynomial::Polynomial;
+
+use crate::fri::terminal::{coeffs_from_terminal_codeword, terminal_codeword_from_coeffs};
+
+type F = GoldilocksField;
+type FE = FieldElement<F>;
+
+/// Roundtrip test: a degree-<8 polynomial survives
+///   coeffs -> codeword (FRI bit-reversed) -> coeffs_from_terminal_codeword
+///   and
+///   recovered_coeffs -> terminal_codeword_from_coeffs -> original codeword.
+#[test]
+fn test_terminal_roundtrip() {
+    // k=3: poly has 8 coefficients, degree < 8.
+    // blowup=2: terminal codeword length = 8*2 = 16.
+    let final_poly_log_degree: u32 = 3;
+    let coeffs: Vec<FE> = (1u64..=8).map(FE::new).collect();
+    let offset = FE::new(3);
+
+    // Build the reference FRI-order codeword:
+    //   evaluate_offset_fft returns natural order -> bit-reverse -> FRI order.
+    let poly = Polynomial::new(&coeffs);
+    let mut codeword = Polynomial::evaluate_offset_fft::<F>(&poly, 2, Some(8), &offset)
+        .expect("evaluate_offset_fft failed");
+    in_place_bit_reverse_permute(&mut codeword);
+    assert_eq!(codeword.len(), 16);
+
+    // --- prover direction ---
+    let recovered_coeffs =
+        coeffs_from_terminal_codeword::<F, F>(&codeword, &offset, final_poly_log_degree);
+    assert_eq!(
+        recovered_coeffs, coeffs,
+        "coeffs_from_terminal_codeword did not recover the original coefficients"
+    );
+
+    // --- verifier direction ---
+    let rebuilt_codeword =
+        terminal_codeword_from_coeffs::<F, F>(&recovered_coeffs, &offset, 16);
+    assert_eq!(
+        rebuilt_codeword, codeword,
+        "terminal_codeword_from_coeffs did not rebuild the original codeword"
+    );
+}
diff --git a/crypto/stark/src/verifier.rs b/crypto/stark/src/verifier.rs
index 68819c76b..ecd031f62 100644
--- a/crypto/stark/src/verifier.rs
+++ b/crypto/stark/src/verifier.rs
@@ -238,10 +238,31 @@ pub trait IsStarkVerifier<
         composition_poly_claimed_ood_evaluation == composition_poly_ood_evaluation
     }
 
+    /// FRI termination params derived from options + domain: `(blowup_log, expected_k, total_folds)`.
+    ///
+    /// * `blowup_log`  - log2 of the LDE blowup factor.
+    /// * `expected_k`  - clamped final-poly log-degree: `min(k, trace_bits)`.
+    /// * `total_folds` - number of FRI folds performed: `trace_bits - expected_k`.
+    ///
+    /// Both the commit phase (prover) and the Fiat-Shamir replay (verifier) must use
+    /// the same computation; having it in one place prevents silent drift between the two
+    /// callers that would break all proofs.
+    fn fri_termination_params(
+        air: &dyn AIR<Field = Field, FieldExtension = FieldExtension, PublicInputs = PI>,
+        domain: &VerifierDomain<Field>,
+    ) -> (u32, u32, u32) {
+        let k = air.options().fri_final_poly_log_degree as u32;
+        let blowup_log = (domain.lde_length / domain.trace_length).trailing_zeros();
+        let expected_k = k.min(domain.root_order);
+        let total_folds = domain.root_order - expected_k;
+        (blowup_log, expected_k, total_folds)
+    }
+
     /// Reconstructs the Deep composition polynomial evaluations at the challenge indices values using the provided
     /// openings of the trace polynomials and the composition polynomial parts. It then uses these to verify that the
     /// FRI decommitments are valid and correspond to the Deep composition polynomial.
     fn step_3_verify_fri(
+        air: &dyn AIR<Field = Field, FieldExtension = FieldExtension, PublicInputs = PI>,
         proof: &StarkProof<Field, FieldExtension, PI>,
         domain: &VerifierDomain<Field>,
         challenges: &Challenges<FieldExtension>,
@@ -258,6 +279,36 @@ pub trait IsStarkVerifier<
                 None => return false,
             };
 
+        // ---- Reconstruct the FRI terminal codeword from the final-poly coeffs ----
+        // The prover folds the deep composition codeword down to a terminal
+        // codeword of length `terminal_len = 2^(blowup_log + expected_k)` and sends the
+        // `2^expected_k` coefficients of the low-degree polynomial it encodes.
+        // `VerifierDomain.root_order` is `log2(trace_length)` (trace bits), and the
+        // LDE blowup adds `blowup_log` bits.
+        let (blowup_log, expected_k, total_folds) = Self::fri_termination_params(air, domain);
+
+        // Structural check: number of committed FRI layers must equal
+        // `total_folds - 1` (zero when no fold or a single final fold happened).
+        if proof.fri_layers_merkle_roots.len() != total_folds.saturating_sub(1) as usize {
+            return false;
+        }
+        // Structural check: the final polynomial must have exactly `2^expected_k`
+        // coefficients; otherwise the reconstruction below is ill-defined.
+        if proof.fri_final_poly_coeffs.len() != (1usize << expected_k) {
+            return false;
+        }
+
+        let terminal_len = (1usize << blowup_log) << expected_k;
+        let terminal_offset = domain.coset_offset.pow(1u64 << total_folds);
+        let terminal_codeword = crate::fri::terminal::terminal_codeword_from_coeffs::<
+            Field,
+            FieldExtension,
+        >(
+            &proof.fri_final_poly_coeffs,
+            &terminal_offset,
+            terminal_len,
+        );
+
         // verify FRI
         let mut evaluation_point_inverse = challenges
             .iotas
@@ -284,6 +335,7 @@ pub trait IsStarkVerifier<
                     eval,
                     &deep_poly_evaluations[i],
                     &deep_poly_evaluations_sym[i],
+                    &terminal_codeword,
                 )
             })
     }
@@ -474,12 +526,28 @@ pub trait IsStarkVerifier<
         evaluation_point_inv: FieldElement<Field>,
         deep_composition_evaluation: &FieldElement<FieldExtension>,
         deep_composition_evaluation_sym: &FieldElement<FieldExtension>,
+        terminal_codeword: &[FieldElement<FieldExtension>],
     ) -> bool
     where
         FieldElement<Field>: AsBytes + Sync + Send,
         FieldElement<FieldExtension>: AsBytes + Sync + Send,
     {
         let fri_layers_merkle_roots = &proof.fri_layers_merkle_roots;
+
+        let p0_eval = deep_composition_evaluation;
+        let p0_eval_sym = deep_composition_evaluation_sym;
+
+        // No-fold (clamp) case: the codeword never folds (`total_folds == 0`), so
+        // no folding challenges were drawn and the terminal codeword *is* the deep
+        // composition codeword p₀ itself. The query's two points 𝜐 and -𝜐 sit at
+        // FRI-order positions `iota*2` and `iota*2 + 1` of the terminal codeword.
+        if zetas.is_empty() {
+            return terminal_codeword.get(iota * 2).is_some_and(|t| p0_eval == t)
+                && terminal_codeword
+                    .get(iota * 2 + 1)
+                    .is_some_and(|t| p0_eval_sym == t);
+        }
+
         let evaluation_point_vec: Vec<FieldElement<Field>> =
             core::iter::successors(Some(evaluation_point_inv.square()), |evaluation_point| {
                 Some(evaluation_point.square())
@@ -487,19 +555,17 @@ pub trait IsStarkVerifier<
             .take(fri_layers_merkle_roots.len())
             .collect();
 
-        let p0_eval = deep_composition_evaluation;
-        let p0_eval_sym = deep_composition_evaluation_sym;
-
         // Reconstruct p₁(𝜐²)
         let mut v =
             (p0_eval + p0_eval_sym) + evaluation_point_inv * &zetas[0] * (p0_eval - p0_eval_sym);
         let mut index = iota;
 
-        // Handle case with 0 FRI layers (trace_length <= 2)
-        // In this case, the fold loop below doesn't iterate, so we need to verify
-        // the final value directly here.
+        // Handle case with 0 committed FRI layers but a single final fold
+        // (`total_folds == 1`). The fold loop below doesn't iterate, so we compare
+        // the folded value `v` against the reconstructed terminal codeword at the
+        // query's terminal-layer position (`index == iota`) directly.
         if fri_layers_merkle_roots.is_empty() {
-            return v == proof.fri_last_value;
+            return terminal_codeword.get(index).is_some_and(|t| &v == t);
         }
 
         // For each FRI layer, starting from the layer 1: use the proof to verify the validity of values pᵢ(−𝜐^(2ⁱ)) (given by the prover) and
@@ -540,8 +606,12 @@ pub trait IsStarkVerifier<
                     if i < fri_decommitment.layers_evaluations_sym.len() - 1 {
                         result & openings_ok
                     } else {
-                        // Check that final value is the given by the prover
-                        result & (v == proof.fri_last_value) & openings_ok
+                        // Last committed layer: `v` is now the folded value at the
+                        // terminal layer and `index` (after the final `index >>= 1`)
+                        // is its FRI-order position there. Check it against the
+                        // reconstructed terminal codeword.
+                        let terminal_ok = terminal_codeword.get(index).is_some_and(|t| &v == t);
+                        result & terminal_ok & openings_ok
                     }
                 },
             )
@@ -1019,11 +1089,25 @@ pub trait IsStarkVerifier<
             })
             .collect::<Vec<FieldElement<FieldExtension>>>();
 
-        // >>>> Send challenge 𝜁ₙ₋₁
-        zetas.push(transcript.sample_field_element());
+        // The prover only samples the final-fold challenge when the codeword
+        // actually folds past the committed layers. For tiny traces (the clamp
+        // case) no fold happens, so no challenge is drawn. This must mirror the
+        // prover's `commit_phase_from_evaluations` exactly.
+        //
+        // `VerifierDomain.root_order` is `log2(trace_length)` (trace bits). The
+        // number of total folds equals `trace_bits - min(k, trace_bits)`.
+        let (_, _, total_folds) = Self::fri_termination_params(air, domain);
+
+        // >>>> Send final-fold challenge 𝜁_final (only when folding occurs)
+        if total_folds > 0 {
+            zetas.push(transcript.sample_field_element());
+        }
 
-        // <<<< Receive value: pₙ
-        transcript.append_field_element(&proof.fri_last_value);
+        // <<<< Receive the FRI final-polynomial coefficients (same Vec, same
+        // order the prover appended them in `commit_phase_from_evaluations`).
+        for c in &proof.fri_final_poly_coeffs {
+            transcript.append_field_element(c);
+        }
 
         // Receive grinding value
         let security_bits = air.context().proof_options.grinding_factor;
@@ -1118,7 +1202,7 @@ pub trait IsStarkVerifier<
         #[cfg(feature = "instruments")]
         let timer3 = Instant::now();
 
-        if !Self::step_3_verify_fri(proof, &domain, &challenges) {
+        if !Self::step_3_verify_fri(air, proof, &domain, &challenges) {
             #[cfg(not(feature = "test_fiat_shamir"))]
             error!("FRI verification failed");
             return false;
diff --git a/prover/src/lib.rs b/prover/src/lib.rs
index 81233d39f..8b814df18 100644
--- a/prover/src/lib.rs
+++ b/prover/src/lib.rs
@@ -798,6 +798,7 @@ pub fn prove_with_options_and_inputs(
         &table_counts,
         num_private_input_pages,
         &runtime_page_ranges,
+        proof_options.fri_final_poly_log_degree,
     );
 
     // Phase 4: Prove (multi_prove)
@@ -949,6 +950,7 @@ pub fn verify_with_options(
         &vm_proof.table_counts,
         vm_proof.num_private_input_pages,
         &vm_proof.runtime_page_ranges,
+        proof_options.fri_final_poly_log_degree,
     );
 
     // Fork the post-absorb state: the replay helper advances through Phase A
diff --git a/prover/src/statement.rs b/prover/src/statement.rs
index 7935abe66..63140a7b5 100644
--- a/prover/src/statement.rs
+++ b/prover/src/statement.rs
@@ -5,9 +5,9 @@
 //! (`DefaultTranscript`), so a single hash suffices — no external digest
 //! needed beyond the ELF.
 //!
-//! All three call sites (prove, verify, bus-balance replay) must absorb
-//! identical bytes; any divergence makes every derived challenge differ and
-//! verification reject.
+//! Both call sites (prove, verify) must absorb identical bytes; the bus-balance
+//! replay inherits the post-absorb transcript via clone(). Any divergence makes
+//! every derived challenge differ and verification reject.
 
 use crypto::fiat_shamir::is_transcript::IsTranscript;
 use sha3::{Digest, Keccak256};
@@ -16,7 +16,7 @@ use crate::test_utils::E;
 use crate::{RuntimePageRange, TableCounts};
 
 /// Domain-separation tag. Bump the suffix (`_V2`, ...) on any encoding change.
-const DOMAIN_TAG: &[u8] = b"LAMBDAVM_STARK_STATEMENT_V2";
+const DOMAIN_TAG: &[u8] = b"LAMBDAVM_STARK_STATEMENT_V3";
 
 fn elf_digest(elf: &[u8]) -> [u8; 32] {
     let mut h = Keccak256::new();
@@ -31,6 +31,7 @@ pub(crate) fn absorb_statement(
     table_counts: &TableCounts,
     num_private_input_pages: usize,
     runtime_page_ranges: &[RuntimePageRange],
+    fri_final_poly_log_degree: u8,
 ) {
     t.append_bytes(DOMAIN_TAG);
 
@@ -81,6 +82,9 @@ pub(crate) fn absorb_statement(
 
     t.append_bytes(&(num_private_input_pages as u64).to_le_bytes());
 
+    // fri_final_poly_log_degree: single byte, no endianness concern.
+    t.append_bytes(&[fri_final_poly_log_degree]);
+
     // runtime_page_ranges: count-prefixed; each entry fixed width.
     t.append_bytes(&(runtime_page_ranges.len() as u64).to_le_bytes());
     for r in runtime_page_ranges {
diff --git a/prover/src/tests/statement_tests.rs b/prover/src/tests/statement_tests.rs
index 55ac5a15b..ed7d965c1 100644
--- a/prover/src/tests/statement_tests.rs
+++ b/prover/src/tests/statement_tests.rs
@@ -45,22 +45,23 @@ fn state_after_absorb(
     counts: &TableCounts,
     priv_pages: usize,
     ranges: &[RuntimePageRange],
+    fri_final_poly_log_degree: u8,
 ) -> [u8; 32] {
     let mut t = DefaultTranscript::<E>::new(&[]);
-    absorb_statement(&mut t, elf, out, counts, priv_pages, ranges);
+    absorb_statement(&mut t, elf, out, counts, priv_pages, ranges, fri_final_poly_log_degree);
     t.state()
 }
 
 #[test]
 fn state_is_deterministic() {
-    let a = state_after_absorb(b"elf", b"out", &sample_counts(), 3, &sample_ranges());
-    let b = state_after_absorb(b"elf", b"out", &sample_counts(), 3, &sample_ranges());
+    let a = state_after_absorb(b"elf", b"out", &sample_counts(), 3, &sample_ranges(), 7);
+    let b = state_after_absorb(b"elf", b"out", &sample_counts(), 3, &sample_ranges(), 7);
     assert_eq!(a, b);
 }
 
 #[test]
 fn state_depends_on_every_field() {
-    let baseline = state_after_absorb(b"elf", b"out", &sample_counts(), 1, &sample_ranges());
+    let baseline = state_after_absorb(b"elf", b"out", &sample_counts(), 1, &sample_ranges(), 7);
 
     assert_ne!(
         baseline,
@@ -69,7 +70,8 @@ fn state_depends_on_every_field() {
             b"out",
             &sample_counts(),
             1,
-            &sample_ranges()
+            &sample_ranges(),
+            7,
         ),
         "state must depend on elf",
     );
@@ -80,7 +82,8 @@ fn state_depends_on_every_field() {
             b"different-output",
             &sample_counts(),
             1,
-            &sample_ranges()
+            &sample_ranges(),
+            7,
         ),
         "state must depend on public_output",
     );
@@ -89,21 +92,27 @@ fn state_depends_on_every_field() {
     counts2.branch += 1;
     assert_ne!(
         baseline,
-        state_after_absorb(b"elf", b"out", &counts2, 1, &sample_ranges()),
+        state_after_absorb(b"elf", b"out", &counts2, 1, &sample_ranges(), 7),
         "state must depend on table_counts",
     );
 
     assert_ne!(
         baseline,
-        state_after_absorb(b"elf", b"out", &sample_counts(), 2, &sample_ranges()),
+        state_after_absorb(b"elf", b"out", &sample_counts(), 2, &sample_ranges(), 7),
         "state must depend on num_private_input_pages",
     );
 
     assert_ne!(
         baseline,
-        state_after_absorb(b"elf", b"out", &sample_counts(), 1, &[]),
+        state_after_absorb(b"elf", b"out", &sample_counts(), 1, &[], 7),
         "state must depend on runtime_page_ranges",
     );
+
+    assert_ne!(
+        baseline,
+        state_after_absorb(b"elf", b"out", &sample_counts(), 1, &sample_ranges(), 8),
+        "state must depend on fri_final_poly_log_degree",
+    );
 }
 
 #[test]
@@ -116,7 +125,7 @@ fn public_output_length_prefix_prevents_collision() {
     let mut counts_b = sample_counts();
     counts_b.cpu = 0;
     assert_ne!(
-        state_after_absorb(b"elf", b"", &counts_a, 0, &[]),
-        state_after_absorb(b"elf", b"\x41", &counts_b, 0, &[]),
+        state_after_absorb(b"elf", b"", &counts_a, 0, &[], 7),
+        state_after_absorb(b"elf", b"\x41", &counts_b, 0, &[], 7),
     );
 }