diff --git a/crates/backend-tests/src/lib.rs b/crates/backend-tests/src/lib.rs
index 9c9a580b..db6089cb 100644
--- a/crates/backend-tests/src/lib.rs
+++ b/crates/backend-tests/src/lib.rs
@@ -62,7 +62,7 @@ use openvm_stark_backend::{
         whir::{binary_k_fold, verify_whir, VerifyWhirError},
     },
     AirRef, FiatShamirTranscript, StarkEngine, StarkProtocolConfig, SystemParams,
-    TranscriptHistory, WhirConfig, WhirParams, WhirRoundConfig,
+    TranscriptHistory, WhirConfig, WhirParams, WhirProximityStrategy, WhirRoundConfig,
 };
 use openvm_stark_sdk::{
     config::{
@@ -153,6 +153,10 @@ pub fn proof_shape_verifier_rng_system_params<E: StarkEngine<SC = SC>>() -> eyre
             mu_pow_bits: 1,
             query_phase_pow_bits: 1,
             folding_pow_bits: 1,
+            proximity: WhirProximityStrategy::SplitUniqueList {
+                m: 3,
+                list_start_round: 1,
+            },
         };
         let params = SystemParams {
             l_skip,
@@ -260,6 +264,9 @@ pub fn fib_air_roundtrip<E: StarkEngine<SC = SC>>(
         k: k_whir,
         log_final_poly_len: k_whir,
         query_phase_pow_bits: 1,
+        folding_pow_bits: 11,
+        mu_pow_bits: 10,
+        proximity: WhirProximityStrategy::UniqueDecoding,
     };
     let log_blowup = 1;
     let whir = WhirConfig::new(log_blowup, l_skip + n_stack, whir_params, 80);
@@ -1196,6 +1203,8 @@ pub fn whir_test_config(k_whir: usize) -> WhirConfig {
         mu_pow_bits: 1,
         query_phase_pow_bits: 1,
         folding_pow_bits: 1,
+        proximity: WhirProximityStrategy::UniqueDecoding, /* not relevant since `rounds` is
+                                                           * manually set above */
     }
 }
 
diff --git a/crates/cuda-backend/examples/keccakf.rs b/crates/cuda-backend/examples/keccakf.rs
index 5a776b63..598f7325 100644
--- a/crates/cuda-backend/examples/keccakf.rs
+++ b/crates/cuda-backend/examples/keccakf.rs
@@ -9,12 +9,12 @@ use openvm_stark_backend::{
     p3_air::{Air, AirBuilder, BaseAir},
     p3_field::Field,
     prover::{AirProvingContext, ColMajorMatrix, DeviceDataTransporter, ProvingContext},
-    BaseAirWithPublicValues, PartitionedBaseAir, StarkEngine, SystemParams, WhirConfig, WhirParams,
+    BaseAirWithPublicValues, PartitionedBaseAir, StarkEngine, SystemParams,
 };
 use openvm_stark_sdk::{
     config::{
+        app_params_with_100_bits_security,
         baby_bear_poseidon2::{BabyBearPoseidon2CpuEngine, DuplexSponge},
-        log_up_params::log_up_security_params_baby_bear_100_bits,
     },
     utils::setup_tracing,
 };
@@ -43,26 +43,7 @@ impl<AB: AirBuilder> Air<AB> for TestAir {
 }
 
 fn make_params() -> SystemParams {
-    let l_skip = 4;
-    let n_stack = 17;
-    let w_stack = 64;
-    let k_whir = 4;
-    let whir_params = WhirParams {
-        k: k_whir,
-        log_final_poly_len: 2 * k_whir,
-        query_phase_pow_bits: 20,
-    };
-    let log_blowup = 1;
-    let whir = WhirConfig::new(log_blowup, l_skip + n_stack, whir_params, 100);
-    SystemParams {
-        l_skip,
-        n_stack,
-        w_stack,
-        log_blowup,
-        whir,
-        logup: log_up_security_params_baby_bear_100_bits(),
-        max_constraint_degree: 3,
-    }
+    app_params_with_100_bits_security(21)
 }
 
 fn main() {
diff --git a/crates/cuda-backend/src/whir.rs b/crates/cuda-backend/src/whir.rs
index 882791dd..d0872ecb 100644
--- a/crates/cuda-backend/src/whir.rs
+++ b/crates/cuda-backend/src/whir.rs
@@ -530,6 +530,7 @@ mod tests {
         test_utils::{FibFixture, TestFixture},
         verifier::whir::{verify_whir, VerifyWhirError},
         StarkEngine, StarkProtocolConfig, SystemParams, WhirConfig, WhirParams,
+        WhirProximityStrategy,
     };
     use openvm_stark_sdk::{
         config::{
@@ -642,6 +643,9 @@ mod tests {
             k: k_whir,
             log_final_poly_len,
             query_phase_pow_bits: 2,
+            folding_pow_bits: 1,
+            mu_pow_bits: 3,
+            proximity: WhirProximityStrategy::UniqueDecoding,
         }
     }
 
diff --git a/crates/stark-backend/Cargo.toml b/crates/stark-backend/Cargo.toml
index bced5170..b85d2ca0 100644
--- a/crates/stark-backend/Cargo.toml
+++ b/crates/stark-backend/Cargo.toml
@@ -59,3 +59,4 @@ jemalloc-prof = ["jemalloc", "tikv-jemallocator?/profiling"]
 metrics = ["dep:metrics"]
 test-utils = []
 lean = [] # feature for Lean constraint codegen
+soundness-bchks25-optimized = [] # use brute force optimized parameters for [BCHKS25] proximity gaps security
diff --git a/crates/stark-backend/src/config.rs b/crates/stark-backend/src/config.rs
index ddf10e56..bf187202 100644
--- a/crates/stark-backend/src/config.rs
+++ b/crates/stark-backend/src/config.rs
@@ -92,6 +92,58 @@ impl SystemParams {
     pub fn num_whir_sumcheck_rounds(&self) -> usize {
         self.whir.num_sumcheck_rounds()
     }
+
+    /// Constructor with many configuration options. Only `k_whir`, `max_constraint_degree`,
+    /// `query_phase_pow_bits` are preset with constants.
+    ///
+    /// The `security_bits` is the target bits of security. It is used to select the number of WHIR
+    /// queries, but does **not** guarantee the target security level is achieved by the overall
+    /// protocol using these parameters. Use the soundness calculator to ensure the target security
+    /// level is met.
+    ///
+    /// This function should only be used for internal cryptography libraries. Most users should
+    /// instead use preset parameters provided in SDKs.
+    #[allow(clippy::too_many_arguments)]
+    pub fn new(
+        log_blowup: usize,
+        l_skip: usize,
+        n_stack: usize,
+        w_stack: usize,
+        log_final_poly_len: usize,
+        folding_pow_bits: usize,
+        mu_pow_bits: usize,
+        proximity: WhirProximityStrategy,
+        security_bits: usize,
+        logup: LogUpSecurityParameters,
+    ) -> SystemParams {
+        const WHIR_QUERY_PHASE_POW_BITS: usize = 20;
+
+        let k_whir = 4;
+        let max_constraint_degree = 4;
+        let log_stacked_height = l_skip + n_stack;
+
+        SystemParams {
+            l_skip,
+            n_stack,
+            w_stack,
+            log_blowup,
+            whir: WhirConfig::new(
+                log_blowup,
+                log_stacked_height,
+                WhirParams {
+                    k: k_whir,
+                    log_final_poly_len,
+                    query_phase_pow_bits: WHIR_QUERY_PHASE_POW_BITS,
+                    proximity,
+                    folding_pow_bits,
+                    mu_pow_bits,
+                },
+                security_bits,
+            ),
+            logup,
+            max_constraint_degree,
+        }
+    }
 }
 
 /// Configurable parameters that are used to determine the [WhirConfig] for a target security level.
@@ -102,6 +154,13 @@ pub struct WhirParams {
     /// log_final_poly_len`.
     pub log_final_poly_len: usize,
     pub query_phase_pow_bits: usize,
+    /// Proximity regime to use within each WHIR round. This is used to determine the number of
+    /// queries in each round for a target security level.
+    pub proximity: WhirProximityStrategy,
+    /// Number of bits of grinding to increase security of each folding step.
+    pub folding_pow_bits: usize,
+    /// Number of bits of grinding before sampling the μ batching challenge.
+    pub mu_pow_bits: usize,
 }
 
 #[derive(Clone, Debug, Serialize, Deserialize, PartialEq, Eq)]
@@ -118,6 +177,12 @@ pub struct WhirConfig {
     /// The folding PoW bits can vary per round, but for simplicity (and efficiency of the
     /// recursion circuit) we use the same number for all rounds.
     pub folding_pow_bits: usize,
+    /// Proximity regimes for WHIR rounds. We use only proven error bounds.
+    ///
+    /// Note: this field is not needed by the verifier as it is only used to determine the number
+    /// of queries in the `rounds` field. However we store it in `WhirConfig` for security analysis
+    /// purposes.
+    pub proximity: WhirProximityStrategy,
 }
 
 #[derive(Clone, Copy, Debug, Serialize, Deserialize, PartialEq, Eq)]
@@ -126,40 +191,87 @@ pub struct WhirRoundConfig {
     pub num_queries: usize,
 }
 
+#[derive(Clone, Copy, Debug, Serialize, Deserialize, PartialEq, Eq)]
+pub enum WhirProximityStrategy {
+    /// Unique decoding regime in every WHIR round.
+    UniqueDecoding,
+    /// Unique decoding regime in the initial `list_start_round` WHIR rounds. Then list decoding
+    /// regime with the same proximity radius derived from `m` (see `ListDecoding`) for all
+    /// subsequent WHIR rounds (0-indices `>= list_start_round`). Note that a WHIR round
+    /// consists of codewords of different degrees with the same rate. The WHIR round changes
+    /// when the rate changes.
+    SplitUniqueList { m: usize, list_start_round: usize },
+    /// List decoding regime in every WHIR round, with the same proximity radius derived from `m`,
+    /// where `m = ceil(sqrt(\rho) / 2 \eta), \eta = 1 - sqrt(\rho) - \delta, where \delta is the
+    /// proximity radius.
+    ListDecoding { m: usize },
+}
+
+impl WhirProximityStrategy {
+    pub fn initial_round(&self) -> ProximityRegime {
+        self.in_round(0)
+    }
+
+    pub fn in_round(&self, whir_round: usize) -> ProximityRegime {
+        match *self {
+            Self::UniqueDecoding => ProximityRegime::UniqueDecoding,
+            Self::SplitUniqueList {
+                m,
+                list_start_round,
+            } => {
+                if whir_round < list_start_round {
+                    ProximityRegime::UniqueDecoding
+                } else {
+                    ProximityRegime::ListDecoding { m }
+                }
+            }
+            Self::ListDecoding { m } => ProximityRegime::ListDecoding { m },
+        }
+    }
+}
+
 /// Defines the proximity regime for the proof system.
 #[derive(Clone, Copy, Debug, Serialize, Deserialize, PartialEq, Eq)]
 pub enum ProximityRegime {
     /// Unique decoding guarantees a single valid witness.
     UniqueDecoding,
+    /// List decoding bounded by multiplicity `m`.
+    ListDecoding { m: usize },
 }
 
 impl ProximityRegime {
-    /// Returns the per-query security bits for WHIR query sampling.
+    /// Returns total security bits for `num_queries` WHIR queries.
+    ///
+    /// This treats the per-query error as an upper bound on the maximum agreement.
     ///
-    /// Unique decoding formula:
-    /// Error per query = (1 + ρ) / 2 where ρ is the rate.
-    /// Security bits = -log₂((1 + ρ) / 2)
-    pub fn whir_per_query_security_bits(self, log_inv_rate: usize) -> f64 {
-        match self {
-            ProximityRegime::UniqueDecoding => {
-                let rate = 1.0 / (1 << log_inv_rate) as f64;
-                -((0.5 * (1.0 + rate)).log2())
+    /// - `UniqueDecoding`: max agreement is `(1 + ρ) / 2`.
+    /// - `ListDecoding { m }`: finite-multiplicity Guruswami-Sudan threshold, `sqrt(ρ(1 + 1/m)) +
+    ///   ε` for a tiny `ε`, to keep the proximity threshold strict.
+    pub fn whir_query_security_bits(&self, num_queries: usize, log_inv_rate: usize) -> f64 {
+        let rho = 2.0_f64.powf(-(log_inv_rate as f64));
+        let max_agreement = match *self {
+            ProximityRegime::UniqueDecoding => (1.0 + rho) / 2.0,
+            ProximityRegime::ListDecoding { m } => {
+                let m = m.max(1) as f64;
+                // Johnson bound with a tiny epsilon to ensure strict proximity.
+                (rho * (1.0 + 1.0 / m)).sqrt() + 1e-6
             }
-        }
+        };
+
+        // Keep the `log2` well-defined.
+        let max_agreement = max_agreement.clamp(f64::MIN_POSITIVE, 1.0);
+        -(num_queries as f64) * max_agreement.log2()
     }
 
-    /// Returns total security bits for `num_queries` WHIR queries.
-    ///
-    /// Unique decoding formula:
-    /// Security bits = -n × log₂((1 + ρ) / 2)
-    pub fn whir_query_security_bits(self, num_queries: usize, log_inv_rate: usize) -> f64 {
-        (num_queries as f64) * self.whir_per_query_security_bits(log_inv_rate)
+    /// Returns the per-query security bits for WHIR query sampling.
+    pub fn whir_per_query_security_bits(&self, log_inv_rate: usize) -> f64 {
+        self.whir_query_security_bits(1, log_inv_rate)
     }
 }
 
 impl WhirConfig {
-    /// Sets parameters targeting 100-bits of provable security, with grinding, using the unique
-    /// decoding regime.
+    /// Sets parameters targeting `security_bits` of provable security (including grinding), using
+    /// the given proximity regime.
     pub fn new(
         log_blowup: usize,
         log_stacked_height: usize,
@@ -173,18 +285,15 @@ impl WhirConfig {
             .saturating_sub(whir_params.log_final_poly_len)
             .div_ceil(k_whir);
         let mut log_inv_rate = log_blowup;
-
-        // A safe setting for BabyBear and ~200 columns
-        // TODO[jpw]: use rbr_soundness_queries_combination
-        const FOLDING_POW_BITS: usize = 10;
+        let proximity = whir_params.proximity;
 
         let mut round_parameters = Vec::with_capacity(num_rounds);
-        for _round in 0..num_rounds {
+        for round in 0..num_rounds {
             // Queries are set w.r.t. to old rate, while the rest to the new rate
             let next_rate = log_inv_rate + (k_whir - 1);
 
             let num_queries = Self::queries(
-                ProximityRegime::UniqueDecoding,
+                proximity.in_round(round),
                 protocol_security_level,
                 log_inv_rate,
             );
@@ -193,14 +302,13 @@ impl WhirConfig {
             log_inv_rate = next_rate;
         }
 
-        const MU_POW_BITS: usize = 13;
-
         Self {
             k: k_whir,
             rounds: round_parameters,
-            mu_pow_bits: MU_POW_BITS,
+            mu_pow_bits: whir_params.mu_pow_bits,
             query_phase_pow_bits,
-            folding_pow_bits: FOLDING_POW_BITS,
+            folding_pow_bits: whir_params.folding_pow_bits,
+            proximity,
         }
     }
 
@@ -233,3 +341,17 @@ impl WhirConfig {
         num_queries_f.ceil() as usize
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_whir_list_decoding_query_bits_monotone_in_num_queries() {
+        let regime = ProximityRegime::ListDecoding { m: 2 };
+        let sec_10 = regime.whir_query_security_bits(10, 1);
+        let sec_20 = regime.whir_query_security_bits(20, 1);
+        assert!(sec_20 > sec_10);
+        assert!(sec_10 > 0.0);
+    }
+}
diff --git a/crates/stark-backend/src/soundness.rs b/crates/stark-backend/src/soundness.rs
index dcb2a4a5..eec6cbb9 100644
--- a/crates/stark-backend/src/soundness.rs
+++ b/crates/stark-backend/src/soundness.rs
@@ -9,7 +9,12 @@
 //! Each component contributes to the overall soundness error, and the total security
 //! is the minimum across all components.
 
-use crate::config::{ProximityRegime, SystemParams, WhirConfig};
+use std::f64;
+
+use crate::{
+    config::{ProximityRegime, SystemParams, WhirConfig},
+    WhirProximityStrategy,
+};
 
 #[derive(Clone, Debug)]
 pub struct SoundnessCalculator {
@@ -36,18 +41,28 @@ pub struct SoundnessCalculator {
 /// WHIR soundness breakdown by error source.
 #[derive(Clone, Debug)]
 pub struct WhirSoundnessCalculator {
-    /// Security bits from query sampling.
-    pub query_bits: f64,
+    /// Security bits from μ batching (initial polynomial batching).
+    pub mu_batching_bits: f64,
+    /// Minimum round-by-round security bits across folding rounds, i.e. `ε_fold`.
+    pub fold_rbr_bits: f64,
     /// Security bits from proximity gaps (folding soundness).
     pub proximity_gaps_bits: f64,
     /// Security bits from sumcheck within WHIR rounds.
     pub sumcheck_bits: f64,
     /// Security bits from out-of-domain sampling.
-    pub ood_bits: f64,
+    pub ood_rbr_bits: f64,
+    /// Minimum round-by-round security bits across shift/final rounds, i.e. `ε_shift` / `ε_fin`.
+    pub shift_rbr_bits: f64,
+    /// Security bits from query sampling.
+    pub query_bits: f64,
     /// Security bits from γ batching (combining query and OOD claims).
     pub gamma_batching_bits: f64,
-    /// Security bits from μ batching (initial polynomial batching).
-    pub mu_batching_bits: f64,
+}
+
+#[derive(Clone, Debug)]
+pub struct ProximityGapSecurity {
+    pub log2_err: f64,
+    pub log2_list_size: f64,
 }
 
 impl SoundnessCalculator {
@@ -75,9 +90,19 @@ impl SoundnessCalculator {
         num_trace_columns: usize,
         num_stacked_columns: usize,
         n_logup: usize,
-        proximity_regime: ProximityRegime,
     ) -> Self {
-        let logup_bits = Self::calculate_logup_soundness(params, challenge_field_bits);
+        let init_prox_gap = Self::whir_proximity_gap_security(
+            params.whir.proximity.initial_round(),
+            challenge_field_bits,
+            params.log_stacked_height(),
+            params.log_blowup,
+            num_stacked_columns,
+        );
+        // log2_list_size is log2(L_{PCS}) where L_{PCS} is the list size with respect to the
+        // proximity radius of the _initial_ WHIR round.
+        let log2_list_size = init_prox_gap.log2_list_size;
+        let logup_bits =
+            Self::calculate_logup_soundness(params, challenge_field_bits, log2_list_size);
 
         let gkr_sumcheck_bits =
             Self::calculate_gkr_sumcheck_soundness(challenge_field_bits, params.l_skip, n_logup);
@@ -90,12 +115,14 @@ impl SoundnessCalculator {
             max_constraint_degree,
             params.l_skip,
             max_log_trace_height,
+            log2_list_size,
         );
 
         let constraint_batching_bits = Self::calculate_constraint_batching_soundness(
             challenge_field_bits,
             max_num_constraints_per_air,
             num_airs,
+            log2_list_size,
         );
 
         let stacked_reduction_bits = Self::calculate_stacked_reduction_soundness(
@@ -103,13 +130,14 @@ impl SoundnessCalculator {
             num_trace_columns,
             params.l_skip,
             params.n_stack,
+            log2_list_size,
         );
 
         let (whir_bits, whir_details) = Self::calculate_whir_soundness(
             params,
             challenge_field_bits,
             num_stacked_columns,
-            proximity_regime,
+            params.whir.proximity,
         );
 
         let total_bits = logup_bits
@@ -144,11 +172,17 @@ impl SoundnessCalculator {
     /// Security = |F_ext| - log₂(2 × max_interaction_count) - log_max_message_length + pow_bits
     ///
     /// Reference: Section 4 of docs/Soundness_of_Interactions_via_LogUp.pdf
-    fn calculate_logup_soundness(params: &SystemParams, challenge_field_bits: f64) -> f64 {
+    fn calculate_logup_soundness(
+        params: &SystemParams,
+        challenge_field_bits: f64,
+        log2_list_size: f64,
+    ) -> f64 {
         let logup = &params.logup;
         let max_interaction_count_bits = (2.0 * logup.max_interaction_count as f64).log2();
 
-        challenge_field_bits - max_interaction_count_bits - logup.log_max_message_length as f64
+        log2_list_size + challenge_field_bits
+            - max_interaction_count_bits
+            - logup.log_max_message_length as f64
             + logup.pow_bits as f64
     }
 
@@ -207,6 +241,7 @@ impl SoundnessCalculator {
         max_constraint_degree: usize,
         l_skip: usize,
         max_log_trace_height: usize,
+        log2_list_size: f64,
     ) -> f64 {
         let univariate_degree = (max_constraint_degree + 1) * ((1 << l_skip) - 1);
         let multilinear_degree = max_constraint_degree + 1;
@@ -220,7 +255,7 @@ impl SoundnessCalculator {
         let poly_degree_sum = (1 << l_skip) - 1 + n_max;
         let poly_identity_bits = challenge_field_bits - (poly_degree_sum as f64).log2();
 
-        sumcheck_bits.min(poly_identity_bits)
+        log2_list_size + sumcheck_bits.min(poly_identity_bits)
     }
 
     /// Constraint batching soundness via Schwartz-Zippel.
@@ -233,6 +268,7 @@ impl SoundnessCalculator {
         challenge_field_bits: f64,
         max_num_constraints_per_air: usize,
         num_airs: usize,
+        log2_list_size: f64,
     ) -> f64 {
         let lambda_batching_bits =
             challenge_field_bits - (max_num_constraints_per_air as f64).log2();
@@ -242,7 +278,7 @@ impl SoundnessCalculator {
         // 3. LogUp denominator (q̂(ξ) input layer)
         let mu_batching_bits = challenge_field_bits - (3.0 * num_airs as f64).log2();
 
-        lambda_batching_bits.min(mu_batching_bits)
+        log2_list_size + lambda_batching_bits.min(mu_batching_bits)
     }
 
     /// Stacked reduction soundness.
@@ -261,6 +297,7 @@ impl SoundnessCalculator {
         num_trace_columns: usize,
         l_skip: usize,
         _n_stack: usize,
+        log2_list_size: f64,
     ) -> f64 {
         let batching_bits = challenge_field_bits - (2.0 * num_trace_columns as f64).log2();
 
@@ -270,22 +307,21 @@ impl SoundnessCalculator {
         // Degree 2 per round => log2(2) = 1.
         let multilinear_bits = challenge_field_bits - 1.0;
 
-        batching_bits.min(univariate_bits).min(multilinear_bits)
+        log2_list_size + batching_bits.min(univariate_bits).min(multilinear_bits)
     }
 
     /// WHIR soundness analysis based on the WHIR paper (ePrint 2024/1586).
     ///
-    /// Error sources (current formulas assume unique decoding, ℓ = 1):
+    /// Error sources (formulas depend on the proximity regime):
     /// 1. **Fold error** (sumcheck + proximity gap per sub-round)
     /// 2. **OOD error** (non-final rounds)
-    /// 3. **Query error** (all rounds)
-    /// 4. **γ batching** (in-domain batching)
+    /// 3. **Shift/final error** (query sampling + γ batching)
     /// 5. **Initial μ batching**
     fn calculate_whir_soundness(
         params: &SystemParams,
         challenge_field_bits: f64,
         num_stacked_columns: usize,
-        proximity_regime: ProximityRegime,
+        proximity: WhirProximityStrategy,
     ) -> (f64, WhirSoundnessCalculator) {
         let whir = &params.whir;
         let k_whir = whir.k;
@@ -297,36 +333,50 @@ impl SoundnessCalculator {
         let mut min_sumcheck_bits = f64::INFINITY;
         let mut min_ood_bits = f64::INFINITY;
         let mut min_gamma_batching_bits = f64::INFINITY;
+        let mut min_fold_rbr_bits = f64::INFINITY;
+        let mut min_shift_rbr_bits = f64::INFINITY;
 
         assert!(
             num_stacked_columns >= 2,
             "WHIR requires at least 2 stacked columns for μ batching"
         );
-        let mu_batching_bits = Self::whir_proximity_gap_security(
-            proximity_regime,
+        let mu_security = Self::whir_proximity_gap_security(
+            proximity.initial_round(),
             challenge_field_bits,
             log_stacked_height,
             params.log_blowup,
             num_stacked_columns,
-        ) + whir.mu_pow_bits as f64;
+        );
+        let mu_batching_bits = mu_security.log2_err + whir.mu_pow_bits as f64;
+        let mut min_rbr_bits = mu_batching_bits;
 
         let mut log_inv_rate = params.log_blowup;
         let mut current_log_degree = log_stacked_height;
 
         for (round, round_config) in whir.rounds.iter().enumerate() {
+            let proximity_regime = proximity.in_round(round);
             let is_final_round = round == num_whir_rounds - 1;
             let next_rate = log_inv_rate + (k_whir - 1);
+            // log2(list size) only depends on proximity regime, will not change depending on the
+            // sub-round
+            let mut log2_list_size: Option<f64> = None;
 
             for sub_round in 0..k_whir {
                 current_log_degree -= 1;
 
-                let prox_gaps_bits = Self::whir_proximity_gap_security(
+                let prox_gaps = Self::whir_proximity_gap_security(
                     proximity_regime,
                     challenge_field_bits,
                     current_log_degree,
                     log_inv_rate,
                     2,
-                ) + whir.folding_pow_bits as f64;
+                );
+                if let Some(l2) = log2_list_size.as_mut() {
+                    debug_assert!((*l2 - prox_gaps.log2_list_size).abs() < 1e-6);
+                } else {
+                    log2_list_size = Some(prox_gaps.log2_list_size);
+                }
+                let prox_gaps_bits = prox_gaps.log2_err + whir.folding_pow_bits as f64;
                 min_prox_gaps_bits = min_prox_gaps_bits.min(prox_gaps_bits);
 
                 let sumcheck_bits = Self::whir_sumcheck_security(
@@ -335,6 +385,11 @@ impl SoundnessCalculator {
                     whir.folding_pow_bits,
                 );
                 min_sumcheck_bits = min_sumcheck_bits.min(sumcheck_bits);
+
+                // Theorem 5.2: ε_fold = d * ℓ / |F| + err*.
+                let fold_rbr_bits = Self::combine_security_bits(sumcheck_bits, prox_gaps_bits);
+                min_fold_rbr_bits = min_fold_rbr_bits.min(fold_rbr_bits);
+                min_rbr_bits = min_rbr_bits.min(fold_rbr_bits);
             }
 
             // Query error (all rounds), protected by query_phase_pow_bits.
@@ -349,29 +404,43 @@ impl SoundnessCalculator {
             let batch_size = round_config.num_queries + NUM_OOD_SAMPLES;
             debug_assert!(batch_size > 0);
             let gamma_batching_bits = Self::whir_gamma_batching_security(
-                proximity_regime,
                 challenge_field_bits,
                 batch_size,
+                log2_list_size.unwrap(),
             );
             min_gamma_batching_bits = min_gamma_batching_bits.min(gamma_batching_bits);
 
+            // Theorem 5.2 / Claim 5.4: ε_shift = (1 - δ)^t + ℓ * (t + 1) / |F|. The implementation
+            // keeps the same additive structure, with the final round batching only the query
+            // claims.
+            let shift_rbr_bits = Self::combine_security_bits(query_bits, gamma_batching_bits);
+            min_shift_rbr_bits = min_shift_rbr_bits.min(shift_rbr_bits);
+            min_rbr_bits = min_rbr_bits.min(shift_rbr_bits);
+
             if !is_final_round {
                 // OOD error (not protected by PoW; sampled after commitment observed).
-                let log_degree_at_round_start = current_log_degree + k_whir;
-                let ood_bits =
-                    Self::whir_ood_security(challenge_field_bits, log_degree_at_round_start);
+                // This is OOD sample on f_i for the *next* round `i = round + 1` after folding. So
+                // `m_i = current_log_degree` (with the present round `round`'s foldings)
+                let ood_bits = Self::whir_ood_security(
+                    log2_list_size.unwrap(),
+                    challenge_field_bits,
+                    current_log_degree,
+                );
                 min_ood_bits = min_ood_bits.min(ood_bits);
+                min_rbr_bits = min_rbr_bits.min(ood_bits);
 
                 tracing::debug!(
-                    "WHIR round {} | rate=2^-{} | queries={} | query={:.1} | prox_gaps={:.1} | sumcheck={:.1} | ood={:.1} | gamma={:.1}",
+                    "WHIR round {} | rate=2^-{} | queries={} | query={:.1} | prox_gaps={:.1} | sumcheck={:.1} | shift={:.1} | ood={:.1} | gamma={:.1}",
                     round, log_inv_rate, round_config.num_queries, query_bits,
-                    min_prox_gaps_bits, min_sumcheck_bits, ood_bits, min_gamma_batching_bits,
+                    min_prox_gaps_bits, min_sumcheck_bits, shift_rbr_bits, ood_bits,
+                    min_gamma_batching_bits,
                 );
             } else {
                 tracing::debug!(
-                    "WHIR round {} (final) | rate=2^-{} | queries={} | query={:.1} | prox_gaps={:.1} | sumcheck={:.1} | gamma={:.1}",
+                    "WHIR round {} (final) | rate=2^-{} | queries={} | query={:.1} | prox_gaps={:.1} | sumcheck={:.1} | final={:.1} | gamma={:.1}",
                     round, log_inv_rate, round_config.num_queries, query_bits,
-                    min_prox_gaps_bits, min_sumcheck_bits, min_gamma_batching_bits,
+                    min_prox_gaps_bits, min_sumcheck_bits, shift_rbr_bits,
+                    min_gamma_batching_bits,
                 );
             }
 
@@ -379,20 +448,18 @@ impl SoundnessCalculator {
         }
 
         let details = WhirSoundnessCalculator {
+            mu_batching_bits,
+            fold_rbr_bits: min_fold_rbr_bits,
+            ood_rbr_bits: min_ood_bits,
+            shift_rbr_bits: min_shift_rbr_bits,
+            // The following are part of above rbr error, but kept for detailed analysis
             query_bits: min_query_bits,
             proximity_gaps_bits: min_prox_gaps_bits,
             sumcheck_bits: min_sumcheck_bits,
-            ood_bits: min_ood_bits,
             gamma_batching_bits: min_gamma_batching_bits,
-            mu_batching_bits,
         };
 
-        let min_security = min_query_bits
-            .min(min_prox_gaps_bits)
-            .min(min_sumcheck_bits)
-            .min(min_ood_bits)
-            .min(min_gamma_batching_bits)
-            .min(mu_batching_bits);
+        let min_security = min_rbr_bits;
 
         (min_security, details)
     }
@@ -401,23 +468,220 @@ impl SoundnessCalculator {
     ///
     /// Per WHIR paper: err*(C, ℓ, δ) = (ℓ - 1) · 2^m / (ρ · |F|)
     ///
-    /// Unique decoding formula:
-    /// Security bits = |F_ext| - log₂(ℓ - 1) - log₂(degree) - log₂(1/rate)
+    /// - `UniqueDecoding`: Security bits = |F_ext| - log₂(ℓ - 1) - log₂(degree) - log₂(1/rate)
+    /// - `ListDecoding { m }`: Uses BCHKS25/TR25-169 Theorem 1.5 (contrapositive) to bound the "bad
+    ///   z set" size by `a`, with Haböck's global extension introducing a linear factor `(ℓ - 1)`.
     pub fn whir_proximity_gap_security(
         proximity_regime: ProximityRegime,
         challenge_field_bits: f64,
         log_degree: usize,
         log_inv_rate: usize,
         batch_size: usize,
-    ) -> f64 {
+    ) -> ProximityGapSecurity {
         debug_assert!(batch_size > 1, "batch_size must be > 1 for err*");
         match proximity_regime {
             ProximityRegime::UniqueDecoding => {
-                challenge_field_bits
+                let log2_err = challenge_field_bits
                     - ((batch_size - 1) as f64).log2()
                     - log_degree as f64
-                    - log_inv_rate as f64
+                    - log_inv_rate as f64;
+                ProximityGapSecurity {
+                    log2_err,
+                    log2_list_size: 0.0,
+                }
             }
+            ProximityRegime::ListDecoding { m } => {
+                let (log2_a, log2_list_size) =
+                    Self::log2_a_bound_bchks25(log_degree, log_inv_rate, m);
+                // Haböck global mutual correlated agreement: error ∝ (ℓ - 1) * a / |F|.
+                let log2_err = challenge_field_bits - ((batch_size - 1) as f64).log2() - log2_a;
+                ProximityGapSecurity {
+                    log2_err,
+                    log2_list_size,
+                }
+            }
+        }
+    }
+
+    /// Numerically stable `log2(2^x + 2^y)`.
+    #[inline]
+    fn log2_add(log2_x: f64, log2_y: f64) -> f64 {
+        if log2_x.is_infinite() && log2_x.is_sign_positive() {
+            return log2_x;
+        }
+        if log2_y.is_infinite() && log2_y.is_sign_positive() {
+            return log2_y;
+        }
+        if log2_x.is_nan() || log2_y.is_nan() {
+            return f64::NAN;
+        }
+
+        let (hi, lo) = if log2_x >= log2_y {
+            (log2_x, log2_y)
+        } else {
+            (log2_y, log2_x)
+        };
+        let ratio = (lo - hi).exp2();
+        hi + (1.0 + ratio).log2()
+    }
+
+    /// Combines two additive error terms `2^-a + 2^-b` into security bits `-log2(error)`.
+    #[inline]
+    fn combine_security_bits(bits_a: f64, bits_b: f64) -> f64 {
+        if bits_a.is_infinite() && bits_a.is_sign_positive() {
+            return bits_b;
+        }
+        if bits_b.is_infinite() && bits_b.is_sign_positive() {
+            return bits_a;
+        }
+        if bits_a.is_nan() || bits_b.is_nan() {
+            return f64::NAN;
+        }
+
+        -Self::log2_add(-bits_a, -bits_b)
+    }
+
+    #[inline]
+    fn bchks25_log2_a_from_log2_degrees(
+        log2_d_x: f64,
+        log2_d_y: f64,
+        log2_d_z: f64,
+        log2_agreement_term: f64,
+    ) -> f64 {
+        // Equation (13): a > 2*D_X*D_Y^2*D_Z + agreement_term*D_Y
+        let log2_term_poly = 1.0 + log2_d_x + 2.0 * log2_d_y + log2_d_z;
+        let log2_term_gamma = log2_d_y + log2_agreement_term;
+        Self::log2_add(log2_term_poly, log2_term_gamma)
+    }
+
+    /// Reference closed-form degrees from BCHKS25 Lemma 3.1, Equations (7), (8), (9).
+    /// For `m < 3`, use `D_Z = max(D_Y, Equation (9) value)` as noted below Lemma 3.1.
+    ///
+    /// Returns (log2(D_X), log2(D_Y), log2(D_Z))
+    fn bchks25_log2_degrees(
+        log_degree: usize,
+        log_inv_rate: usize,
+        m: usize,
+        _gamma: f64,
+    ) -> (f64, f64, f64) {
+        #[cfg(feature = "soundness-bchks25-optimized")]
+        if let Some((degrees, _)) = bchks25_brute_force_params::bchks25_optimal_degrees_bruteforce(
+            log_degree,
+            log_inv_rate,
+            m,
+            _gamma,
+        ) {
+            debug_assert!(degrees.d_x > 0 && degrees.d_y > 0 && degrees.d_z > 0);
+            return (
+                (degrees.d_x as f64).log2(),
+                (degrees.d_y as f64).log2(),
+                (degrees.d_z as f64).log2(),
+            );
+        }
+
+        Self::bchks25_reference_log2_degrees(log_degree, log_inv_rate, m)
+    }
+
+    fn bchks25_reference_log2_degrees(
+        log_degree: usize,
+        log_inv_rate: usize,
+        m: usize,
+    ) -> (f64, f64, f64) {
+        let m_bar = m.max(1) as f64 + 0.5;
+        let log2_m_bar = m_bar.log2();
+        let log2_n = (log_degree + log_inv_rate) as f64;
+        let log2_3 = 3.0_f64.log2();
+        let log2_rho = -(log_inv_rate as f64);
+
+        // D_X = (m + 1/2) * sqrt(k * n)
+        // D_Y = (m + 1/2) * sqrt(n / k)
+        // D_Z (Equation 9) = ((m + 1/2)^2 * n) / (3 * k)
+        let log2_d_x = log2_m_bar + log2_n + 0.5 * log2_rho;
+        let log2_d_y = log2_m_bar - 0.5 * log2_rho;
+        let log2_d_z = 2.0 * log2_m_bar - log2_3 - log2_rho;
+        let log2_d_z = if m < 3 {
+            log2_d_y.max(log2_d_z)
+        } else {
+            log2_d_z
+        };
+
+        (log2_d_x, log2_d_y, log2_d_z)
+    }
+
+    /// Computes `log2(a_bound)` from BCHKS25/TR25-169 Theorem 1.5 (contrapositive), where
+    /// `a_bound = ceil(a).max(1)`.
+    ///
+    /// We use Lemma 3.1 and the bounds on `a` in terms of `D_X, D_Y, D_Z` from Section 3.2 and
+    /// Equation (13). As noted in the paragraph after Lemma 3.1, the parameters chosen in the
+    /// Lemma 3.1 statement are not optimal and chosen to provide cleaner expressions.
+    /// We do a brute-force search in `bchks25_optimal_degrees_bruteforce` to find parameters that
+    /// meet the conditions for the proof of Lemma 3.1 to be applied to find the polynomial `Q`.
+    ///
+    /// A closed-form Lemma 3.1 degree computation is kept in
+    /// `bchks25_reference_log2_degrees` for fallback/reference.
+    ///
+    /// Parameters are mapped as:
+    /// - `num_variables = log_degree`
+    /// - `rho = 2^{-log_inv_rate}`
+    /// - `n = 2^{log_degree + log_inv_rate}`
+    ///
+    /// We set the theorem slack `η` from the provided multiplicity `m` as
+    /// `η = sqrt(rho) / (2m)`, so that `m = ceil(sqrt(rho)/(2η))`.
+    ///
+    /// Returns `log2(a_bound), log2(list_size)`.
+    fn log2_a_bound_bchks25(log_degree: usize, log_inv_rate: usize, m: usize) -> (f64, f64) {
+        const INVALID: (f64, f64) = (f64::INFINITY, f64::INFINITY);
+        let m_eff = m.max(1);
+        let log2_rho = -(log_inv_rate as f64);
+        let rho = log2_rho.exp2();
+        if rho <= 0.0 || !rho.is_finite() {
+            return INVALID;
+        }
+        if m_eff == 1 && rho >= (4.0 / 9.0) {
+            // For m=1: gamma = 1 - sqrt(rho) - sqrt(rho)/(2m) = 1 - 3*sqrt(rho)/2.
+            // Gamma must be positive to apply the Section 3.2 argument.
+            return INVALID;
+        }
+
+        let sqrt_rho = rho.sqrt();
+        let eta = sqrt_rho / (2.0 * m_eff as f64);
+        let gamma = 1.0 - sqrt_rho - eta;
+        if eta <= 0.0 || gamma <= 0.0 || gamma >= 1.0 - sqrt_rho {
+            // Invalid theorem regime => no security from this term.
+            return INVALID;
+        }
+
+        let log2_n = (log_degree + log_inv_rate) as f64;
+        let (log2_a_real, log2_list_size) = {
+            // Fallback for extreme parameter regimes where exact integer search is not
+            // representable.
+            let (log2_d_x, log2_d_y, log2_d_z) =
+                Self::bchks25_log2_degrees(log_degree, log_inv_rate, m_eff, gamma);
+            let log2_gamma_n_plus_1 = Self::log2_add(gamma.log2() + log2_n, 0.0);
+            let log2_a = Self::bchks25_log2_a_from_log2_degrees(
+                log2_d_x,
+                log2_d_y,
+                log2_d_z,
+                log2_gamma_n_plus_1,
+            );
+            // Note: we could take log2(floor(2^log2_d_y)) for a tighter list size bound
+            (log2_a, log2_d_y)
+        };
+        if !log2_a_real.is_finite() {
+            return INVALID;
+        }
+
+        // Clamp `a_bound >= 1` => `log2(a_bound) >= 0`.
+        let log2_a_real = log2_a_real.max(0.0);
+
+        // If `a` is small enough, apply `ceil` in normal space for exactness.
+        if log2_a_real < 52.0 {
+            let a = log2_a_real.exp2();
+            let a_bound = a.ceil().max(1.0);
+            (a_bound.log2(), log2_list_size)
+        } else {
+            // For large `a`, `ceil` does not materially affect `log2(a)`.
+            (log2_a_real, log2_list_size)
         }
     }
 
@@ -436,27 +700,28 @@ impl SoundnessCalculator {
 
     /// Computes WHIR out-of-domain (OOD) security bits.
     ///
-    /// OOD error is 2^{m - 1} / |F| where m is the log_degree at round start.
-    /// Security bits = |F_ext| - log_degree + 1
-    fn whir_ood_security(challenge_field_bits: f64, log_degree_at_round_start: usize) -> f64 {
-        challenge_field_bits - log_degree_at_round_start as f64 + 1.0
+    /// OOD error is 2^{m_i - 1} ℓ^2 / |F| where m_i is the log_degree at the start of WHIR round
+    /// `i`. Security bits = |F_ext| - log_degree + 1
+    fn whir_ood_security(
+        log2_list_size: f64,
+        challenge_field_bits: f64,
+        log_degree_at_round_start: usize,
+    ) -> f64 {
+        let base_bits = challenge_field_bits - log_degree_at_round_start as f64 + 1.0;
+        base_bits - 2.0 * log2_list_size
     }
 
     /// Computes WHIR in-domain γ batching security bits.
     ///
-    /// In-domain batching error is (t - 1) / |F| for batch size t.
-    /// Security bits = |F_ext| - log₂(t - 1)
+    /// Theorem 5.6 / Claim 5.4: batching `t` claims against a list of size `ℓ` gives
+    /// error `ℓ * t / |F|`.
     fn whir_gamma_batching_security(
-        proximity_regime: ProximityRegime,
         challenge_field_bits: f64,
         batch_size: usize,
+        log2_list_size: f64,
     ) -> f64 {
-        debug_assert!(batch_size > 1, "batch_size must be > 1 for gamma batching");
-        match proximity_regime {
-            ProximityRegime::UniqueDecoding => {
-                challenge_field_bits - ((batch_size - 1) as f64).log2()
-            }
-        }
+        debug_assert!(batch_size > 0, "batch_size must be > 0 for gamma batching");
+        challenge_field_bits - (batch_size as f64).log2() - log2_list_size
     }
 }
 
@@ -484,7 +749,6 @@ pub fn print_soundness_report(
         num_trace_columns,
         num_stacked_columns,
         n_logup,
-        proximity_regime,
     );
 
     println!("=== V2 Proof System Soundness Report ===");
@@ -547,7 +811,7 @@ pub fn print_soundness_report(
         "  Stacked reduction:           {:.1}",
         soundness.stacked_reduction_bits
     );
-    println!("  WHIR (min across sources):   {:.1}", soundness.whir_bits);
+    println!("  WHIR (round-by-round min):   {:.1}", soundness.whir_bits);
     println!();
     println!(
         "  TOTAL SECURITY:              {:.1} bits",
@@ -563,11 +827,13 @@ pub fn print_soundness_report(
         whir.proximity_gaps_bits
     );
     println!("  Sumcheck error:       {:.1} bits", whir.sumcheck_bits);
-    println!("  OOD error:            {:.1} bits", whir.ood_bits);
+    println!("  Min ε_fold:           {:.1} bits", whir.fold_rbr_bits);
+    println!("  OOD error:            {:.1} bits", whir.ood_rbr_bits);
     println!(
         "  γ batching error:     {:.1} bits",
         whir.gamma_batching_bits
     );
+    println!("  Min ε_shift/ε_fin:    {:.1} bits", whir.shift_rbr_bits);
     println!("  μ batching error:     {:.1} bits", whir.mu_batching_bits);
     println!();
 
@@ -601,13 +867,15 @@ pub fn min_whir_queries(
 
 #[cfg(test)]
 mod tests {
-    use openvm_stark_sdk::config::log_up_params::log_up_security_params_baby_bear_100_bits as sdk_log_up_security_params_baby_bear_100_bits;
     use p3_baby_bear::BabyBear;
     use p3_field::PrimeField64;
 
     use super::*;
-    use crate::{config::WhirRoundConfig, interaction::LogUpSecurityParameters, WhirParams};
+    use crate::{config::WhirRoundConfig, interaction::LogUpSecurityParameters};
 
+    fn babybear_quartic_extension_bits() -> f64 {
+        4.0 * (BabyBear::ORDER_U64 as f64).log2()
+    }
     // ==========================================================================
     // Test fixtures
     // ==========================================================================
@@ -627,6 +895,7 @@ mod tests {
                 mu_pow_bits: 16,
                 query_phase_pow_bits: 16,
                 folding_pow_bits: 10,
+                proximity: WhirProximityStrategy::UniqueDecoding,
             },
             logup: LogUpSecurityParameters {
                 max_interaction_count: 1 << 20,
@@ -637,165 +906,10 @@ mod tests {
         }
     }
 
-    // ==========================================================================
-    // Production configurations
-    //
-    // These must be kept in sync with v2-proof-system/crates/sdk/src/config.rs:
-    //   - default_app_params()
-    //   - default_leaf_params()
-    //   - default_internal_params()
-    //   - default_compression_params()
-    //
-    // When production params change in the SDK, update these values accordingly.
-    // ==========================================================================
-
-    // From SDK config.rs constants
-    const WHIR_MAX_LOG_FINAL_POLY_LEN: usize = 10;
-    const WHIR_POW_BITS: usize = 20;
-    const SECURITY_BITS_TARGET: usize = 100;
-    fn babybear_quartic_extension_bits() -> f64 {
-        4.0 * (BabyBear::ORDER_U64 as f64).log2()
-    }
-
-    // From SDK config.rs: DEFAULT_APP_L_SKIP, DEFAULT_APP_LOG_BLOWUP, etc.
-    const DEFAULT_APP_L_SKIP: usize = 4;
-    const DEFAULT_APP_LOG_BLOWUP: usize = 1;
-    const DEFAULT_LEAF_LOG_BLOWUP: usize = 2;
-    const DEFAULT_INTERNAL_LOG_BLOWUP: usize = 2;
-    const DEFAULT_COMPRESSION_LOG_BLOWUP: usize = 4;
-
-    fn production_system_params(
-        log_blowup: usize,
-        l_skip: usize,
-        n_stack: usize,
-        w_stack: usize,
-        log_final_poly_len: usize,
-    ) -> SystemParams {
-        let k_whir = 4;
-        let max_constraint_degree = 4;
-        let log_stacked_height = l_skip + n_stack;
-
-        SystemParams {
-            l_skip,
-            n_stack,
-            w_stack,
-            log_blowup,
-            whir: WhirConfig::new(
-                log_blowup,
-                log_stacked_height,
-                WhirParams {
-                    k: k_whir,
-                    log_final_poly_len,
-                    query_phase_pow_bits: WHIR_POW_BITS,
-                },
-                SECURITY_BITS_TARGET,
-            ),
-            logup: log_up_security_params_baby_bear_100_bits_local(),
-            max_constraint_degree,
-        }
-    }
-
-    fn log_up_security_params_baby_bear_100_bits_local() -> LogUpSecurityParameters {
-        let params = sdk_log_up_security_params_baby_bear_100_bits();
-        LogUpSecurityParameters {
-            max_interaction_count: params.max_interaction_count,
-            log_max_message_length: params.log_max_message_length,
-            pow_bits: params.pow_bits,
-        }
-    }
-
-    /// App VM params: from SDK default_app_params(DEFAULT_APP_LOG_BLOWUP, DEFAULT_APP_L_SKIP, 20)
-    fn app_params() -> SystemParams {
-        production_system_params(
-            DEFAULT_APP_LOG_BLOWUP,
-            DEFAULT_APP_L_SKIP,
-            20,
-            2048,
-            WHIR_MAX_LOG_FINAL_POLY_LEN,
-        )
-    }
-
-    /// Leaf params: from SDK default_leaf_params(DEFAULT_LEAF_LOG_BLOWUP)
-    /// l_skip=2, n_stack=18
-    fn leaf_params() -> SystemParams {
-        production_system_params(
-            DEFAULT_LEAF_LOG_BLOWUP,
-            2,
-            18,
-            1024,
-            WHIR_MAX_LOG_FINAL_POLY_LEN,
-        )
-    }
-
-    /// Internal params: from SDK default_internal_params(DEFAULT_INTERNAL_LOG_BLOWUP)
-    /// l_skip=2, n_stack=17
-    fn internal_params() -> SystemParams {
-        production_system_params(
-            DEFAULT_INTERNAL_LOG_BLOWUP,
-            2,
-            17,
-            1024,
-            WHIR_MAX_LOG_FINAL_POLY_LEN,
-        )
-    }
-
-    /// Compression params: from SDK default_compression_params(DEFAULT_COMPRESSION_LOG_BLOWUP)
-    /// l_skip=2, n_stack=20, log_final_poly_len=11 (different from others!)
-    fn compression_params() -> SystemParams {
-        production_system_params(DEFAULT_COMPRESSION_LOG_BLOWUP, 2, 20, 64, 11)
-    }
-
-    // ==========================================================================
-    // Circuit parameter upper bounds for soundness analysis
-    //
-    // These are conservative estimates based on actual production values.
-    // Stacking can only reduce width, so num_columns is an upper bound on stacked columns.
-    // ==========================================================================
-
-    /// Upper bound on n_logup derived from circuit parameters.
-    ///
-    /// n_logup = ceil_log2(total_interactions) - l_skip, where:
-    /// - total_interactions ≤ num_airs × max_interactions_per_air × 2^max_log_height
-    /// - total_interactions < max_interaction_count (enforced by verifier as one of the
-    ///   `LinearConstraint`s, keygen ensures this linear constraint is included)
-    ///
-    /// So: n_logup ≤ min(ceil_log2(max_interaction_count) - l_skip, log2(num_airs ×
-    /// max_interactions) + max_log_height - l_skip)
-    fn n_logup_bound(
-        l_skip: usize,
-        num_airs: usize,
-        max_interactions_per_air: usize,
-        max_log_height: usize,
-        max_interaction_count: usize,
-    ) -> usize {
-        let field_bound = (max_interaction_count as f64).log2().ceil() as usize - l_skip;
-        let param_bound = (num_airs as f64).log2().ceil() as usize
-            + (max_interactions_per_air as f64).log2().ceil() as usize
-            + max_log_height
-            - l_skip;
-        field_bound.min(param_bound)
-    }
-
-    // App VM: large circuits with many AIRs
-    // Actual: max_constraints=4513 (keccak), num_airs=73, max_interactions=832
-    const APP_MAX_CONSTRAINTS: usize = 5000;
-    const APP_NUM_AIRS: usize = 100;
-    const APP_MAX_LOG_HEIGHT: usize = 24;
-    const APP_NUM_COLUMNS: usize = 30000;
-    const APP_MAX_INTERACTIONS_PER_AIR: usize = 1000;
-
-    // Recursion circuits: smaller, fixed structure
-    // Actual: num_airs=42
-    const RECURSION_MAX_CONSTRAINTS: usize = 1000;
-    const RECURSION_NUM_AIRS: usize = 50;
-    const RECURSION_NUM_COLUMNS: usize = 2000;
-    const RECURSION_MAX_INTERACTIONS_PER_AIR: usize = 100; // estimate, needs verification
-
-    const TARGET_SECURITY_BITS: usize = 100;
-
     // ==========================================================================
     // Unit tests
     // ==========================================================================
+    const TARGET_SECURITY_BITS: usize = 100;
 
     #[test]
     fn test_soundness_calculation() {
@@ -810,7 +924,6 @@ mod tests {
             200,
             10,
             15,
-            ProximityRegime::UniqueDecoding,
         );
 
         assert!(soundness.logup_bits > 0.0);
@@ -845,6 +958,7 @@ mod tests {
         let security = SoundnessCalculator::calculate_logup_soundness(
             &params,
             babybear_quartic_extension_bits(),
+            0.0,
         );
         assert!(security > TARGET_SECURITY_BITS as f64);
     }
@@ -868,275 +982,504 @@ mod tests {
         );
     }
 
-    // ==========================================================================
-    // Production configuration tests
-    // ==========================================================================
+    #[test]
+    fn test_whir_gamma_batching_uses_list_size_and_full_batch_size() {
+        let security = SoundnessCalculator::whir_gamma_batching_security(100.0, 5, 3.0);
+        let expected = 100.0 - 5.0_f64.log2() - 3.0;
+        assert!((security - expected).abs() < 1e-9);
+    }
 
-    fn check_soundness(
-        name: &str,
-        params: &SystemParams,
-        max_constraints: usize,
-        num_airs: usize,
-        max_log_height: usize,
-        num_columns: usize,
-        n_logup: usize,
-    ) -> SoundnessCalculator {
-        let soundness = SoundnessCalculator::calculate(
-            params,
-            babybear_quartic_extension_bits(),
-            max_constraints,
-            num_airs,
-            params.max_constraint_degree,
-            max_log_height,
-            num_columns,
-            params.w_stack,
-            n_logup,
-            ProximityRegime::UniqueDecoding,
-        );
+    #[test]
+    fn test_combine_security_bits_sums_errors_before_taking_log() {
+        let combined = SoundnessCalculator::combine_security_bits(100.0, 100.0);
+        let expected = 99.0;
+        assert!((combined - expected).abs() < 1e-9);
+    }
 
-        println!("\n=== {} Soundness ===", name);
-        println!(
-            "Config: l_skip={}, n_stack={}, w_stack={}, log_blowup={}, k_whir={}",
-            params.l_skip, params.n_stack, params.w_stack, params.log_blowup, params.whir.k
-        );
-        println!(
-            "Context: max_constraints={}, num_airs={}, max_log_height={}, num_columns={}, n_logup={}",
-            max_constraints, num_airs, max_log_height, num_columns, n_logup
-        );
-        println!();
-        println!("LogUp (α/β + PoW):   {:.1} bits", soundness.logup_bits);
-        println!(
-            "GKR sumcheck:        {:.1} bits",
-            soundness.gkr_sumcheck_bits
-        );
-        println!(
-            "GKR batching (μ/λ):  {:.1} bits",
-            soundness.gkr_batching_bits
-        );
-        println!(
-            "ZeroCheck sumcheck:  {:.1} bits",
-            soundness.zerocheck_sumcheck_bits
-        );
-        println!(
-            "Constraint batching: {:.1} bits",
-            soundness.constraint_batching_bits
-        );
-        println!(
-            "Stacked reduction:   {:.1} bits",
-            soundness.stacked_reduction_bits
-        );
-        println!("WHIR:                {:.1} bits", soundness.whir_bits);
-        println!("TOTAL:               {:.1} bits", soundness.total_bits);
+    #[test]
+    fn test_bchks25_reference_m2_enforces_dz_ge_dy() {
+        let (_log2_d_x, log2_d_y, log2_d_z) =
+            SoundnessCalculator::bchks25_reference_log2_degrees(24, 2, 2);
+        assert!(log2_d_z >= log2_d_y);
+    }
 
-        println!("\nWHIR Error Source Breakdown:");
-        let whir = &soundness.whir_details;
-        println!("  Query error:          {:.1} bits", whir.query_bits);
-        println!(
-            "  Proximity gaps:       {:.1} bits",
-            whir.proximity_gaps_bits
-        );
-        println!("  Sumcheck error:       {:.1} bits", whir.sumcheck_bits);
-        println!("  OOD error:            {:.1} bits", whir.ood_bits);
-        println!(
-            "  γ batching error:     {:.1} bits",
-            whir.gamma_batching_bits
-        );
-        println!("  μ batching error:     {:.1} bits", whir.mu_batching_bits);
+    #[test]
+    fn test_bchks25_m1_requires_rho_below_four_ninths() {
+        // log_inv_rate=1 => rho=1/2 > 4/9, so m=1 regime is invalid.
+        let invalid = SoundnessCalculator::log2_a_bound_bchks25(12, 1, 1);
+        assert!(invalid.0.is_infinite() && invalid.1.is_infinite());
+
+        // log_inv_rate=2 => rho=1/4 < 4/9, so m=1 regime is admissible.
+        let valid = SoundnessCalculator::log2_a_bound_bchks25(12, 2, 1);
+        assert!(valid.0.is_finite() && valid.1.is_finite());
+    }
+}
 
-        soundness
+/// The D_X, D_Y, D_Z given in [BCHKS25] Lemma 3.1 are not optimal (as noted by the authors) and `m
+/// < 3` assumption is not needed. We can perform a brute force search over possible values of D_X,
+/// D_Y, D_Z that satisfy properties to allow the proof of Lemma 3.1 to go through.
+///
+/// Everything in this module is still backed by proven results.
+#[allow(dead_code)]
+#[cfg(feature = "soundness-bchks25-optimized")]
+mod bchks25_brute_force_params {
+    use crate::soundness::SoundnessCalculator;
+
+    const BCHKS25_DY_SEARCH_MIN_MAX: u128 = 9;
+    const BCHKS25_DY_SEARCH_REF_MULTIPLIER: u128 = 4;
+    const BCHKS25_DY_SEARCH_HARD_MAX: u128 = 4096;
+    const BCHKS25_DZ_SEARCH_MAX: u128 = 500_000;
+
+    #[derive(Clone, Copy, Debug)]
+    pub struct Bchks25Degrees {
+        pub d_x: u128,
+        pub d_y: u128,
+        // Integer index representation for Z-degree support:
+        // `j + h < D_Z` is represented as `0 <= h <= d_z - j`, so `d_z = ceil(D_Z) - 1`.
+        pub d_z: u128,
     }
 
-    #[test]
-    fn test_app_vm_security() {
-        let params = app_params();
-        let n_logup = n_logup_bound(
-            params.l_skip,
-            APP_NUM_AIRS,
-            APP_MAX_INTERACTIONS_PER_AIR,
-            APP_MAX_LOG_HEIGHT,
-            params.logup.max_interaction_count as usize,
-        );
-        let soundness = check_soundness(
-            "App VM",
-            &params,
-            APP_MAX_CONSTRAINTS,
-            APP_NUM_AIRS,
-            APP_MAX_LOG_HEIGHT,
-            APP_NUM_COLUMNS,
-            n_logup,
-        );
-        assert!(
-            soundness.total_bits >= TARGET_SECURITY_BITS as f64,
-            "App VM: got {:.1} bits",
-            soundness.total_bits
-        );
+    /// We find optimal parameters `D_X, D_Y, D_Z` that minimize Equation (13) in BCHKS25 **and**
+    /// satisfy the conditions necessary for the proof of Lemma 3.1 to carry through:
+    /// - `D_X >= k * D_Y`
+    /// - `D_Z >= D_Y`
+    /// - for `m < 3`, additionally `D_Z >=` Equation (9), i.e. `D_Z = max(D_Y, Equation (9) value)`
+    /// - `D_Y >= m - 1`
+    /// - `D_X <= (1 - gamma) * m * n` (Section 3.2 precondition before applying Equation (13))
+    /// - `n_vars > n_eqs` where `n_eqs` is given by Equation (11) and `n_vars = \sum_0^{ceil(D_Y) -
+    ///   1} (ceil(D_X) - kj)(ceil(D_Z) - j)`
+    /// ```text
+    /// n_{\mathrm{vars}}=\sum_{j=0}^{\lceil D_Y\rceil-1}(\lceil D_X\rceil-kj)(\lceil D_Z\rceil-j)
+    /// n_{\mathrm{eqs}}=n\sum_{s=0}^{m-1}(\lceil D_Z\rceil-s)(m-s)
+    /// ```
+    ///
+    /// Brute-force search for degrees minimizing Equation (13):
+    /// - scan `D_Y in [max(1, m - 1), D_Y_max]`
+    /// - `D_Y_max` is chosen from a scaled Lemma 3.1 reference degree (with a hard cap to keep
+    ///   computation bounded)
+    /// - scan candidate `D_X >= k * D_Y` up to the Section 3.2 limit
+    /// - solve directly for the smallest valid `D_Z` for each `(D_X, D_Y)`
+    pub fn bchks25_optimal_degrees_bruteforce(
+        log_degree: usize,
+        log_inv_rate: usize,
+        m: usize,
+        gamma: f64,
+    ) -> Option<(Bchks25Degrees, f64)> {
+        if !gamma.is_finite() || gamma <= 0.0 {
+            return None;
+        }
+
+        let log_n = log_degree.checked_add(log_inv_rate)?;
+        if log_n >= u128::BITS as usize || log_degree >= u128::BITS as usize {
+            return None;
+        }
+
+        let n = 1_u128.checked_shl(log_n as u32)?;
+        let k = 1_u128.checked_shl(log_degree as u32)?;
+        let m_u = m as u128;
+
+        let agreements_plus_one = (gamma * n as f64).ceil() + 1.0;
+        if !agreements_plus_one.is_finite() || agreements_plus_one <= 0.0 {
+            return None;
+        }
+        let log2_agreements_plus_one = agreements_plus_one.log2();
+        let max_d_x_for_gamma = (1.0 - gamma) * (m_u as f64) * (n as f64);
+        if !max_d_x_for_gamma.is_finite() || max_d_x_for_gamma <= 0.0 {
+            return None;
+        }
+
+        let mut best: Option<(Bchks25Degrees, f64)> = None;
+        let d_y_start = 1_u128.max(m_u.saturating_sub(1));
+        let d_y_end = bchks25_dy_search_upper_bound(log_degree, log_inv_rate, m);
+        let d_z_floor = if m < 3 {
+            bchks25_dz_eq9_index_lower_bound(log_inv_rate, m)?
+        } else {
+            0
+        };
+        if d_y_start > d_y_end {
+            return None;
+        }
+
+        for d_y in d_y_start..=d_y_end {
+            let Some(d_x_base) = k.checked_mul(d_y) else {
+                continue;
+            };
+            if (d_x_base as f64) >= max_d_x_for_gamma {
+                continue;
+            }
+
+            let d_x_upper = max_d_x_for_gamma.ceil() as u128;
+            let mut d_x_candidates = Vec::with_capacity(24);
+            d_x_candidates.push(d_x_base);
+            if let Some(v) = d_x_base.checked_add(1) {
+                d_x_candidates.push(v);
+            }
+
+            let d_y_plus_1 = d_y.checked_add(1)?;
+            let k_term = k
+                .checked_mul(d_y)?
+                .checked_mul(d_y_plus_1)?
+                .checked_div(2)?;
+            let a_e = n.checked_mul(m_u.checked_mul(m_u.checked_add(1)?)?.checked_div(2)?)?;
+            let d_x_slope_cross = a_e.checked_add(k_term)?.checked_div(d_y_plus_1)?;
+            for off in [0_u128, 1, 2] {
+                if d_x_slope_cross >= off {
+                    d_x_candidates.push(d_x_slope_cross - off);
+                }
+                if let Some(v) = d_x_slope_cross.checked_add(off) {
+                    d_x_candidates.push(v);
+                }
+            }
+
+            if d_x_upper > d_x_base {
+                let step = ((d_x_upper - d_x_base) / 16).max(1);
+                let mut cur = d_x_base;
+                while cur <= d_x_upper {
+                    d_x_candidates.push(cur);
+                    let Some(next) = cur.checked_add(step) else {
+                        break;
+                    };
+                    if next <= cur {
+                        break;
+                    }
+                    cur = next;
+                }
+                d_x_candidates.push(d_x_upper);
+                d_x_candidates.push(d_x_upper.saturating_sub(1));
+            }
+
+            d_x_candidates.sort_unstable();
+            d_x_candidates.dedup();
+
+            for d_x in d_x_candidates {
+                if d_x < d_x_base || (d_x as f64) >= max_d_x_for_gamma {
+                    continue;
+                }
+
+                let Some(d_z) = bchks25_min_dz_for_dx_dy(k, n, m_u, d_x, d_y, d_z_floor) else {
+                    continue;
+                };
+
+                let log2_d_x = (d_x as f64).log2();
+                let log2_d_y = (d_y as f64).log2();
+                let log2_d_z = (d_z as f64).log2();
+                let log2_a = SoundnessCalculator::bchks25_log2_a_from_log2_degrees(
+                    log2_d_x,
+                    log2_d_y,
+                    log2_d_z,
+                    log2_agreements_plus_one,
+                );
+                if !log2_a.is_finite() {
+                    continue;
+                }
+
+                let candidate = (Bchks25Degrees { d_x, d_y, d_z }, log2_a);
+                match best {
+                    None => best = Some(candidate),
+                    Some((best_deg, best_log2_a)) => {
+                        // Stable tie-breaking keeps smaller degrees if scores are effectively
+                        // equal.
+                        let better = log2_a + 1e-12 < best_log2_a
+                            || ((log2_a - best_log2_a).abs() <= 1e-12
+                                && (d_y < best_deg.d_y
+                                    || (d_y == best_deg.d_y
+                                        && (d_z < best_deg.d_z
+                                            || (d_z == best_deg.d_z && d_x < best_deg.d_x)))));
+                        if better {
+                            best = Some(candidate);
+                        }
+                    }
+                }
+            }
+        }
+        best
     }
 
-    #[test]
-    fn test_leaf_aggregation_security() {
-        let params = leaf_params();
-        let max_log_height = 20;
-        let n_logup = n_logup_bound(
-            params.l_skip,
-            RECURSION_NUM_AIRS,
-            RECURSION_MAX_INTERACTIONS_PER_AIR,
-            max_log_height,
-            params.logup.max_interaction_count as usize,
-        );
-        let soundness = check_soundness(
-            "Leaf Aggregation",
-            &params,
-            RECURSION_MAX_CONSTRAINTS,
-            RECURSION_NUM_AIRS,
-            max_log_height,
-            RECURSION_NUM_COLUMNS,
-            n_logup,
-        );
-        assert!(
-            soundness.total_bits >= TARGET_SECURITY_BITS as f64,
-            "Leaf: got {:.1} bits",
-            soundness.total_bits
-        );
+    fn bchks25_dy_search_upper_bound(log_degree: usize, log_inv_rate: usize, m: usize) -> u128 {
+        let (_log2_d_x, log2_d_y, _log2_d_z) =
+            SoundnessCalculator::bchks25_reference_log2_degrees(log_degree, log_inv_rate, m);
+        if !log2_d_y.is_finite() {
+            return BCHKS25_DY_SEARCH_HARD_MAX;
+        }
+        let ref_d_y = log2_d_y.exp2().ceil();
+        if !ref_d_y.is_finite() || ref_d_y <= 0.0 {
+            return BCHKS25_DY_SEARCH_HARD_MAX;
+        }
+        let ref_scaled = (ref_d_y as u128).saturating_mul(BCHKS25_DY_SEARCH_REF_MULTIPLIER);
+        ref_scaled.clamp(BCHKS25_DY_SEARCH_MIN_MAX, BCHKS25_DY_SEARCH_HARD_MAX)
     }
 
-    #[test]
-    fn test_internal_aggregation_security() {
-        let params = internal_params();
-        let max_log_height = 19;
-        let n_logup = n_logup_bound(
-            params.l_skip,
-            RECURSION_NUM_AIRS,
-            RECURSION_MAX_INTERACTIONS_PER_AIR,
-            max_log_height,
-            params.logup.max_interaction_count as usize,
-        );
-        let soundness = check_soundness(
-            "Internal Aggregation",
-            &params,
-            RECURSION_MAX_CONSTRAINTS,
-            RECURSION_NUM_AIRS,
-            max_log_height,
-            RECURSION_NUM_COLUMNS,
-            n_logup,
-        );
-        assert!(
-            soundness.total_bits >= TARGET_SECURITY_BITS as f64,
-            "Internal: got {:.1} bits",
-            soundness.total_bits
-        );
+    /// Index-space lower bound from Equation (9), where `d_z = ceil(D_Z)-1`.
+    fn bchks25_dz_eq9_index_lower_bound(log_inv_rate: usize, m: usize) -> Option<u128> {
+        let m_u = m.max(1) as u128;
+        if log_inv_rate >= u128::BITS as usize {
+            return None;
+        }
+
+        // Equation (9): D_Z = ((m + 1/2)^2 * (n/k)) / 3
+        // with n/k = 2^{log_inv_rate}. So:
+        // D_Z = ((2m+1)^2 * 2^{log_inv_rate}) / 12.
+        let n_over_k = 1_u128.checked_shl(log_inv_rate as u32)?;
+        let two_m_plus_1 = m_u.checked_mul(2)?.checked_add(1)?;
+        let numerator = two_m_plus_1
+            .checked_mul(two_m_plus_1)?
+            .checked_mul(n_over_k)?;
+        let ceil_d_z = numerator.checked_add(11)?.checked_div(12)?;
+        Some(ceil_d_z.saturating_sub(1))
     }
 
-    #[test]
-    fn test_compression_security() {
-        let params = compression_params();
-        let max_log_height = 22;
-        let n_logup = n_logup_bound(
-            params.l_skip,
-            RECURSION_NUM_AIRS,
-            RECURSION_MAX_INTERACTIONS_PER_AIR,
-            max_log_height,
-            params.logup.max_interaction_count as usize,
-        );
-        let soundness = check_soundness(
-            "Compression",
-            &params,
-            RECURSION_MAX_CONSTRAINTS,
-            RECURSION_NUM_AIRS,
-            max_log_height,
-            RECURSION_NUM_COLUMNS,
-            n_logup,
-        );
-        assert!(
-            soundness.total_bits >= TARGET_SECURITY_BITS as f64,
-            "Compression: got {:.1} bits",
-            soundness.total_bits
-        );
+    /// Counts interpolation variables for fixed `D_X, D_Y, D_Z`.
+    ///
+    /// Here `d_x`, `d_y` and `d_z` are index-space bounds
+    /// (`ceil(D_X)-1`, `ceil(D_Y)-1`, `ceil(D_Z)-1`), not real degrees.
+    /// This matches the lattice count used in Lemma 3.1:
+    /// `j + h < D_Z` contributes `(d_z - j + 1)` monomials in `Z`.
+    #[cfg(test)]
+    fn bchks25_num_vars(k: u128, d_x: u128, d_y: u128, d_z: u128) -> Option<u128> {
+        if d_z < d_y {
+            return Some(0);
+        }
+
+        let mut total = 0_u128;
+        for j in 0..=d_y {
+            let x_terms = d_x.checked_sub(k.checked_mul(j)?)?.checked_add(1)?;
+            let z_terms = (d_z - j).checked_add(1)?;
+            let add = x_terms.checked_mul(z_terms)?;
+            total = total.checked_add(add)?;
+        }
+        Some(total)
+    }
+
+    /// Equation (11) RHS (closed form):
+    /// `n_eqs = n * ( m(m+1)/2 * ceil(D_Z) - (m^3-m)/6 )`.
+    ///
+    /// We store `d_z = ceil(D_Z)-1` (index-space convention), therefore `ceil(D_Z)=d_z+1`.
+    #[cfg(test)]
+    fn bchks25_num_eqs_eq11(n: u128, m: u128, d_z: u128) -> Option<u128> {
+        let ceil_d_z = d_z.checked_add(1)?;
+        let m_plus_1 = m.checked_add(1)?;
+        let m_choose_2_scaled = m.checked_mul(m_plus_1)?.checked_div(2)?;
+        let m_cubic_minus_m_over_6 = m
+            .checked_mul(m)?
+            .checked_mul(m)?
+            .checked_sub(m)?
+            .checked_div(6)?;
+        let inner = m_choose_2_scaled
+            .checked_mul(ceil_d_z)?
+            .checked_sub(m_cubic_minus_m_over_6)?;
+        n.checked_mul(inner)
+    }
+
+    /// Solves for the minimal index-space `d_z` satisfying
+    /// `n_vars(d_z) > n_eqs(d_z)` (Equation (11)).
+    ///
+    /// Both sides are affine in `d_z`, so this is a 1D linear inequality with bounds
+    /// `d_z in [max(d_y, m-1), BCHKS25_DZ_SEARCH_MAX]` and does not require binary search.
+    ///
+    /// The returned value corresponds to real-degree parameter `D_Z` via `d_z = ceil(D_Z)-1`.
+    fn bchks25_min_dz_for_dx_dy(
+        k: u128,
+        n: u128,
+        m: u128,
+        d_x: u128,
+        d_y: u128,
+        d_z_floor: u128,
+    ) -> Option<u128> {
+        let low = d_y.max(m.saturating_sub(1)).max(d_z_floor);
+        let high = BCHKS25_DZ_SEARCH_MAX;
+        if low > high {
+            return None;
+        }
+
+        // n_vars(d_z) for fixed (d_x, d_y):
+        // n_vars = sum_{j=0}^{d_y} (d_x - k*j + 1) * (d_z - j + 1)
+        //        = A_v * (d_z + 1) - B_v
+        //
+        let d_y_plus_1 = d_y.checked_add(1)?;
+        let d_y_d_y_plus_1_over_2 = d_y.checked_mul(d_y_plus_1)?.checked_div(2)?;
+        let d_y_d_y_plus_1_two_d_y_plus_1_over_6 = d_y
+            .checked_mul(d_y)?
+            .checked_add(d_y)?
+            .checked_mul(d_y.checked_mul(2)?.checked_add(1)?)?
+            .checked_div(6)?;
+        let a_v = d_y_plus_1
+            .checked_mul(d_x.checked_add(1)?)?
+            .checked_sub(k.checked_mul(d_y_d_y_plus_1_over_2)?)?;
+        let b_v = d_x
+            .checked_add(1)?
+            .checked_mul(d_y_d_y_plus_1_over_2)?
+            .checked_sub(k.checked_mul(d_y_d_y_plus_1_two_d_y_plus_1_over_6)?)?;
+        if a_v == 0 {
+            return None;
+        }
+
+        // n_eqs(d_z) = A_e * (d_z + 1) - B_e from Equation (11) closed form.
+        let m_plus_1 = m.checked_add(1)?;
+        let a_e = n.checked_mul(m.checked_mul(m_plus_1)?.checked_div(2)?)?;
+        let b_e = n.checked_mul(
+            m.checked_mul(m)?
+                .checked_mul(m)?
+                .checked_sub(m)?
+                .checked_div(6)?,
+        )?;
+
+        let is_valid = |d_z: u128| -> Option<bool> {
+            let x = d_z.checked_add(1)?;
+            let n_vars = a_v.checked_mul(x)?.checked_sub(b_v)?;
+            let n_eqs = a_e.checked_mul(x)?.checked_sub(b_e)?;
+            Some(n_vars > n_eqs)
+        };
+
+        match a_v.cmp(&a_e) {
+            core::cmp::Ordering::Greater => {
+                // Increasing predicate: solve exactly, then clamp to bounds.
+                let slope = a_v.checked_sub(a_e)?;
+                let candidate = if b_v < b_e {
+                    low
+                } else {
+                    let rhs = b_v.checked_sub(b_e)?;
+                    let x_min = rhs.checked_div(slope)?.checked_add(1)?;
+                    let d_min = x_min.checked_sub(1)?;
+                    low.max(d_min)
+                };
+                if candidate > high {
+                    return None;
+                }
+                if is_valid(candidate)? {
+                    Some(candidate)
+                } else {
+                    None
+                }
+            }
+            core::cmp::Ordering::Equal => {
+                if b_v < b_e {
+                    Some(low)
+                } else {
+                    None
+                }
+            }
+            core::cmp::Ordering::Less => {
+                // Decreasing predicate: if low is not valid, no later value can be valid.
+                if is_valid(low)? {
+                    Some(low)
+                } else {
+                    None
+                }
+            }
+        }
     }
 
     #[test]
-    fn test_all_production_configs() {
-        println!("\n========== ALL PRODUCTION CONFIGS ==========");
+    fn test_bchks25_optimizer_finds_minimal_valid_dz() {
+        let log_degree = 14;
+        let log_inv_rate = 5;
+        let m = 1;
+
+        let rho = (-(log_inv_rate as f64)).exp2();
+        let sqrt_rho = rho.sqrt();
+        let eta = sqrt_rho / (2.0 * m as f64);
+        let gamma = 1.0 - sqrt_rho - eta;
+
+        let (degrees, _log2_a) =
+            bchks25_optimal_degrees_bruteforce(log_degree, log_inv_rate, m, gamma)
+                .expect("optimizer should find valid degrees");
+        let n = 1_u128 << (log_degree + log_inv_rate);
+        let k = 1_u128 << log_degree;
+        let m_u = m as u128;
+
+        assert!(degrees.d_y >= m_u.saturating_sub(1));
+        let max_d_x_for_gamma = (1.0 - gamma) * (m as f64) * (n as f64);
+        assert!(degrees.d_x >= k * degrees.d_y);
+        assert!((degrees.d_x as f64) < max_d_x_for_gamma);
+        let d_z_floor = bchks25_dz_eq9_index_lower_bound(log_inv_rate, m)
+            .expect("d_z floor should be representable");
+        assert!(degrees.d_z >= degrees.d_y.max(d_z_floor));
+        let vars = bchks25_num_vars(k, degrees.d_x, degrees.d_y, degrees.d_z)
+            .expect("vars should fit in u128");
+        let eqs = bchks25_num_eqs_eq11(n, m_u, degrees.d_z).expect("eqs should fit in u128");
+        assert!(vars > eqs);
+        let low = degrees.d_y.max(m_u.saturating_sub(1)).max(d_z_floor);
+        if degrees.d_z > low {
+            let prev_vars = bchks25_num_vars(k, degrees.d_x, degrees.d_y, degrees.d_z - 1)
+                .expect("vars should fit in u128");
+            let prev_eqs =
+                bchks25_num_eqs_eq11(n, m_u, degrees.d_z - 1).expect("eqs should fit in u128");
+            assert!(prev_vars <= prev_eqs);
+        }
+    }
 
-        let app = app_params();
-        let leaf = leaf_params();
-        let internal = internal_params();
-        let compression = compression_params();
+    #[test]
+    fn test_bchks25_eq11_closed_form_matches_expanded_sum() {
+        let n = 1_u128 << 12;
+        for m in 2_u128..=8 {
+            for d_z in (m - 1)..=(m + 12) {
+                let closed_form =
+                    bchks25_num_eqs_eq11(n, m, d_z).expect("closed-form n_eqs should fit in u128");
+                let ceil_d_z = d_z + 1;
+                let mut expanded_sum = 0_u128;
+                for s in 0..m {
+                    expanded_sum += (ceil_d_z - s) * (m - s);
+                }
+                let expanded = n * expanded_sum;
+                assert_eq!(closed_form, expanded);
+            }
+        }
+    }
 
-        // (name, params, max_constraints, num_airs, max_log_height, num_columns,
-        // max_interactions_per_air)
-        let configs: [(&str, &SystemParams, usize, usize, usize, usize, usize); 4] = [
+    #[test]
+    fn test_bchks25_min_dz_direct_solve_matches_linear_scan() {
+        let cases = [
+            // Increasing predicate case.
             (
-                "App VM",
-                &app,
-                APP_MAX_CONSTRAINTS,
-                APP_NUM_AIRS,
-                APP_MAX_LOG_HEIGHT,
-                APP_NUM_COLUMNS,
-                APP_MAX_INTERACTIONS_PER_AIR,
+                1_u128 << 20,
+                1_u128 << 22,
+                3_u128,
+                2_u128,
+                (1_u128 << 20) * 2,
             ),
+            // Decreasing predicate case.
             (
-                "Leaf",
-                &leaf,
-                RECURSION_MAX_CONSTRAINTS,
-                RECURSION_NUM_AIRS,
-                20,
-                RECURSION_NUM_COLUMNS,
-                RECURSION_MAX_INTERACTIONS_PER_AIR,
+                1_u128 << 12,
+                1_u128 << 24,
+                6_u128,
+                5_u128,
+                (1_u128 << 12) * 5,
             ),
+            // Near-flat-ish case.
             (
-                "Internal",
-                &internal,
-                RECURSION_MAX_CONSTRAINTS,
-                RECURSION_NUM_AIRS,
-                19,
-                RECURSION_NUM_COLUMNS,
-                RECURSION_MAX_INTERACTIONS_PER_AIR,
+                1_u128 << 16,
+                1_u128 << 20,
+                4_u128,
+                3_u128,
+                (1_u128 << 16) * 3 + 1,
             ),
+            // m < 3 with Equation (9) lower bound active.
             (
-                "Compression",
-                &compression,
-                RECURSION_MAX_CONSTRAINTS,
-                RECURSION_NUM_AIRS,
-                22,
-                RECURSION_NUM_COLUMNS,
-                RECURSION_MAX_INTERACTIONS_PER_AIR,
+                1_u128 << 12,
+                1_u128 << 17,
+                1_u128,
+                2_u128,
+                (1_u128 << 12) * 2 + 17,
             ),
         ];
 
-        for (
-            name,
-            params,
-            max_constraints,
-            num_airs,
-            max_log_height,
-            num_columns,
-            max_interactions,
-        ) in configs
-        {
-            let n_logup = n_logup_bound(
-                params.l_skip,
-                num_airs,
-                max_interactions,
-                max_log_height,
-                params.logup.max_interaction_count as usize,
-            );
-            let soundness = check_soundness(
-                name,
-                params,
-                max_constraints,
-                num_airs,
-                max_log_height,
-                num_columns,
-                n_logup,
-            );
-            assert!(
-                soundness.total_bits >= TARGET_SECURITY_BITS as f64,
-                "{}: got {:.1} bits",
-                name,
-                soundness.total_bits
-            );
+        for (k, n, m, d_y, d_x) in cases {
+            assert!(d_x >= k * d_y);
+            let log_inv_rate = (n / k).ilog2() as usize;
+            let d_z_floor = if m < 3 {
+                bchks25_dz_eq9_index_lower_bound(log_inv_rate, m as usize)
+                    .expect("d_z floor should be representable")
+            } else {
+                0
+            };
+            let got = bchks25_min_dz_for_dx_dy(k, n, m, d_x, d_y, d_z_floor);
+            let low = d_y.max(m.saturating_sub(1)).max(d_z_floor);
+            let expected = (low..=BCHKS25_DZ_SEARCH_MAX).find(|&d_z| {
+                let vars = bchks25_num_vars(k, d_x, d_y, d_z).expect("vars should fit");
+                let eqs = bchks25_num_eqs_eq11(n, m, d_z).expect("eqs should fit");
+                vars > eqs
+            });
+            assert_eq!(got, expected);
         }
-
-        println!("\n========== ALL CONFIGS PASSED ==========");
     }
 }
diff --git a/crates/stark-backend/src/test_utils/mod.rs b/crates/stark-backend/src/test_utils/mod.rs
index 0e0ae716..1d0ddd3c 100644
--- a/crates/stark-backend/src/test_utils/mod.rs
+++ b/crates/stark-backend/src/test_utils/mod.rs
@@ -23,6 +23,7 @@ use crate::{
         MultiRapProver, Prover, ProvingContext, TraceCommitter,
     },
     AirRef, StarkEngine, StarkProtocolConfig, SystemParams, WhirConfig, WhirParams,
+    WhirProximityStrategy,
 };
 
 pub mod dummy_airs;
@@ -566,6 +567,12 @@ pub fn test_whir_config_small(
         k: k_whir,
         log_final_poly_len,
         query_phase_pow_bits: 1,
+        folding_pow_bits: 2,
+        mu_pow_bits: 3,
+        proximity: WhirProximityStrategy::SplitUniqueList {
+            m: 3,
+            list_start_round: 1,
+        },
     };
     let security_bits = 5;
     WhirConfig::new(log_blowup, log_stacked_height, params, security_bits)
diff --git a/crates/stark-backend/tests/soundness.rs b/crates/stark-backend/tests/soundness.rs
new file mode 100644
index 00000000..00fe89b7
--- /dev/null
+++ b/crates/stark-backend/tests/soundness.rs
@@ -0,0 +1,336 @@
+//! ==========================================================================
+//! Production configuration soundness tests
+//! ==========================================================================
+
+use openvm_stark_backend::{soundness::*, SystemParams};
+use openvm_stark_sdk::config::{
+    app_params_with_100_bits_security,
+    compression_params_with_100_bits_security as compression_params,
+    internal_params_with_100_bits_security as internal_params,
+    leaf_params_with_100_bits_security as leaf_params, MAX_APP_LOG_STACKED_HEIGHT,
+};
+use p3_baby_bear::BabyBear;
+use p3_field::PrimeField64;
+
+// ==========================================================================
+// Circuit parameter upper bounds for soundness analysis
+//
+// These are conservative estimates based on actual production values.
+// Stacking can only reduce width, so num_columns is an upper bound on stacked columns.
+// ==========================================================================
+
+/// Upper bound on n_logup derived from circuit parameters.
+///
+/// n_logup = ceil_log2(total_interactions) - l_skip, where:
+/// - total_interactions ≤ num_airs × max_interactions_per_air × 2^max_log_height
+/// - total_interactions < max_interaction_count (enforced by verifier as one of the
+///   `LinearConstraint`s, keygen ensures this linear constraint is included)
+///
+/// So: n_logup ≤ min(ceil_log2(max_interaction_count) - l_skip, log2(num_airs ×
+/// max_interactions) + max_log_height - l_skip)
+fn n_logup_bound(
+    l_skip: usize,
+    num_airs: usize,
+    max_interactions_per_air: usize,
+    max_log_height: usize,
+    max_interaction_count: usize,
+) -> usize {
+    let field_bound = (max_interaction_count as f64).log2().ceil() as usize - l_skip;
+    let param_bound = (num_airs as f64).log2().ceil() as usize
+        + (max_interactions_per_air as f64).log2().ceil() as usize
+        + max_log_height
+        - l_skip;
+    field_bound.min(param_bound)
+}
+
+// App VM: large circuits with many AIRs
+// Actual: max_constraints=4513 (keccak), num_airs=73, max_interactions=832
+const APP_MAX_CONSTRAINTS: usize = 5000;
+const APP_NUM_AIRS: usize = 100;
+const APP_MAX_LOG_HEIGHT: usize = 24;
+const APP_NUM_COLUMNS: usize = 30000;
+const APP_MAX_INTERACTIONS_PER_AIR: usize = 1000;
+
+// Recursion circuits: smaller, fixed structure
+// Actual: num_airs=42
+const RECURSION_MAX_CONSTRAINTS: usize = 1000;
+const RECURSION_NUM_AIRS: usize = 50;
+const RECURSION_NUM_COLUMNS: usize = 2000;
+const RECURSION_MAX_INTERACTIONS_PER_AIR: usize = 100; // estimate, needs verification
+
+const TARGET_SECURITY_BITS: usize = 100;
+
+fn babybear_quartic_extension_bits() -> f64 {
+    4.0 * (BabyBear::ORDER_U64 as f64).log2()
+}
+
+fn app_params() -> SystemParams {
+    app_params_with_100_bits_security(MAX_APP_LOG_STACKED_HEIGHT)
+}
+
+fn check_soundness(
+    name: &str,
+    params: &SystemParams,
+    max_constraints: usize,
+    num_airs: usize,
+    max_log_height: usize,
+    num_columns: usize,
+    n_logup: usize,
+) -> SoundnessCalculator {
+    let soundness = SoundnessCalculator::calculate(
+        params,
+        babybear_quartic_extension_bits(),
+        max_constraints,
+        num_airs,
+        params.max_constraint_degree,
+        max_log_height,
+        num_columns,
+        params.w_stack,
+        n_logup,
+    );
+
+    println!("\n=== {} Soundness ===", name);
+    println!(
+        "Config: l_skip={}, n_stack={}, w_stack={}, log_blowup={}, k_whir={}, whir.rounds={:?}",
+        params.l_skip,
+        params.n_stack,
+        params.w_stack,
+        params.log_blowup,
+        params.whir.k,
+        params.whir.rounds
+    );
+    println!(
+        "Context: max_constraints={}, num_airs={}, max_log_height={}, num_columns={}, n_logup={}",
+        max_constraints, num_airs, max_log_height, num_columns, n_logup
+    );
+    println!();
+    println!("LogUp (α/β + PoW):   {:.1} bits", soundness.logup_bits);
+    println!(
+        "GKR sumcheck:        {:.1} bits",
+        soundness.gkr_sumcheck_bits
+    );
+    println!(
+        "GKR batching (μ/λ):  {:.1} bits",
+        soundness.gkr_batching_bits
+    );
+    println!(
+        "ZeroCheck sumcheck:  {:.1} bits",
+        soundness.zerocheck_sumcheck_bits
+    );
+    println!(
+        "Constraint batching: {:.1} bits",
+        soundness.constraint_batching_bits
+    );
+    println!(
+        "Stacked reduction:   {:.1} bits",
+        soundness.stacked_reduction_bits
+    );
+    println!("WHIR:                {:.1} bits", soundness.whir_bits);
+    println!("TOTAL:               {:.1} bits", soundness.total_bits);
+
+    println!("\nWHIR Error Source Breakdown:");
+    let whir = &soundness.whir_details;
+    println!("  Query error:          {:.1} bits", whir.query_bits);
+    println!(
+        "  Proximity gaps:       {:.1} bits",
+        whir.proximity_gaps_bits
+    );
+    println!("  Sumcheck error:       {:.1} bits", whir.sumcheck_bits);
+    println!("  Min ε_fold:           {:.1} bits", whir.fold_rbr_bits);
+    println!("  OOD error:            {:.1} bits", whir.ood_rbr_bits);
+    println!(
+        "  γ batching error:     {:.1} bits",
+        whir.gamma_batching_bits
+    );
+    println!("  Min ε_shift/ε_fin:    {:.1} bits", whir.shift_rbr_bits);
+    println!("  μ batching error:     {:.1} bits", whir.mu_batching_bits);
+
+    soundness
+}
+
+#[test]
+fn test_app_vm_security() {
+    let params = app_params();
+    let n_logup = n_logup_bound(
+        params.l_skip,
+        APP_NUM_AIRS,
+        APP_MAX_INTERACTIONS_PER_AIR,
+        APP_MAX_LOG_HEIGHT,
+        params.logup.max_interaction_count as usize,
+    );
+    let soundness = check_soundness(
+        "App VM",
+        &params,
+        APP_MAX_CONSTRAINTS,
+        APP_NUM_AIRS,
+        APP_MAX_LOG_HEIGHT,
+        APP_NUM_COLUMNS,
+        n_logup,
+    );
+    assert!(
+        soundness.total_bits >= TARGET_SECURITY_BITS as f64,
+        "App VM: got {:.1} bits",
+        soundness.total_bits
+    );
+}
+
+#[test]
+fn test_leaf_aggregation_security() {
+    let params = leaf_params();
+    let max_log_height = 20;
+    let n_logup = n_logup_bound(
+        params.l_skip,
+        RECURSION_NUM_AIRS,
+        RECURSION_MAX_INTERACTIONS_PER_AIR,
+        max_log_height,
+        params.logup.max_interaction_count as usize,
+    );
+    let soundness = check_soundness(
+        "Leaf Aggregation",
+        &params,
+        RECURSION_MAX_CONSTRAINTS,
+        RECURSION_NUM_AIRS,
+        max_log_height,
+        RECURSION_NUM_COLUMNS,
+        n_logup,
+    );
+    assert!(
+        soundness.total_bits >= TARGET_SECURITY_BITS as f64,
+        "Leaf: got {:.1} bits",
+        soundness.total_bits
+    );
+}
+
+#[test]
+fn test_internal_aggregation_security() {
+    let params = internal_params();
+    let max_log_height = 19;
+    let n_logup = n_logup_bound(
+        params.l_skip,
+        RECURSION_NUM_AIRS,
+        RECURSION_MAX_INTERACTIONS_PER_AIR,
+        max_log_height,
+        params.logup.max_interaction_count as usize,
+    );
+    let soundness = check_soundness(
+        "Internal Aggregation",
+        &params,
+        RECURSION_MAX_CONSTRAINTS,
+        RECURSION_NUM_AIRS,
+        max_log_height,
+        RECURSION_NUM_COLUMNS,
+        n_logup,
+    );
+    assert!(
+        soundness.total_bits >= TARGET_SECURITY_BITS as f64,
+        "Internal: got {:.1} bits",
+        soundness.total_bits
+    );
+}
+
+#[test]
+fn test_compression_security() {
+    let params = compression_params();
+    let max_log_height = 22;
+    let n_logup = n_logup_bound(
+        params.l_skip,
+        RECURSION_NUM_AIRS,
+        RECURSION_MAX_INTERACTIONS_PER_AIR,
+        max_log_height,
+        params.logup.max_interaction_count as usize,
+    );
+    let soundness = check_soundness(
+        "Compression",
+        &params,
+        RECURSION_MAX_CONSTRAINTS,
+        RECURSION_NUM_AIRS,
+        max_log_height,
+        RECURSION_NUM_COLUMNS,
+        n_logup,
+    );
+    assert!(
+        soundness.total_bits >= TARGET_SECURITY_BITS as f64,
+        "Compression: got {:.1} bits",
+        soundness.total_bits
+    );
+}
+
+#[test]
+fn test_all_production_configs() {
+    println!("\n========== ALL PRODUCTION CONFIGS ==========");
+
+    let app = app_params();
+    let leaf = leaf_params();
+    let internal = internal_params();
+    let compression = compression_params();
+
+    // (name, params, max_constraints, num_airs, max_log_height, num_columns,
+    // max_interactions_per_air)
+    let configs: [(&str, &SystemParams, usize, usize, usize, usize, usize); 4] = [
+        (
+            "App VM",
+            &app,
+            APP_MAX_CONSTRAINTS,
+            APP_NUM_AIRS,
+            APP_MAX_LOG_HEIGHT,
+            APP_NUM_COLUMNS,
+            APP_MAX_INTERACTIONS_PER_AIR,
+        ),
+        (
+            "Leaf",
+            &leaf,
+            RECURSION_MAX_CONSTRAINTS,
+            RECURSION_NUM_AIRS,
+            20,
+            RECURSION_NUM_COLUMNS,
+            RECURSION_MAX_INTERACTIONS_PER_AIR,
+        ),
+        (
+            "Internal",
+            &internal,
+            RECURSION_MAX_CONSTRAINTS,
+            RECURSION_NUM_AIRS,
+            19,
+            RECURSION_NUM_COLUMNS,
+            RECURSION_MAX_INTERACTIONS_PER_AIR,
+        ),
+        (
+            "Compression",
+            &compression,
+            RECURSION_MAX_CONSTRAINTS,
+            RECURSION_NUM_AIRS,
+            22,
+            RECURSION_NUM_COLUMNS,
+            RECURSION_MAX_INTERACTIONS_PER_AIR,
+        ),
+    ];
+
+    for (name, params, max_constraints, num_airs, max_log_height, num_columns, max_interactions) in
+        configs
+    {
+        let n_logup = n_logup_bound(
+            params.l_skip,
+            num_airs,
+            max_interactions,
+            max_log_height,
+            params.logup.max_interaction_count as usize,
+        );
+        let soundness = check_soundness(
+            name,
+            params,
+            max_constraints,
+            num_airs,
+            max_log_height,
+            num_columns,
+            n_logup,
+        );
+        assert!(
+            soundness.total_bits >= TARGET_SECURITY_BITS as f64,
+            "{}: got {:.1} bits",
+            name,
+            soundness.total_bits
+        );
+    }
+
+    println!("\n========== ALL CONFIGS PASSED ==========");
+}
diff --git a/crates/stark-sdk/examples/keccakf.rs b/crates/stark-sdk/examples/keccakf.rs
index 9d437cf1..ad32524d 100644
--- a/crates/stark-sdk/examples/keccakf.rs
+++ b/crates/stark-sdk/examples/keccakf.rs
@@ -5,12 +5,12 @@ use std::sync::Arc;
 use cfg_if::cfg_if;
 use eyre::eyre;
 use openvm_stark_sdk::{
-    config::log_up_params::log_up_security_params_baby_bear_100_bits,
+    config::app_params_with_100_bits_security,
     openvm_stark_backend::{
         p3_air::{Air, AirBuilder, BaseAir, BaseAirWithPublicValues},
         p3_field::Field,
         prover::{AirProvingContext, ColMajorMatrix, DeviceDataTransporter, ProvingContext},
-        PartitionedBaseAir, StarkEngine, SystemParams, WhirConfig, WhirParams,
+        PartitionedBaseAir, StarkEngine,
     },
 };
 use p3_keccak_air::KeccakAir;
@@ -44,27 +44,7 @@ impl<AB: AirBuilder> Air<AB> for TestAir {
 }
 
 fn main() -> eyre::Result<()> {
-    let l_skip = 4;
-    let n_stack = 17;
-    let w_stack = 64;
-    let k_whir = 4;
-    let whir_params = WhirParams {
-        k: k_whir,
-        log_final_poly_len: 2 * k_whir,
-        query_phase_pow_bits: 20,
-    };
-    let log_blowup = 1;
-    let whir = WhirConfig::new(log_blowup, l_skip + n_stack, whir_params, 100);
-    let params = SystemParams {
-        l_skip,
-        n_stack,
-        w_stack,
-        log_blowup,
-        whir,
-        logup: log_up_security_params_baby_bear_100_bits(),
-        max_constraint_degree: 3,
-    };
-
+    let params = app_params_with_100_bits_security(21);
     let mut rng = StdRng::seed_from_u64(42);
     let air = TestAir(KeccakAir {});
 
diff --git a/crates/stark-sdk/src/config/mod.rs b/crates/stark-sdk/src/config/mod.rs
index 6ac37ed3..4794beea 100644
--- a/crates/stark-sdk/src/config/mod.rs
+++ b/crates/stark-sdk/src/config/mod.rs
@@ -1,3 +1,7 @@
+use openvm_stark_backend::{SystemParams, WhirProximityStrategy};
+
+use crate::config::log_up_params::log_up_security_params_baby_bear_100_bits;
+
 /// STARK config where the base field is BabyBear, extension field is BabyBear^4, and the hasher is
 /// `Poseidon2<Bn254>`.
 #[cfg(feature = "baby-bear-bn254-poseidon2")]
@@ -6,3 +10,156 @@ pub mod baby_bear_bn254_poseidon2;
 /// `Poseidon2<BabyBear>`.
 pub mod baby_bear_poseidon2;
 pub mod log_up_params;
+
+// ==========================================================================
+// Production configurations
+// ==========================================================================
+// These configurations target 100-bits of proven round-by-round (RBR) security with BabyBear as the
+// base field and BabyBear^4 as the extension field.
+
+const WHIR_MAX_LOG_FINAL_POLY_LEN: usize = 10;
+const SECURITY_BITS_TARGET: usize = 100;
+
+pub const DEFAULT_APP_L_SKIP: usize = 4;
+pub const DEFAULT_APP_LOG_BLOWUP: usize = 1;
+pub const DEFAULT_LEAF_LOG_BLOWUP: usize = 2;
+pub const DEFAULT_INTERNAL_LOG_BLOWUP: usize = 3;
+pub const DEFAULT_ROOT_LOG_BLOWUP: usize = 3;
+pub const DEFAULT_COMPRESSION_LOG_BLOWUP: usize = 4;
+
+pub const MAX_APP_LOG_STACKED_HEIGHT: usize = 24;
+
+/// Returns `SystemParams` targeting 100 bits of proven RBR security for App VM circuits.
+///
+/// # Assumptions for 100-bit security
+/// - **Max trace height**: `log_stacked_height` ≤ [`MAX_APP_LOG_STACKED_HEIGHT`] (24)
+/// - **Max constraints per AIR**: ≤ 5,000
+/// - **Num AIRs**: ≤ 100
+/// - **Max interactions per AIR**: ≤ 1,000
+/// - **Num trace columns** (unstacked, total across all AIRs): ≤ 30,000
+/// - **`w_stack`** = 2,048, bounding total stacked cells to `w_stack × 2^(n_stack + l_skip)`
+//
+// See `test_all_production_configs` in `crates/stark-backend/tests/soundness.rs` for the
+// full soundness analysis.
+pub fn app_params_with_100_bits_security(log_stacked_height: usize) -> SystemParams {
+    assert!(
+        log_stacked_height <= MAX_APP_LOG_STACKED_HEIGHT,
+        "log_stacked_height must be <= {MAX_APP_LOG_STACKED_HEIGHT}",
+    );
+    SystemParams::new(
+        DEFAULT_APP_LOG_BLOWUP,
+        DEFAULT_APP_L_SKIP,
+        log_stacked_height.saturating_sub(DEFAULT_APP_L_SKIP), // n_stack
+        2048,                                                  // w_stack
+        WHIR_MAX_LOG_FINAL_POLY_LEN,
+        5,  // folding pow
+        15, // mu pow
+        WhirProximityStrategy::UniqueDecoding,
+        SECURITY_BITS_TARGET,
+        log_up_security_params_baby_bear_100_bits(),
+    )
+}
+
+/// Returns `SystemParams` targeting 100 bits of proven RBR security for leaf aggregation circuits.
+///
+/// # Assumptions for 100-bit security
+/// - **Max trace height**: ≤ 2^21
+/// - **Max constraints per AIR**: ≤ 1,000
+/// - **Num AIRs**: ≤ 50
+/// - **Max interactions per AIR**: ≤ 100 (maximum number of interactions in a single AIR for a
+///   single row)
+/// - **Num trace columns** (unstacked, total across all AIRs): ≤ 2,000
+/// - **`w_stack`** = 2,048, bounding total stacked cells to `w_stack × 2^(n_stack + l_skip)`
+///
+/// Config: `l_skip=4, n_stack=17, log_blowup=2`.
+//
+// See `test_all_production_configs` in `crates/stark-backend/tests/soundness.rs` for the
+// full soundness analysis.
+pub fn leaf_params_with_100_bits_security() -> SystemParams {
+    SystemParams::new(
+        DEFAULT_LEAF_LOG_BLOWUP,
+        4,    // l_skip
+        17,   // n_stack
+        2048, // w_stack
+        WHIR_MAX_LOG_FINAL_POLY_LEN,
+        4,  // folding pow
+        13, // mu pow
+        WhirProximityStrategy::UniqueDecoding,
+        SECURITY_BITS_TARGET,
+        log_up_security_params_baby_bear_100_bits(),
+    )
+}
+
+/// Returns `SystemParams` targeting 100 bits of proven RBR security for internal aggregation
+/// circuits.
+///
+/// # Assumptions for 100-bit security
+/// - **Max trace height**: ≤ 2^19
+/// - **Max constraints per AIR**: ≤ 1,000
+/// - **Num AIRs**: ≤ 50
+/// - **Max interactions per AIR**: ≤ 100
+/// - **Num trace columns** (unstacked, total across all AIRs): ≤ 2,000
+/// - **`w_stack`** = 512, bounding total stacked cells to `w_stack × 2^(n_stack + l_skip)`
+///
+/// Config: `l_skip=2, n_stack=17, log_blowup=2`.
+//
+// See `test_all_production_configs` in `crates/stark-backend/tests/soundness.rs` for the
+// full soundness analysis.
+pub fn internal_params_with_100_bits_security() -> SystemParams {
+    SystemParams::new(
+        DEFAULT_INTERNAL_LOG_BLOWUP,
+        2,   // l_skip
+        17,  // n_stack
+        512, // w_stack
+        WHIR_MAX_LOG_FINAL_POLY_LEN,
+        18, // folding pow
+        20, // mu pow
+        WhirProximityStrategy::ListDecoding { m: 2 },
+        SECURITY_BITS_TARGET,
+        log_up_security_params_baby_bear_100_bits(),
+    )
+}
+
+pub fn root_params_with_100_bits_security() -> SystemParams {
+    SystemParams::new(
+        DEFAULT_ROOT_LOG_BLOWUP,
+        2,  // l_skip
+        17, // n_stack
+        64, // w_stack
+        WHIR_MAX_LOG_FINAL_POLY_LEN,
+        18, // folding pow
+        20, // mu pow
+        WhirProximityStrategy::ListDecoding { m: 2 },
+        SECURITY_BITS_TARGET,
+        log_up_security_params_baby_bear_100_bits(),
+    )
+}
+
+/// Returns `SystemParams` targeting 100 bits of proven RBR security for the compression circuit.
+///
+/// # Assumptions for 100-bit security
+/// - **Max trace height**: ≤ 2^22
+/// - **Max constraints per AIR**: ≤ 1,000
+/// - **Num AIRs**: ≤ 50
+/// - **Max interactions per AIR**: ≤ 100
+/// - **Num trace columns** (unstacked, total across all AIRs): ≤ 2,000
+/// - **`w_stack`** = 16, bounding total stacked cells to `w_stack × 2^(n_stack + l_skip)`
+///
+/// Config: `l_skip=2, n_stack=20, log_blowup=4, log_final_poly_len=11`.
+//
+// See `test_all_production_configs` in `crates/stark-backend/tests/soundness.rs` for the
+// full soundness analysis.
+pub fn compression_params_with_100_bits_security() -> SystemParams {
+    SystemParams::new(
+        DEFAULT_COMPRESSION_LOG_BLOWUP,
+        2,
+        20, // n_stack
+        16, // w_stack
+        11, // log_final_poly_len
+        20, // folding pow
+        20, // mu pow
+        WhirProximityStrategy::ListDecoding { m: 1 },
+        SECURITY_BITS_TARGET,
+        log_up_security_params_baby_bear_100_bits(),
+    )
+}