diff --git a/plonky2/src/batch_fri/oracle.rs b/plonky2/src/batch_fri/oracle.rs
index 192e374451..58deeaa3c0 100644
--- a/plonky2/src/batch_fri/oracle.rs
+++ b/plonky2/src/batch_fri/oracle.rs
@@ -450,6 +450,8 @@ mod test {
             proof.pow_witness,
             k0,
             &fri_params.config,
+            None,
+            None,
         );
         let degree_bits = [k0, k1, k2];
         let merkle_cap = trace_oracle.batch_merkle_tree.cap;
diff --git a/plonky2/src/batch_fri/prover.rs b/plonky2/src/batch_fri/prover.rs
index 770c2c2285..e71fe25b44 100644
--- a/plonky2/src/batch_fri/prover.rs
+++ b/plonky2/src/batch_fri/prover.rs
@@ -318,6 +318,8 @@ mod tests {
             proof.pow_witness,
             k,
             &fri_params.config,
+            None,
+            None,
         );
 
         let fri_opening_batch = FriOpeningBatch {
@@ -440,6 +442,8 @@ mod tests {
             proof.pow_witness,
             k0,
             &fri_params.config,
+            None,
+            None,
         );
         let fri_opening_batch_0 = FriOpenings {
             batches: vec![FriOpeningBatch {
diff --git a/plonky2/src/fri/challenges.rs b/plonky2/src/fri/challenges.rs
index be73a8c241..b261a55e31 100644
--- a/plonky2/src/fri/challenges.rs
+++ b/plonky2/src/fri/challenges.rs
@@ -1,10 +1,14 @@
+#[cfg(not(feature = "std"))]
+use alloc::vec;
+
 use crate::field::extension::Extendable;
 use crate::field::polynomial::PolynomialCoeffs;
+use crate::field::types::Field;
 use crate::fri::proof::{FriChallenges, FriChallengesTarget};
 use crate::fri::structure::{FriOpenings, FriOpeningsTarget};
 use crate::fri::FriConfig;
 use crate::gadgets::polynomial::PolynomialCoeffsExtTarget;
-use crate::hash::hash_types::{MerkleCapTarget, RichField};
+use crate::hash::hash_types::{MerkleCapTarget, RichField, NUM_HASH_OUT_ELTS};
 use crate::hash::merkle_tree::MerkleCap;
 use crate::iop::challenger::{Challenger, RecursiveChallenger};
 use crate::iop::target::Target;
@@ -28,6 +32,8 @@ impl<F: RichField, H: Hasher<F>> Challenger<F, H> {
         pow_witness: F,
         degree_bits: usize,
         config: &FriConfig,
+        final_poly_coeff_len: Option<usize>,
+        max_num_query_steps: Option<usize>,
     ) -> FriChallenges<F, D>
     where
         F: RichField + Extendable<D>,
@@ -46,7 +52,26 @@ impl<F: RichField, H: Hasher<F>> Challenger<F, H> {
             })
             .collect();
 
+        // When this proof was generated in a circuit with a different number of query steps,
+        // the challenger needs to observe the additional hash caps.
+        if let Some(step_count) = max_num_query_steps {
+            let cap_len = (1 << config.cap_height) * NUM_HASH_OUT_ELTS;
+            let zero_cap = vec![F::ZERO; cap_len];
+            for _ in commit_phase_merkle_caps.len()..step_count {
+                self.observe_elements(&zero_cap);
+                self.get_extension_challenge::<D>();
+            }
+        }
+
         self.observe_extension_elements(&final_poly.coeffs);
+        // When this proof was generated in a circuit with a different final polynomial length,
+        // the challenger needs to observe the full length of the final polynomial.
+        if let Some(len) = final_poly_coeff_len {
+            let current_len = final_poly.coeffs.len();
+            for _ in current_len..len {
+                self.observe_extension_element(&F::Extension::ZERO);
+            }
+        }
 
         self.observe_element(pow_witness);
         let fri_pow_response = self.get_challenge();
diff --git a/plonky2/src/fri/oracle.rs b/plonky2/src/fri/oracle.rs
index 3e1ac781b1..e413071a45 100644
--- a/plonky2/src/fri/oracle.rs
+++ b/plonky2/src/fri/oracle.rs
@@ -178,6 +178,8 @@ impl<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>, const D: usize>
         oracles: &[&Self],
         challenger: &mut Challenger<F, C::Hasher>,
         fri_params: &FriParams,
+        final_poly_coeff_len: Option<usize>,
+        max_num_query_steps: Option<usize>,
         timing: &mut TimingTree,
     ) -> FriProof<F, C::Hasher, D> {
         assert!(D > 1, "Not implemented for D=1.");
@@ -226,6 +228,8 @@ impl<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>, const D: usize>
             lde_final_values,
             challenger,
             fri_params,
+            final_poly_coeff_len,
+            max_num_query_steps,
             timing,
         );
 
diff --git a/plonky2/src/fri/prover.rs b/plonky2/src/fri/prover.rs
index b385fb5369..24c88ced70 100644
--- a/plonky2/src/fri/prover.rs
+++ b/plonky2/src/fri/prover.rs
@@ -1,13 +1,16 @@
 #[cfg(not(feature = "std"))]
+use alloc::vec;
+#[cfg(not(feature = "std"))]
 use alloc::vec::Vec;
 
+use plonky2_field::types::Field;
 use plonky2_maybe_rayon::*;
 
 use crate::field::extension::{flatten, unflatten, Extendable};
 use crate::field::polynomial::{PolynomialCoeffs, PolynomialValues};
 use crate::fri::proof::{FriInitialTreeProof, FriProof, FriQueryRound, FriQueryStep};
 use crate::fri::{FriConfig, FriParams};
-use crate::hash::hash_types::RichField;
+use crate::hash::hash_types::{RichField, NUM_HASH_OUT_ELTS};
 use crate::hash::hashing::PlonkyPermutation;
 use crate::hash::merkle_tree::MerkleTree;
 use crate::iop::challenger::Challenger;
@@ -26,6 +29,8 @@ pub fn fri_proof<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>, const
     lde_polynomial_values: PolynomialValues<F::Extension>,
     challenger: &mut Challenger<F, C::Hasher>,
     fri_params: &FriParams,
+    final_poly_coeff_len: Option<usize>,
+    max_num_query_steps: Option<usize>,
     timing: &mut TimingTree,
 ) -> FriProof<F, C::Hasher, D> {
     let n = lde_polynomial_values.len();
@@ -40,6 +45,8 @@ pub fn fri_proof<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>, const
             lde_polynomial_values,
             challenger,
             fri_params,
+            final_poly_coeff_len,
+            max_num_query_steps,
         )
     );
 
@@ -67,11 +74,20 @@ pub(crate) type FriCommitedTrees<F, C, const D: usize> = (
     PolynomialCoeffs<<F as Extendable<D>>::Extension>,
 );
 
+pub fn final_poly_coeff_len(mut degree_bits: usize, reduction_arity_bits: &Vec<usize>) -> usize {
+    for arity_bits in reduction_arity_bits {
+        degree_bits -= *arity_bits;
+    }
+    1 << degree_bits
+}
+
 fn fri_committed_trees<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>, const D: usize>(
     mut coeffs: PolynomialCoeffs<F::Extension>,
     mut values: PolynomialValues<F::Extension>,
     challenger: &mut Challenger<F, C::Hasher>,
     fri_params: &FriParams,
+    final_poly_coeff_len: Option<usize>,
+    max_num_query_steps: Option<usize>,
 ) -> FriCommitedTrees<F, C, D> {
     let mut trees = Vec::with_capacity(fri_params.reduction_arity_bits.len());
 
@@ -103,12 +119,33 @@ fn fri_committed_trees<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>,
         values = coeffs.coset_fft(shift.into())
     }
 
+    // When verifying this proof in a circuit with a different number of query steps,
+    // we need the challenger to stay in sync with the verifier. Therefore, the challenger
+    // must observe the additional hash caps and generate dummy challenges.
+    if let Some(step_count) = max_num_query_steps {
+        let cap_len = (1 << fri_params.config.cap_height) * NUM_HASH_OUT_ELTS;
+        let zero_cap = vec![F::ZERO; cap_len];
+        for _ in fri_params.reduction_arity_bits.len()..step_count {
+            challenger.observe_elements(&zero_cap);
+            challenger.get_extension_challenge::<D>();
+        }
+    }
+
     // The coefficients being removed here should always be zero.
     coeffs
         .coeffs
         .truncate(coeffs.len() >> fri_params.config.rate_bits);
 
     challenger.observe_extension_elements(&coeffs.coeffs);
+    // When verifying this proof in a circuit with a different final polynomial length,
+    // the challenger needs to observe the full length of the final polynomial.
+    if let Some(len) = final_poly_coeff_len {
+        let current_len = coeffs.coeffs.len();
+        for _ in current_len..len {
+            challenger.observe_extension_element(&F::Extension::ZERO);
+        }
+    }
+
     (trees, coeffs)
 }
 
diff --git a/plonky2/src/fri/recursive_verifier.rs b/plonky2/src/fri/recursive_verifier.rs
index 16e02f6a81..f2880f678f 100644
--- a/plonky2/src/fri/recursive_verifier.rs
+++ b/plonky2/src/fri/recursive_verifier.rs
@@ -1,5 +1,6 @@
 #[cfg(not(feature = "std"))]
 use alloc::{format, vec::Vec};
+use core::ops::RangeInclusive;
 
 use itertools::Itertools;
 
@@ -179,6 +180,97 @@ impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
         }
     }
 
+    /// Verifies the current FRI proof with `current_degree_bits`, which may differ from the
+    /// circuit's `degree_bits` in `params`.
+    /// The circuit uses random access gates to select and connect the current hash/evaluation
+    /// values with those in the proof. It is designed with the maximum number of query/folding
+    /// steps and final polynomial length at `degree_bits`, "skipping" steps when the actual proof
+    /// has fewer.
+    pub fn verify_fri_proof_with_multiple_degree_bits<C: GenericConfig<D, F = F>>(
+        &mut self,
+        instance: &FriInstanceInfoTarget<D>,
+        openings: &FriOpeningsTarget<D>,
+        challenges: &FriChallengesTarget<D>,
+        initial_merkle_caps: &[MerkleCapTarget],
+        proof: &FriProofTarget<D>,
+        params: &FriParams,
+        current_degree_bits: Target,
+        degree_sub_one_bits_vec: &[BoolTarget],
+        min_degree_bits_to_support: usize,
+    ) where
+        C::Hasher: AlgebraicHasher<F>,
+    {
+        if let Some(max_arity_bits) = params.max_arity_bits() {
+            self.check_recursion_config(max_arity_bits);
+        }
+
+        debug_assert_eq!(
+            params.final_poly_len(),
+            proof.final_poly.len(),
+            "Final polynomial has wrong degree."
+        );
+
+        // Size of the LDE domain.
+        let log_n = params.config.rate_bits + params.degree_bits;
+        let mut current_log_n = self.constant(F::from_canonical_usize(params.config.rate_bits));
+        current_log_n = self.add(current_log_n, current_degree_bits);
+        let min_log_n_to_support = params.config.rate_bits + min_degree_bits_to_support;
+
+        with_context!(
+            self,
+            "check PoW",
+            self.fri_verify_proof_of_work(challenges.fri_pow_response, &params.config)
+        );
+
+        // Check that parameters are coherent.
+        debug_assert_eq!(
+            params.config.num_query_rounds,
+            proof.query_round_proofs.len(),
+            "Number of query rounds does not match config."
+        );
+
+        let precomputed_reduced_evals = with_context!(
+            self,
+            "precompute reduced evaluations",
+            PrecomputedReducedOpeningsTarget::from_os_and_alpha(
+                openings,
+                challenges.fri_alpha,
+                self
+            )
+        );
+
+        for (i, round_proof) in proof.query_round_proofs.iter().enumerate() {
+            // To minimize noise in our logs, we will only record a context for a single FRI query.
+            // The very first query will have some extra gates due to constants being registered, so
+            // the second query is a better representative.
+            let level = if i == 1 {
+                log::Level::Debug
+            } else {
+                log::Level::Trace
+            };
+
+            let num_queries = proof.query_round_proofs.len();
+            with_context!(
+                self,
+                level,
+                &format!("verify one (of {num_queries}) query rounds"),
+                self.fri_verifier_query_round_with_multiple_degree_bits::<C>(
+                    instance,
+                    challenges,
+                    &precomputed_reduced_evals,
+                    initial_merkle_caps,
+                    proof,
+                    challenges.fri_query_indices[i],
+                    min_log_n_to_support..=log_n,
+                    current_log_n,
+                    degree_sub_one_bits_vec,
+                    round_proof,
+                    params,
+                )
+            );
+        }
+    }
+
     fn fri_verify_initial_proof<H: AlgebraicHasher<F>>(
         &mut self,
         x_index_bits: &[BoolTarget],
@@ -206,6 +298,39 @@ impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
         }
     }
 
+    fn fri_verify_initial_proof_with_multiple_degree_bits<H: AlgebraicHasher<F>>(
+        &mut self,
+        x_index_bits: &[BoolTarget],
+        log_n_range: RangeInclusive<usize>,
+        n_index: Target,
+        proof: &FriInitialTreeProofTarget,
+        initial_merkle_caps: &[MerkleCapTarget],
+        cap_index: Target,
+    ) {
+        let one = self.one();
+        for (i, ((evals, merkle_proof), cap)) in proof
+            .evals_proofs
+            .iter()
+            .zip(initial_merkle_caps)
+            .enumerate()
+        {
+            with_context!(
+                self,
+                &format!("verify {i}'th initial Merkle proof"),
+                self.verify_merkle_proof_to_cap_with_cap_indices::<H>(
+                    one,
+                    evals.clone(),
+                    x_index_bits,
+                    log_n_range.clone(),
+                    n_index,
+                    cap_index,
+                    cap,
+                    merkle_proof
+                )
+            );
+        }
+    }
+
     fn fri_combine_initial(
         &mut self,
         instance: &FriInstanceInfoTarget<D>,
@@ -364,6 +489,155 @@ impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
         self.connect_extension(eval, old_eval);
     }
 
+    fn fri_verifier_query_round_with_multiple_degree_bits<C: GenericConfig<D, F = F>>(
+        &mut self,
+        instance: &FriInstanceInfoTarget<D>,
+        challenges: &FriChallengesTarget<D>,
+        precomputed_reduced_evals: &PrecomputedReducedOpeningsTarget<D>,
+        initial_merkle_caps: &[MerkleCapTarget],
+        proof: &FriProofTarget<D>,
+        x_index: Target,
+        log_n_range: RangeInclusive<usize>,
+        log_n: Target,
+        degree_sub_one_bits_vec: &[BoolTarget],
+        round_proof: &FriQueryRoundTarget<D>,
+        params: &FriParams,
+    ) where
+        C::Hasher: AlgebraicHasher<F>,
+    {
+        assert!(*log_n_range.start() > params.config.cap_height);
+        let n_index = {
+            let min_log_n = self.constant(F::from_canonical_usize(*log_n_range.start()));
+            self.sub(log_n, min_log_n)
+        };
+
+        // Note that this `low_bits` decomposition permits non-canonical binary encodings. Here we
+        // verify that this has a negligible impact on soundness error.
+        Self::assert_noncanonical_indices_ok(&params.config);
+        let mut x_index_bits = self.low_bits(x_index, *log_n_range.end(), F::BITS);
+
+        let cap_indices: Vec<_> = log_n_range
+            .clone()
+            .map(|n| {
+                let slice_start = n - params.config.cap_height;
+                self.le_sum(x_index_bits[slice_start..n].iter())
+            })
+            .collect();
+        let cap_index = self.random_access(n_index, cap_indices);
+        with_context!(
+            self,
+            "check FRI initial proof",
+            self.fri_verify_initial_proof_with_multiple_degree_bits::<C::Hasher>(
+                &x_index_bits,
+                log_n_range.clone(),
+                n_index,
+                &round_proof.initial_trees_proof,
+                initial_merkle_caps,
+                cap_index,
+            )
+        );
+
+        let g = self.constant(F::coset_shift());
+        // `subgroup_x` is `subgroup[x_index]`, i.e., the actual field element in the domain.
+        let subgroup_x_vec: Vec<_> = log_n_range
+            .clone()
+            .map(|n| {
+                with_context!(self, "compute x from its index", {
+                    let phi = F::primitive_root_of_unity(n);
+                    let phi = self.exp_from_bits_const_base(phi, x_index_bits[..n].iter().rev());
+                    // subgroup_x = g * phi
+                    self.mul(g, phi)
+                })
+            })
+            .collect();
+
+        let mut subgroup_x = self.random_access(n_index, subgroup_x_vec);
+
+        // old_eval is the last derived evaluation; it will be checked for consistency with its
+        // committed "parent" value in the next iteration.
+        let mut old_eval = with_context!(
+            self,
+            "combine initial oracles",
+            self.fri_combine_initial(
+                instance,
+                &round_proof.initial_trees_proof,
+                challenges.fri_alpha,
+                subgroup_x,
+                precomputed_reduced_evals,
+                params,
+            )
+        );
+
+        let mut index_in_degree_sub_one_bits_vec = {
+            let mut degree_bits_len = degree_sub_one_bits_vec.len();
+            for arity_bits in &params.reduction_arity_bits {
+                degree_bits_len -= arity_bits;
+            }
+            degree_bits_len
+        };
+        for (i, &arity_bits) in params.reduction_arity_bits.iter().enumerate() {
+            let evals = &round_proof.steps[i].evals;
+
+            // Split x_index into the index of the coset x is in, and the index of x within that coset.
+            let coset_index_bits = x_index_bits[arity_bits..].to_vec();
+            let x_index_within_coset_bits = &x_index_bits[..arity_bits];
+            let x_index_within_coset = self.le_sum(x_index_within_coset_bits.iter());
+
+            // Check consistency with our old evaluation from the previous round.
+            let new_eval = self.random_access_extension(x_index_within_coset, evals.clone());
+            let step_active = degree_sub_one_bits_vec[index_in_degree_sub_one_bits_vec];
+            self.conditional_assert_eq_ext(step_active.target, new_eval, old_eval);
+
+            // Infer P(y) from {P(x)}_{x^arity=y}.
+            let eval = with_context!(
+                self,
+                "infer evaluation using interpolation",
+                self.compute_evaluation(
+                    subgroup_x,
+                    x_index_within_coset_bits,
+                    arity_bits,
+                    evals,
+                    challenges.fri_betas[i],
+                )
+            );
+            old_eval = self.select_ext(step_active, eval, old_eval);
+
+            with_context!(
+                self,
+                "verify FRI round Merkle proof.",
+                self.verify_merkle_proof_to_cap_with_cap_indices::<C::Hasher>(
+                    step_active.target,
+                    flatten_target(evals),
+                    &coset_index_bits,
+                    log_n_range.clone(),
+                    n_index,
+                    cap_index,
+                    &proof.commit_phase_merkle_caps[i],
+                    &round_proof.steps[i].merkle_proof,
+                )
+            );
+
+            // Update the point x to x^arity.
+            let subgroup_x_cur = self.exp_power_of_2(subgroup_x, arity_bits);
+            subgroup_x = self.select(step_active, subgroup_x_cur, subgroup_x);
+
+            x_index_bits = coset_index_bits;
+            index_in_degree_sub_one_bits_vec += arity_bits;
+        }
+
+        // Final check of FRI. After all the reductions, we check that the final polynomial is equal
+        // to the one sent by the prover.
+        let eval = with_context!(
+            self,
+            &format!(
+                "evaluate final polynomial of length {}",
+                proof.final_poly.len()
+            ),
+            proof.final_poly.eval_scalar(self, subgroup_x)
+        );
+        self.connect_extension(eval, old_eval);
+    }
+
     /// We decompose FRI query indices into bits without verifying that the decomposition given by
     /// the prover is the canonical one. In particular, if `x_index < 2^field_bits - p`, then the
     /// prover could supply the binary encoding of either `x_index` or `x_index + p`, since the are
diff --git a/plonky2/src/fri/witness_util.rs b/plonky2/src/fri/witness_util.rs
index 041d43c134..7f8cee147a 100644
--- a/plonky2/src/fri/witness_util.rs
+++ b/plonky2/src/fri/witness_util.rs
@@ -1,9 +1,10 @@
-use anyhow::Result;
+use anyhow::{anyhow, Result};
 use itertools::Itertools;
+use plonky2_field::types::Field;
 
 use crate::field::extension::Extendable;
 use crate::fri::proof::{FriProof, FriProofTarget};
-use crate::hash::hash_types::RichField;
+use crate::hash::hash_types::{HashOut, RichField};
 use crate::iop::witness::WitnessWrite;
 use crate::plonk::config::AlgebraicHasher;
 
@@ -20,21 +21,47 @@ where
 {
     witness.set_target(fri_proof_target.pow_witness, fri_proof.pow_witness)?;
 
-    for (&t, &x) in fri_proof_target
-        .final_poly
-        .0
-        .iter()
-        .zip_eq(&fri_proof.final_poly.coeffs)
-    {
-        witness.set_extension_target(t, x)?;
+    let target_len = fri_proof_target.final_poly.0.len();
+    let coeffs_len = fri_proof.final_poly.coeffs.len();
+
+    if target_len < coeffs_len {
+        return Err(anyhow!(
+            "fri_proof->final_poly's target length is less than the proof length"
+        ));
     }
 
-    for (t, x) in fri_proof_target
-        .commit_phase_merkle_caps
-        .iter()
-        .zip_eq(&fri_proof.commit_phase_merkle_caps)
-    {
-        witness.set_cap_target(t, x)?;
+    // Set overlapping elements
+    for i in 0..coeffs_len {
+        witness.set_extension_target(
+            fri_proof_target.final_poly.0[i],
+            fri_proof.final_poly.coeffs[i],
+        )?;
+    }
+
+    // Set remaining elements in target to ZERO if target is longer
+    for i in coeffs_len..target_len {
+        witness.set_extension_target(fri_proof_target.final_poly.0[i], F::Extension::ZERO)?;
+    }
+
+    let target_caps = &fri_proof_target.commit_phase_merkle_caps;
+    let proof_caps = &fri_proof.commit_phase_merkle_caps;
+
+    if target_caps.len() < proof_caps.len() {
+        return Err(anyhow!(
+            "fri_proof->commit_phase_merkle_caps's target length is less than the proof length"
+        ));
+    }
+
+    // Set matching elements in both proof and target caps
+    for (target_cap, proof_cap) in target_caps.iter().zip(proof_caps) {
+        witness.set_cap_target(target_cap, proof_cap)?;
+    }
+
+    // Set remaining elements in target caps to ZERO if target is longer
+    for target_cap in target_caps.iter().skip(proof_caps.len()) {
+        for hash in target_cap.0.iter() {
+            witness.set_hash_target(*hash, HashOut::ZERO)?;
+        }
     }
 
     for (qt, q) in fri_proof_target
@@ -51,22 +78,55 @@ where
             for (&t, &x) in at.0.iter().zip_eq(&a.0) {
                 witness.set_target(t, x)?;
             }
-            for (&t, &x) in at.1.siblings.iter().zip_eq(&a.1.siblings) {
-                witness.set_hash_target(t, x)?;
+            let target_len = at.1.siblings.len();
+            let siblings_len = a.1.siblings.len();
+
+            if target_len < siblings_len {
+                return Err(anyhow!("fri_proof->query_round_proofs->initial_trees_proof->evals_proofs->siblings' target length is less than the proof length"));
+            }
+
+            // Set overlapping elements
+            for i in 0..siblings_len {
+                witness.set_hash_target(at.1.siblings[i], a.1.siblings[i])?;
+            }
+
+            // Set remaining elements in target to ZERO if target is longer
+            for i in siblings_len..target_len {
+                witness.set_hash_target(at.1.siblings[i], HashOut::ZERO)?;
             }
         }
 
-        for (st, s) in qt.steps.iter().zip_eq(&q.steps) {
+        for (st, s) in qt.steps.iter().zip(&q.steps) {
             for (&t, &x) in st.evals.iter().zip_eq(&s.evals) {
                 witness.set_extension_target(t, x)?;
             }
-            for (&t, &x) in st
-                .merkle_proof
-                .siblings
-                .iter()
-                .zip_eq(&s.merkle_proof.siblings)
-            {
-                witness.set_hash_target(t, x)?;
+
+            let target_len = st.merkle_proof.siblings.len();
+            let siblings_len = s.merkle_proof.siblings.len();
+
+            if target_len < siblings_len {
+                return Err(anyhow!("fri_proof->query_round_proofs->steps->merkle_proof->siblings' target length is less than the proof length"));
+            }
+
+            // Set overlapping elements
+            for i in 0..siblings_len {
+                witness.set_hash_target(st.merkle_proof.siblings[i], s.merkle_proof.siblings[i])?;
+            }
+
+            // Set remaining elements in target to ZERO if target is longer
+            for i in siblings_len..target_len {
+                witness.set_hash_target(st.merkle_proof.siblings[i], HashOut::ZERO)?;
+            }
+        }
+
+        // Set remaining steps in qt to ZERO if qt.steps is longer
+        for st in qt.steps.iter().skip(q.steps.len()) {
+            for &eval in &st.evals {
+                witness.set_extension_target(eval, F::Extension::ZERO)?;
+            }
+
+            for &sibling in &st.merkle_proof.siblings {
+                witness.set_hash_target(sibling, HashOut::ZERO)?;
             }
         }
     }
diff --git a/plonky2/src/gadgets/arithmetic_extension.rs b/plonky2/src/gadgets/arithmetic_extension.rs
index 6026a8cb16..355d5e253a 100644
--- a/plonky2/src/gadgets/arithmetic_extension.rs
+++ b/plonky2/src/gadgets/arithmetic_extension.rs
@@ -15,7 +15,7 @@ use crate::gates::multiplication_extension::MulExtensionGate;
 use crate::hash::hash_types::RichField;
 use crate::iop::ext_target::{ExtensionAlgebraTarget, ExtensionTarget};
 use crate::iop::generator::{GeneratedValues, SimpleGenerator};
-use crate::iop::target::Target;
+use crate::iop::target::{BoolTarget, Target};
 use crate::iop::witness::{PartitionWitness, Witness, WitnessWrite};
 use crate::plonk::circuit_builder::CircuitBuilder;
 use crate::plonk::circuit_data::CommonCircuitData;
@@ -421,6 +421,21 @@ impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
         self.scalar_mul_add_ext_algebra(a, b, zero)
     }
 
+    /// Exponentiates `base` to the power of exponent expressed as `exponent_bits`.
+    pub fn exp_extension_from_bits(
+        &mut self,
+        mut base: ExtensionTarget<D>,
+        exponent_bits: &[BoolTarget],
+    ) -> ExtensionTarget<D> {
+        let mut res = self.one_extension();
+        for i in 0..exponent_bits.len() {
+            let new_res = self.mul_extension(res, base);
+            res = self.select_ext(exponent_bits[i], new_res, res);
+            base = self.mul_extension(base, base);
+        }
+        res
+    }
+
     /// Exponentiate `base` to the power of `2^power_log`.
     // TODO: Test
     pub fn exp_power_of_2_extension(
diff --git a/plonky2/src/gadgets/random_access.rs b/plonky2/src/gadgets/random_access.rs
index 0d99a3e918..543248bf4f 100644
--- a/plonky2/src/gadgets/random_access.rs
+++ b/plonky2/src/gadgets/random_access.rs
@@ -1,6 +1,8 @@
 #[cfg(not(feature = "std"))]
 use alloc::vec::Vec;
 
+use itertools::repeat_n;
+
 use crate::field::extension::Extendable;
 use crate::gates::random_access::RandomAccessGate;
 use crate::hash::hash_types::{HashOutTarget, MerkleCapTarget, RichField};
@@ -13,6 +15,15 @@ use crate::util::log2_strict;
 impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
     /// Checks that a `Target` matches a vector at a particular index.
     pub fn random_access(&mut self, access_index: Target, v: Vec<Target>) -> Target {
+        let mut v = v;
+        let current_len = v.len();
+        let next_power_of_two = current_len.next_power_of_two();
+        if current_len < next_power_of_two {
+            // Get the last element (if there is one) and extend with it
+            if let Some(&last) = v.last() {
+                v.extend(repeat_n(last, next_power_of_two - current_len));
+            }
+        }
         let vec_size = v.len();
         let bits = log2_strict(vec_size);
         debug_assert!(vec_size > 0);
@@ -45,6 +56,15 @@ impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
         access_index: Target,
         v: Vec<ExtensionTarget<D>>,
     ) -> ExtensionTarget<D> {
+        let mut v = v;
+        let current_len = v.len();
+        let next_power_of_two = current_len.next_power_of_two();
+        if current_len < next_power_of_two {
+            // Get the last element (if there is one) and extend with it
+            if let Some(&last) = v.last() {
+                v.extend(repeat_n(last, next_power_of_two - current_len));
+            }
+        }
         let selected: Vec<_> = (0..D)
             .map(|i| self.random_access(access_index, v.iter().map(|et| et.0[i]).collect()))
             .collect();
diff --git a/plonky2/src/hash/merkle_proofs.rs b/plonky2/src/hash/merkle_proofs.rs
index 021240a98e..424e03ae64 100644
--- a/plonky2/src/hash/merkle_proofs.rs
+++ b/plonky2/src/hash/merkle_proofs.rs
@@ -1,5 +1,6 @@
 #[cfg(not(feature = "std"))]
 use alloc::{vec, vec::Vec};
+use core::ops::RangeInclusive;
 
 use anyhow::{ensure, Result};
 use itertools::Itertools;
@@ -180,6 +181,63 @@ impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
         }
     }
 
+    /// Same as `verify_merkle_proof_to_cap`, except with the final "cap index" as separate parameter,
+    /// rather than being contained in `leaf_index_bits`.
+    pub(crate) fn verify_merkle_proof_to_cap_with_cap_indices<H: AlgebraicHasher<F>>(
+        &mut self,
+        condition: Target,
+        leaf_data: Vec<Target>,
+        leaf_index_bits: &[BoolTarget],
+        log_n_range: RangeInclusive<usize>,
+        n_index: Target,
+        cap_index: Target,
+        merkle_cap: &MerkleCapTarget,
+        proof: &MerkleProofTarget,
+    ) {
+        debug_assert!(H::AlgebraicPermutation::RATE >= NUM_HASH_OUT_ELTS);
+
+        let zero = self.zero();
+        let mut state: HashOutTarget = self.hash_or_noop::<H>(leaf_data);
+        debug_assert_eq!(state.elements.len(), NUM_HASH_OUT_ELTS);
+
+        let num_log_n = log_n_range.clone().count();
+        let mut final_states = vec![state; num_log_n];
+
+        for (&bit, &sibling) in leaf_index_bits.iter().zip(&proof.siblings) {
+            debug_assert_eq!(sibling.elements.len(), NUM_HASH_OUT_ELTS);
+
+            let mut perm_inputs = H::AlgebraicPermutation::default();
+            perm_inputs.set_from_slice(&state.elements, 0);
+            perm_inputs.set_from_slice(&sibling.elements, NUM_HASH_OUT_ELTS);
+            // Ensure the rest of the state, if any, is zero:
+            perm_inputs.set_from_iter(core::iter::repeat(zero), 2 * NUM_HASH_OUT_ELTS);
+            let perm_outs = self.permute_swapped::<H>(perm_inputs, bit);
+            let hash_outs = perm_outs.squeeze()[0..NUM_HASH_OUT_ELTS]
+                .try_into()
+                .unwrap();
+            state = HashOutTarget {
+                elements: hash_outs,
+            };
+            // Store state at specific indices
+            for n in 0..num_log_n - 1 {
+                final_states[n] = final_states[n + 1];
+            }
+            final_states[num_log_n - 1] = state;
+        }
+
+        for i in 0..NUM_HASH_OUT_ELTS {
+            let result = self.random_access(
+                cap_index,
+                merkle_cap.0.iter().map(|h| h.elements[i]).collect(),
+            );
+            let state = self.random_access(
+                n_index,
+                final_states.iter().map(|s| s.elements[i]).collect(),
+            );
+            self.conditional_assert_eq(condition, result, state);
+        }
+    }
+
     /// Same as `verify_batch_merkle_proof_to_cap`, except with the final "cap index" as separate parameter,
     /// rather than being contained in `leaf_index_bits`.
     pub(crate) fn verify_batch_merkle_proof_to_cap_with_cap_index<H: AlgebraicHasher<F>>(
diff --git a/plonky2/src/plonk/circuit_builder.rs b/plonky2/src/plonk/circuit_builder.rs
index d0d96f39ba..16f2a61c32 100644
--- a/plonky2/src/plonk/circuit_builder.rs
+++ b/plonky2/src/plonk/circuit_builder.rs
@@ -548,6 +548,18 @@ impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
         self.connect(constr, zero);
     }
 
+    /// If `condition`, enforces that two `ExtensionTarget<D>` values are equal.
+    pub fn conditional_assert_eq_ext(
+        &mut self,
+        condition: Target,
+        x: ExtensionTarget<D>,
+        y: ExtensionTarget<D>,
+    ) {
+        for i in 0..D {
+            self.conditional_assert_eq(condition, x.0[i], y.0[i]);
+        }
+    }
+
     /// Enforces that a routable `Target` value is 0, using Plonk's permutation argument.
     pub fn assert_zero(&mut self, x: Target) {
         let zero = self.zero();
diff --git a/plonky2/src/plonk/get_challenges.rs b/plonky2/src/plonk/get_challenges.rs
index 45d79f99aa..5872cf6953 100644
--- a/plonky2/src/plonk/get_challenges.rs
+++ b/plonky2/src/plonk/get_challenges.rs
@@ -85,6 +85,8 @@ fn get_challenges<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>, cons
             pow_witness,
             common_data.degree_bits(),
             &config.fri_config,
+            None,
+            None,
         ),
     })
 }
diff --git a/plonky2/src/plonk/prover.rs b/plonky2/src/plonk/prover.rs
index fcd784f326..2b450b01e0 100644
--- a/plonky2/src/plonk/prover.rs
+++ b/plonky2/src/plonk/prover.rs
@@ -340,6 +340,8 @@ where
             ],
             &mut challenger,
             &common_data.fri_params,
+            None,
+            None,
             timing,
         )
     );
diff --git a/starky/src/fibonacci_stark.rs b/starky/src/fibonacci_stark.rs
index 69dfc46d37..4dc1752f33 100644
--- a/starky/src/fibonacci_stark.rs
+++ b/starky/src/fibonacci_stark.rs
@@ -134,7 +134,11 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for FibonacciStar
 
 #[cfg(test)]
 mod tests {
+    #[cfg(not(feature = "std"))]
+    use alloc::vec::Vec;
+
     use anyhow::Result;
+    use itertools::Itertools;
     use plonky2::field::extension::Extendable;
     use plonky2::field::types::Field;
     use plonky2::hash::hash_types::RichField;
@@ -156,17 +160,17 @@ mod tests {
     use crate::stark_testing::{test_stark_circuit_constraints, test_stark_low_degree};
     use crate::verifier::verify_stark_proof;
 
+    const D: usize = 2;
+    type C = PoseidonGoldilocksConfig;
+    type F = <C as GenericConfig<D>>::F;
+    type S = FibonacciStark<F, D>;
+
     fn fibonacci<F: Field>(n: usize, x0: F, x1: F) -> F {
         (0..n).fold((x0, x1), |x, _| (x.1, x.0 + x.1)).1
     }
 
     #[test]
     fn test_fibonacci_stark() -> Result<()> {
-        const D: usize = 2;
-        type C = PoseidonGoldilocksConfig;
-        type F = <C as GenericConfig<D>>::F;
-        type S = FibonacciStark<F, D>;
-
         let config = StarkConfig::standard_fast_config();
         let num_rows = 1 << 5;
         let public_inputs = [F::ZERO, F::ONE, fibonacci(num_rows - 1, F::ZERO, F::ONE)];
@@ -178,19 +182,15 @@ mod tests {
             &config,
             trace,
             &public_inputs,
+            None,
             &mut TimingTree::default(),
         )?;
 
-        verify_stark_proof(stark, proof, &config)
+        verify_stark_proof(stark, proof, &config, None)
     }
 
     #[test]
     fn test_fibonacci_stark_degree() -> Result<()> {
-        const D: usize = 2;
-        type C = PoseidonGoldilocksConfig;
-        type F = <C as GenericConfig<D>>::F;
-        type S = FibonacciStark<F, D>;
-
         let num_rows = 1 << 5;
         let stark = S::new(num_rows);
         test_stark_low_degree(stark)
@@ -198,11 +198,6 @@ mod tests {
 
     #[test]
     fn test_fibonacci_stark_circuit() -> Result<()> {
-        const D: usize = 2;
-        type C = PoseidonGoldilocksConfig;
-        type F = <C as GenericConfig<D>>::F;
-        type S = FibonacciStark<F, D>;
-
         let num_rows = 1 << 5;
         let stark = S::new(num_rows);
         test_stark_circuit_constraints::<F, C, S, D>(stark)
@@ -211,13 +206,10 @@ mod tests {
     #[test]
     fn test_recursive_stark_verifier() -> Result<()> {
         init_logger();
-        const D: usize = 2;
-        type C = PoseidonGoldilocksConfig;
-        type F = <C as GenericConfig<D>>::F;
-        type S = FibonacciStark<F, D>;
 
         let config = StarkConfig::standard_fast_config();
-        let num_rows = 1 << 5;
+        let degree_bits = 5;
+        let num_rows = 1 << degree_bits;
         let public_inputs = [F::ZERO, F::ONE, fibonacci(num_rows - 1, F::ZERO, F::ONE)];
 
         // Test first STARK
@@ -228,9 +220,11 @@ mod tests {
             &config,
             trace,
             &public_inputs,
+            None,
             &mut TimingTree::default(),
         )?;
-        verify_stark_proof(stark, proof.clone(), &config)?;
+        verify_stark_proof(stark, proof.clone(), &config, None)?;
+        assert_eq!(degree_bits, proof.proof.recover_degree_bits(&config));
 
         recursive_proof::<F, C, S, C, D>(stark, proof, &config, true)
     }
@@ -256,9 +250,9 @@ mod tests {
         let degree_bits = inner_proof.proof.recover_degree_bits(inner_config);
         let pt =
             add_virtual_stark_proof_with_pis(&mut builder, &stark, inner_config, degree_bits, 0, 0);
-        set_stark_proof_with_pis_target(&mut pw, &pt, &inner_proof, builder.zero())?;
+        set_stark_proof_with_pis_target(&mut pw, &pt, &inner_proof, degree_bits, builder.zero())?;
 
-        verify_stark_proof_circuit::<F, InnerC, S, D>(&mut builder, stark, pt, inner_config);
+        verify_stark_proof_circuit::<F, InnerC, S, D>(&mut builder, stark, pt, inner_config, None);
 
         if print_gate_counts {
             builder.print_gate_counts(0);
@@ -272,4 +266,87 @@ mod tests {
     fn init_logger() {
         let _ = env_logger::builder().format_timestamp(None).try_init();
     }
+
+    #[test]
+    fn test_recursive_verifier_with_multiple_degree_bits() -> Result<()> {
+        init_logger();
+
+        let mut stark_config = StarkConfig::standard_fast_config();
+        stark_config.fri_config.num_query_rounds = 1;
+
+        let min_degree_bits_to_support = 4;
+        // Currently, we only support verifier_degree_bits to be {30, 26, 22, 18, …}, as they
+        // generate the max final polynomial length when using the default configuration
+        // ConstantArityBits(4, 5). This ensures that for other degrees, the final proof polynomial
+        // will not be longer than the circuit’s final polynomial length.
+        let verifier_degree_bits = 30;
+        let degree_bits = 4..=15;
+        let verifier_fri_params = stark_config.fri_params(verifier_degree_bits);
+
+        // Generate STARK proofs for each degree in `degree_bits`
+        let proofs: Vec<_> = degree_bits
+            .clone()
+            .map(|degree_bits| {
+                let num_rows = 1 << degree_bits;
+                let public_inputs = [F::ZERO, F::ONE, fibonacci(num_rows - 1, F::ZERO, F::ONE)];
+                let stark = S::new(num_rows);
+                let trace = stark.generate_trace(public_inputs[0], public_inputs[1]);
+
+                // Generate proof with the specified verifier degree
+                prove::<F, C, S, D>(
+                    stark,
+                    &stark_config,
+                    trace,
+                    &public_inputs,
+                    Some(verifier_fri_params.clone()),
+                    &mut TimingTree::default(),
+                )
+                .unwrap()
+            })
+            .collect();
+
+        // Configure the circuit for recursive verification
+        let num_rows = 1 << verifier_degree_bits;
+        let stark = S::new(num_rows);
+        for p in proofs.clone() {
+            verify_stark_proof(stark, p, &stark_config, Some(verifier_fri_params.clone()))?;
+        }
+
+        let recursive_verification_circuit_config = CircuitConfig::standard_recursion_config();
+        let mut builder = CircuitBuilder::<F, D>::new(recursive_verification_circuit_config);
+        let zero = builder.zero();
+
+        // Set up proof verification within the circuit
+        let pt = add_virtual_stark_proof_with_pis(
+            &mut builder,
+            &stark,
+            &stark_config,
+            verifier_degree_bits,
+            0,
+            0,
+        );
+        verify_stark_proof_circuit::<F, C, S, D>(
+            &mut builder,
+            stark,
+            pt.clone(),
+            &stark_config,
+            Some(min_degree_bits_to_support),
+        );
+        builder.print_gate_counts(0);
+
+        // Build the recursive circuit
+        let data = builder.build::<C>();
+
+        // Verify each proof using partial witnesses
+        degree_bits
+            .zip_eq(proofs)
+            .try_for_each(|(degree_bits, proof)| {
+                let mut pw = PartialWitness::new();
+                set_stark_proof_with_pis_target(&mut pw, &pt, &proof, degree_bits, zero)?;
+                let proof = data.prove(pw)?;
+                data.verify(proof)
+            })?;
+
+        Ok(())
+    }
 }
diff --git a/starky/src/get_challenges.rs b/starky/src/get_challenges.rs
index 6e8f4bc70e..33e7128caa 100644
--- a/starky/src/get_challenges.rs
+++ b/starky/src/get_challenges.rs
@@ -1,6 +1,8 @@
 use plonky2::field::extension::Extendable;
 use plonky2::field::polynomial::PolynomialCoeffs;
 use plonky2::fri::proof::{FriProof, FriProofTarget};
+use plonky2::fri::prover::final_poly_coeff_len;
+use plonky2::fri::FriParams;
 use plonky2::gadgets::polynomial::PolynomialCoeffsExtTarget;
 use plonky2::hash::hash_types::{MerkleCapTarget, RichField};
 use plonky2::hash::merkle_tree::MerkleCap;
@@ -35,6 +37,7 @@ fn get_challenges<F, C, const D: usize>(
     pow_witness: F,
     config: &StarkConfig,
     degree_bits: usize,
+    verifier_circuit_fri_params: Option<FriParams>,
 ) -> StarkProofChallenges<F, D>
 where
     F: RichField + Extendable<D>,
@@ -67,6 +70,19 @@ where
 
     challenger.observe_openings(&openings.to_fri_openings());
 
+    let (final_poly_coeff_len, max_num_query_steps) =
+        if let Some(verifier_circuit_fri_params) = verifier_circuit_fri_params {
+            (
+                Some(final_poly_coeff_len(
+                    verifier_circuit_fri_params.degree_bits,
+                    &verifier_circuit_fri_params.reduction_arity_bits,
+                )),
+                Some(verifier_circuit_fri_params.reduction_arity_bits.len()),
+            )
+        } else {
+            (None, None)
+        };
+
     StarkProofChallenges {
         lookup_challenge_set,
         stark_alphas,
@@ -77,6 +93,8 @@ where
             pow_witness,
             degree_bits,
             &config.fri_config,
+            final_poly_coeff_len,
+            max_num_query_steps,
         ),
     }
 }
@@ -99,6 +117,7 @@ where
         challenges: Option<&GrandProductChallengeSet<F>>,
         ignore_trace_cap: bool,
         config: &StarkConfig,
+        verifier_circuit_fri_params: Option<FriParams>,
     ) -> StarkProofChallenges<F, D> {
         let degree_bits = self.recover_degree_bits(config);
 
@@ -134,6 +153,7 @@ where
             *pow_witness,
             config,
             degree_bits,
+            verifier_circuit_fri_params,
         )
     }
 }
@@ -156,10 +176,16 @@ where
         challenges: Option<&GrandProductChallengeSet<F>>,
         ignore_trace_cap: bool,
         config: &StarkConfig,
+        verifier_circuit_fri_params: Option<FriParams>,
     ) -> StarkProofChallenges<F, D> {
         challenger.observe_elements(&self.public_inputs);
-        self.proof
-            .get_challenges(challenger, challenges, ignore_trace_cap, config)
+        self.proof.get_challenges(
+            challenger,
+            challenges,
+            ignore_trace_cap,
+            config,
+            verifier_circuit_fri_params,
+        )
     }
 }
 
@@ -258,6 +284,7 @@ impl<const D: usize> StarkProofTarget<D> {
                     pow_witness,
                     ..
                 },
+            ..
         } = self;
 
         let trace_cap = if ignore_trace_cap {
diff --git a/starky/src/lib.rs b/starky/src/lib.rs
index 607a9879a4..a0edcfe798 100644
--- a/starky/src/lib.rs
+++ b/starky/src/lib.rs
@@ -192,10 +192,11 @@
 //!         &CONFIG,
 //!         trace,
 //!         &public_inputs,
+//!         None,
 //!         &mut TimingTree::default(),
 //!     ).expect("We should have a valid proof!");
 //!
-//!     verify_stark_proof(stark, proof, &CONFIG)
+//!     verify_stark_proof(stark, proof, &CONFIG, None)
 //!         .expect("We should be able to verify this proof!")
 //! }
 //! ```
diff --git a/starky/src/permutation_stark.rs b/starky/src/permutation_stark.rs
index ec7f2e41ef..e656554104 100644
--- a/starky/src/permutation_stark.rs
+++ b/starky/src/permutation_stark.rs
@@ -141,10 +141,11 @@ mod tests {
             &config,
             trace,
             &[public_input],
+            None,
             &mut TimingTree::default(),
         )?;
 
-        verify_stark_proof(stark, proof, &config)
+        verify_stark_proof(stark, proof, &config, None)
     }
 
     #[test]
@@ -190,9 +191,10 @@ mod tests {
             &config,
             trace,
             &[public_input],
+            None,
             &mut TimingTree::default(),
         )?;
-        verify_stark_proof(stark, proof.clone(), &config)?;
+        verify_stark_proof(stark, proof.clone(), &config, None)?;
 
         recursive_proof::<F, C, S, C, D>(stark, proof, &config, true)
     }
@@ -218,9 +220,9 @@ mod tests {
         let degree_bits = inner_proof.proof.recover_degree_bits(inner_config);
         let pt =
             add_virtual_stark_proof_with_pis(&mut builder, &stark, inner_config, degree_bits, 0, 0);
-        set_stark_proof_with_pis_target(&mut pw, &pt, &inner_proof, builder.zero())?;
+        set_stark_proof_with_pis_target(&mut pw, &pt, &inner_proof, degree_bits, builder.zero())?;
 
-        verify_stark_proof_circuit::<F, InnerC, S, D>(&mut builder, stark, pt, inner_config);
+        verify_stark_proof_circuit::<F, InnerC, S, D>(&mut builder, stark, pt, inner_config, None);
 
         if print_gate_counts {
             builder.print_gate_counts(0);
diff --git a/starky/src/proof.rs b/starky/src/proof.rs
index cad1f1e787..2d71d8708c 100644
--- a/starky/src/proof.rs
+++ b/starky/src/proof.rs
@@ -66,11 +66,14 @@ pub struct StarkProofTarget<const D: usize> {
     pub openings: StarkOpeningSetTarget<D>,
     /// `Target`s for the batch FRI argument for all openings.
     pub opening_proof: FriProofTarget<D>,
+    /// `Target`s for the proof's degree bits.
+    pub degree_bits: Target,
 }
 
 impl<const D: usize> StarkProofTarget<D> {
     /// Serializes a STARK proof.
     pub fn to_buffer(&self, buffer: &mut Vec<u8>) -> IoResult<()> {
+        buffer.write_target(self.degree_bits)?;
         buffer.write_target_merkle_cap(&self.trace_cap)?;
         buffer.write_bool(self.auxiliary_polys_cap.is_some())?;
         if let Some(poly) = &self.auxiliary_polys_cap {
@@ -87,6 +90,7 @@ impl<const D: usize> StarkProofTarget<D> {
 
     /// Deserializes a STARK proof.
     pub fn from_buffer(buffer: &mut Buffer) -> IoResult<Self> {
+        let degree_bits = buffer.read_target()?;
         let trace_cap = buffer.read_target_merkle_cap()?;
         let auxiliary_polys_cap = if buffer.read_bool()? {
             Some(buffer.read_target_merkle_cap()?)
@@ -107,6 +111,7 @@ impl<const D: usize> StarkProofTarget<D> {
             quotient_polys_cap,
             openings,
             opening_proof,
+            degree_bits,
         })
     }
 
diff --git a/starky/src/prover.rs b/starky/src/prover.rs
index 36d544b624..c6c88b3710 100644
--- a/starky/src/prover.rs
+++ b/starky/src/prover.rs
@@ -13,6 +13,9 @@ use plonky2::field::polynomial::{PolynomialCoeffs, PolynomialValues};
 use plonky2::field::types::Field;
 use plonky2::field::zero_poly_coset::ZeroPolyOnCoset;
 use plonky2::fri::oracle::PolynomialBatch;
+use plonky2::fri::prover::final_poly_coeff_len;
+use plonky2::fri::reduction_strategies::FriReductionStrategy;
+use plonky2::fri::FriParams;
 use plonky2::hash::hash_types::RichField;
 use plonky2::iop::challenger::Challenger;
 use plonky2::plonk::config::GenericConfig;
@@ -39,6 +42,7 @@ pub fn prove<F, C, S, const D: usize>(
     config: &StarkConfig,
     trace_poly_values: Vec<PolynomialValues<F>>,
     public_inputs: &[F],
+    verifier_circuit_fri_params: Option<FriParams>,
     timing: &mut TimingTree,
 ) -> Result<StarkProofWithPublicInputs<F, C, D>>
 where
@@ -55,6 +59,26 @@ where
         fri_params.total_arities() <= degree_bits + rate_bits - cap_height,
         "FRI total reduction arity is too large.",
     );
+    let (final_poly_coeff_len, max_num_query_steps) =
+        if let Some(verifier_circuit_fri_params) = verifier_circuit_fri_params {
+            assert_eq!(verifier_circuit_fri_params.config, fri_params.config);
+            match &config.fri_config.reduction_strategy {
+                FriReductionStrategy::ConstantArityBits(_, final_poly_bits) => {
+                    let len = final_poly_coeff_len(
+                        verifier_circuit_fri_params.degree_bits,
+                        &verifier_circuit_fri_params.reduction_arity_bits,
+                    );
+                    assert_eq!(len, 1 << (1 + *final_poly_bits));
+                    (
+                        Some(len),
+                        Some(verifier_circuit_fri_params.reduction_arity_bits.len()),
+                    )
+                }
+                _ => panic!("Fri Reduction Strategy is not ConstantArityBits"),
+            }
+        } else {
+            (None, None)
+        };
 
     let trace_commitment = timed!(
         timing,
@@ -73,7 +97,6 @@ where
     let mut challenger = Challenger::new();
     challenger.observe_elements(public_inputs);
     challenger.observe_cap(&trace_cap);
-
     prove_with_commitment(
         &stark,
         config,
@@ -83,6 +106,8 @@ where
         None,
         &mut challenger,
         public_inputs,
+        final_poly_coeff_len,
+        max_num_query_steps,
         timing,
     )
 }
@@ -103,6 +128,8 @@ pub fn prove_with_commitment<F, C, S, const D: usize>(
     ctl_challenges: Option<&GrandProductChallengeSet<F>>,
     challenger: &mut Challenger<F, C::Hasher>,
     public_inputs: &[F],
+    final_poly_coeff_len: Option<usize>,
+    max_num_query_steps: Option<usize>,
     timing: &mut TimingTree,
 ) -> Result<StarkProofWithPublicInputs<F, C, D>>
 where
@@ -319,6 +346,8 @@ where
             &initial_merkle_trees,
             challenger,
             &fri_params,
+            final_poly_coeff_len,
+            max_num_query_steps,
             timing,
         )
     );
diff --git a/starky/src/recursive_verifier.rs b/starky/src/recursive_verifier.rs
index 2c485d0d0d..92895eb935 100644
--- a/starky/src/recursive_verifier.rs
+++ b/starky/src/recursive_verifier.rs
@@ -8,7 +8,6 @@ use core::iter::once;
 use anyhow::{ensure, Result};
 use itertools::Itertools;
 use plonky2::field::extension::Extendable;
-use plonky2::field::types::Field;
 use plonky2::fri::witness_util::set_fri_proof_target;
 use plonky2::hash::hash_types::RichField;
 use plonky2::iop::challenger::RecursiveChallenger;
@@ -44,10 +43,12 @@ pub fn verify_stark_proof_circuit<
     stark: S,
     proof_with_pis: StarkProofWithPublicInputsTarget<D>,
     inner_config: &StarkConfig,
+    min_degree_bits_to_support: Option<usize>,
 ) where
     C::Hasher: AlgebraicHasher<F>,
 {
     assert_eq!(proof_with_pis.public_inputs.len(), S::PUBLIC_INPUTS);
+    let max_degree_bits_to_support = proof_with_pis.proof.recover_degree_bits(inner_config);
 
     let mut challenger = RecursiveChallenger::<F, C::Hasher, D>::new(builder);
     let challenges = with_context!(
@@ -64,6 +65,8 @@ pub fn verify_stark_proof_circuit<
         challenges,
         None,
         inner_config,
+        max_degree_bits_to_support,
+        min_degree_bits_to_support,
     );
 }
 
@@ -81,6 +84,8 @@ pub fn verify_stark_proof_with_challenges_circuit<
     challenges: StarkProofChallengesTarget<D>,
     ctl_vars: Option<&[CtlCheckVarsTarget<F, D>]>,
     inner_config: &StarkConfig,
+    degree_bits: usize,
+    min_degree_bits_to_support: Option<usize>,
 ) where
     C::Hasher: AlgebraicHasher<F>,
 {
@@ -88,6 +93,7 @@ pub fn verify_stark_proof_with_challenges_circuit<
 
     let zero = builder.zero();
     let one = builder.one_extension();
+    let two = builder.two();
 
     let num_ctl_polys = ctl_vars
         .map(|v| v.iter().map(|ctl| ctl.helper_columns.len()).sum::<usize>())
@@ -111,13 +117,29 @@ pub fn verify_stark_proof_with_challenges_circuit<
             .collect::<Vec<_>>(),
     );
 
-    let degree_bits = proof.recover_degree_bits(inner_config);
-    let zeta_pow_deg = builder.exp_power_of_2_extension(challenges.stark_zeta, degree_bits);
+    // degree_bits should be nonzero.
+    let _ = builder.inverse(proof.degree_bits);
+
+    let max_num_of_bits_in_degree = degree_bits + 1;
+    let degree = builder.exp(two, proof.degree_bits, max_num_of_bits_in_degree);
+    let degree_bits_vec = builder.split_le(degree, max_num_of_bits_in_degree);
+
+    let zeta_pow_deg = builder.exp_extension_from_bits(challenges.stark_zeta, &degree_bits_vec);
     let z_h_zeta = builder.sub_extension(zeta_pow_deg, one);
+    let degree_ext = builder.convert_to_ext(degree);
+
+    // Calculate primitive_root_of_unity(degree_bits)
+    let two_adicity = builder.constant(F::from_canonical_usize(F::TWO_ADICITY));
+    let two_adicity_sub_degree_bits = builder.sub(two_adicity, proof.degree_bits);
+    let two_exp_two_adicity_sub_degree_bits =
+        builder.exp(two, two_adicity_sub_degree_bits, F::TWO_ADICITY);
+    let base = builder.constant(F::POWER_OF_TWO_GENERATOR);
+    let g = builder.exp(base, two_exp_two_adicity_sub_degree_bits, F::TWO_ADICITY);
+    let g_ext = builder.convert_to_ext(g);
+
     let (l_0, l_last) =
-        eval_l_0_and_l_last_circuit(builder, degree_bits, challenges.stark_zeta, z_h_zeta);
-    let last =
-        builder.constant_extension(F::Extension::primitive_root_of_unity(degree_bits).inverse());
+        eval_l_0_and_l_last_circuit(builder, degree_ext, g_ext, challenges.stark_zeta, z_h_zeta);
+    let last = builder.inverse_extension(g_ext);
     let z_last = builder.sub_extension(challenges.stark_zeta, last);
 
     let mut consumer = RecursiveConstraintConsumer::<F, D>::new(
@@ -181,29 +203,48 @@ pub fn verify_stark_proof_with_challenges_circuit<
     let fri_instance = stark.fri_instance_target(
         builder,
         challenges.stark_zeta,
-        F::primitive_root_of_unity(degree_bits),
+        g,
         num_ctl_polys,
         ctl_zs_first.as_ref().map_or(0, |c| c.len()),
         inner_config,
     );
-    builder.verify_fri_proof::<C>(
-        &fri_instance,
-        &proof.openings.to_fri_openings(zero),
-        &challenges.fri_challenges,
-        &merkle_caps,
-        &proof.opening_proof,
-        &inner_config.fri_params(degree_bits),
-    );
+
+    let one = builder.one();
+    let degree_sub_one = builder.sub(degree, one);
+    // Used to check if we want to skip a Fri query step.
+    let degree_sub_one_bits_vec = builder.split_le(degree_sub_one, degree_bits);
+
+    if let Some(min_degree_bits_to_support) = min_degree_bits_to_support {
+        builder.verify_fri_proof_with_multiple_degree_bits::<C>(
+            &fri_instance,
+            &proof.openings.to_fri_openings(zero),
+            &challenges.fri_challenges,
+            &merkle_caps,
+            &proof.opening_proof,
+            &inner_config.fri_params(degree_bits),
+            proof.degree_bits,
+            &degree_sub_one_bits_vec,
+            min_degree_bits_to_support,
+        );
+    } else {
+        builder.verify_fri_proof::<C>(
+            &fri_instance,
+            &proof.openings.to_fri_openings(zero),
+            &challenges.fri_challenges,
+            &merkle_caps,
+            &proof.opening_proof,
+            &inner_config.fri_params(degree_bits),
+        );
+    }
 }
 
 fn eval_l_0_and_l_last_circuit<F: RichField + Extendable<D>, const D: usize>(
     builder: &mut CircuitBuilder<F, D>,
-    log_n: usize,
+    n: ExtensionTarget<D>,
+    g: ExtensionTarget<D>,
     x: ExtensionTarget<D>,
     z_x: ExtensionTarget<D>,
 ) -> (ExtensionTarget<D>, ExtensionTarget<D>) {
-    let n = builder.constant_extension(F::Extension::from_canonical_usize(1 << log_n));
-    let g = builder.constant_extension(F::Extension::primitive_root_of_unity(log_n));
     let one = builder.one_extension();
     let l_0_deno = builder.mul_sub_extension(n, x, n);
     let l_last_deno = builder.mul_sub_extension(g, x, one);
@@ -284,6 +325,7 @@ pub fn add_virtual_stark_proof<F: RichField + Extendable<D>, S: Stark<F, D>, con
             config,
         ),
         opening_proof: builder.add_virtual_fri_proof(&num_leaves_per_oracle, &fri_params),
+        degree_bits: builder.add_virtual_target(),
     }
 }
 
@@ -324,6 +366,7 @@ pub fn set_stark_proof_with_pis_target<F, C: GenericConfig<D, F = F>, W, const D
     witness: &mut W,
     stark_proof_with_pis_target: &StarkProofWithPublicInputsTarget<D>,
     stark_proof_with_pis: &StarkProofWithPublicInputs<F, C, D>,
+    pis_degree_bits: usize,
     zero: Target,
 ) -> Result<()>
 where
@@ -345,7 +388,7 @@ where
         witness.set_target(pi_t, pi)?;
     }
 
-    set_stark_proof_target(witness, pt, proof, zero)
+    set_stark_proof_target(witness, pt, proof, pis_degree_bits, zero)
 }
 
 /// Set the targets in a [`StarkProofTarget`] to their corresponding values in a
@@ -354,6 +397,7 @@ pub fn set_stark_proof_target<F, C: GenericConfig<D, F = F>, W, const D: usize>(
     witness: &mut W,
     proof_target: &StarkProofTarget<D>,
     proof: &StarkProof<F, C, D>,
+    pis_degree_bits: usize,
     zero: Target,
 ) -> Result<()>
 where
@@ -361,6 +405,10 @@ where
     C::Hasher: AlgebraicHasher<F>,
     W: WitnessWrite<F>,
 {
+    witness.set_target(
+        proof_target.degree_bits,
+        F::from_canonical_usize(pis_degree_bits),
+    )?;
     witness.set_cap_target(&proof_target.trace_cap, &proof.trace_cap)?;
     if let (Some(quotient_polys_cap_target), Some(quotient_polys_cap)) =
         (&proof_target.quotient_polys_cap, &proof.quotient_polys_cap)
diff --git a/starky/src/stark.rs b/starky/src/stark.rs
index c47f969245..8d429ba011 100644
--- a/starky/src/stark.rs
+++ b/starky/src/stark.rs
@@ -13,6 +13,7 @@ use plonky2::fri::structure::{
 };
 use plonky2::hash::hash_types::RichField;
 use plonky2::iop::ext_target::ExtensionTarget;
+use plonky2::iop::target::Target;
 use plonky2::plonk::circuit_builder::CircuitBuilder;
 
 use crate::config::StarkConfig;
@@ -175,7 +176,7 @@ pub trait Stark<F: RichField + Extendable<D>, const D: usize>: Sync {
         &self,
         builder: &mut CircuitBuilder<F, D>,
         zeta: ExtensionTarget<D>,
-        g: F,
+        g: Target,
         num_ctl_helper_polys: usize,
         num_ctl_zs: usize,
         config: &StarkConfig,
@@ -222,7 +223,8 @@ pub trait Stark<F: RichField + Extendable<D>, const D: usize>: Sync {
             ]
             .concat(),
         };
-        let zeta_next = builder.mul_const_extension(g, zeta);
+        let g_ext = builder.convert_to_ext(g);
+        let zeta_next = builder.mul_extension(g_ext, zeta);
         let zeta_next_batch = FriBatchInfoTarget {
             point: zeta_next,
             polynomials: [trace_info, auxiliary_polys_info].concat(),
diff --git a/starky/src/unconstrained_stark.rs b/starky/src/unconstrained_stark.rs
index 495123acf8..ec6045c4bc 100644
--- a/starky/src/unconstrained_stark.rs
+++ b/starky/src/unconstrained_stark.rs
@@ -114,9 +114,10 @@ mod tests {
 
         let stark = S::new(num_rows);
         let trace = stark.generate_trace();
-        let proof = prove::<F, C, S, D>(stark, &config, trace, &[], &mut TimingTree::default())?;
+        let proof =
+            prove::<F, C, S, D>(stark, &config, trace, &[], None, &mut TimingTree::default())?;
 
-        verify_stark_proof(stark, proof, &config)
+        verify_stark_proof(stark, proof, &config, None)
     }
 
     #[test]
@@ -156,8 +157,9 @@ mod tests {
 
         let stark = S::new(num_rows);
         let trace = stark.generate_trace();
-        let proof = prove::<F, C, S, D>(stark, &config, trace, &[], &mut TimingTree::default())?;
-        verify_stark_proof(stark, proof.clone(), &config)?;
+        let proof =
+            prove::<F, C, S, D>(stark, &config, trace, &[], None, &mut TimingTree::default())?;
+        verify_stark_proof(stark, proof.clone(), &config, None)?;
 
         recursive_proof::<F, C, S, C, D>(stark, proof, &config, true)
     }
@@ -183,9 +185,9 @@ mod tests {
         let degree_bits = inner_proof.proof.recover_degree_bits(inner_config);
         let pt =
             add_virtual_stark_proof_with_pis(&mut builder, &stark, inner_config, degree_bits, 0, 0);
-        set_stark_proof_with_pis_target(&mut pw, &pt, &inner_proof, builder.zero())?;
+        set_stark_proof_with_pis_target(&mut pw, &pt, &inner_proof, degree_bits, builder.zero())?;
 
-        verify_stark_proof_circuit::<F, InnerC, S, D>(&mut builder, stark, pt, inner_config);
+        verify_stark_proof_circuit::<F, InnerC, S, D>(&mut builder, stark, pt, inner_config, None);
 
         if print_gate_counts {
             builder.print_gate_counts(0);
diff --git a/starky/src/verifier.rs b/starky/src/verifier.rs
index d56072ad3a..7bf43a4e0e 100644
--- a/starky/src/verifier.rs
+++ b/starky/src/verifier.rs
@@ -10,6 +10,7 @@ use itertools::Itertools;
 use plonky2::field::extension::{Extendable, FieldExtension};
 use plonky2::field::types::Field;
 use plonky2::fri::verifier::verify_fri_proof;
+use plonky2::fri::FriParams;
 use plonky2::hash::hash_types::RichField;
 use plonky2::hash::merkle_tree::MerkleCap;
 use plonky2::iop::challenger::Challenger;
@@ -35,11 +36,18 @@ pub fn verify_stark_proof<
     stark: S,
     proof_with_pis: StarkProofWithPublicInputs<F, C, D>,
     config: &StarkConfig,
+    verifier_circuit_fri_params: Option<FriParams>,
 ) -> Result<()> {
     ensure!(proof_with_pis.public_inputs.len() == S::PUBLIC_INPUTS);
     let mut challenger = Challenger::<F, C::Hasher>::new();
 
-    let challenges = proof_with_pis.get_challenges(&mut challenger, None, false, config);
+    let challenges = proof_with_pis.get_challenges(
+        &mut challenger,
+        None,
+        false,
+        config,
+        verifier_circuit_fri_params,
+    );
 
     verify_stark_proof_with_challenges(
         &stark,