diff --git a/air/src/proof/mod.rs b/air/src/proof/mod.rs
index 8936857d0..9b28bf4aa 100644
--- a/air/src/proof/mod.rs
+++ b/air/src/proof/mod.rs
@@ -33,6 +33,9 @@ pub use table::Table;
 
 const GRINDING_CONTRIBUTION_FLOOR: u32 = 80;
 
+#[cfg(feature = "std")]
+const MAX_PROXIMITY_PARAMETER: u64 = 1000;
+
 // STARK PROOF
 // ================================================================================================
 /// A proof generated by Winterfell prover.
@@ -204,8 +207,8 @@ fn get_conjectured_security(
     cmp::min(cmp::min(field_security, query_security) - 1, collision_resistance)
 }
 
-#[cfg(feature = "std")]
 /// Estimates proven security level for the specified proof parameters.
+#[cfg(feature = "std")]
 fn get_proven_security(
     options: &ProofOptions,
     base_field_bits: u32,
@@ -213,49 +216,120 @@ fn get_proven_security(
     trace_domain_size: u64,
     collision_resistance: u32,
 ) -> u32 {
-    let extension_field_bits = (base_field_bits * options.field_extension().degree()) as f64;
+    let m_min: usize = 3;
+    let m_max = compute_upper_m(trace_domain_size);
+
+    let m_optimal = (m_min as u32..m_max as u32)
+        .max_by_key(|&a| {
+            proven_security_protocol_for_m(
+                options,
+                base_field_bits,
+                lde_domain_size,
+                trace_domain_size,
+                a as usize,
+            )
+        })
+        .expect(
+            "Should not fail since m_max is larger than m_min for all trace sizes of length greater than 4",
+        );
+
+    cmp::min(
+        proven_security_protocol_for_m(
+            options,
+            base_field_bits,
+            lde_domain_size,
+            trace_domain_size,
+            m_optimal as usize,
+        ),
+        collision_resistance as u64,
+    ) as u32
+}
 
-    let blowup_bits = options.blowup_factor().ilog2() as f64;
+/// Computes proven security level for the specified proof parameters for a fixed
+/// value of the proximity parameter m in the list-decoding regime.
+#[cfg(feature = "std")]
+fn proven_security_protocol_for_m(
+    options: &ProofOptions,
+    base_field_bits: u32,
+    lde_domain_size: u64,
+    trace_domain_size: u64,
+    m: usize,
+) -> u64 {
+    let extension_field_bits = (base_field_bits * options.field_extension().degree()) as f64;
     let num_fri_queries = options.num_queries() as f64;
-    let lde_size_bits = lde_domain_size.trailing_zeros() as f64;
-
-    // blowup_plus_bits is the number of bits in the blowup factor which is the inverse of
-    // `\rho^+ := (trace_domain_size + 2) / lde_domain_size`. `\rho^+` is used in order to define a larger
-    // agreement parameter `\alpha^+ := (1 + 1/2m)\sqrt{rho^+} := 1 - \theta^+`. The reason for
-    // running FRI with a larger agreement parameter is to account for the simplified
-    // DEEP composition polynomial. See Protocol 3 in https://eprint.iacr.org/2022/1216.
-    let blowup_plus_bits = ((lde_domain_size as f64) / (trace_domain_size as f64 + 2_f64)).log2();
-
-    // m is a parameter greater or equal to 3.
-    // A larger m gives a worse field security bound but a better query security bound.
-    // An optimal value of m is then a value that would balance field and query security
-    // but there is no simple closed form solution.
-    // This sets m so that field security is equal to the best query security for any value
-    // of m, unless the calculated value is less than 3 in which case it gets rounded up to 3.
-    let mut m = extension_field_bits + 1.0;
-    m -= options.grinding_factor() as f64;
-    m -= 1.5 * blowup_bits;
-    m -= 0.5 * num_fri_queries * blowup_plus_bits;
-    m -= 2.0 * lde_size_bits;
-    m /= 7.0;
-    m = 2.0_f64.powf(m);
-    m -= 0.5;
-    m = m.max(3.0);
-
-    // compute pre-FRI query security
-    // this considers only the third component given in the corresponding part of eq. 20
-    // in https://eprint.iacr.org/2021/582, i.e. (m+1/2)^7.n^2 / (2\rho^1.5.q) as all
-    // other terms are negligible in comparison.
-    let pre_query_security = (extension_field_bits + 1.0
-        - 3.0 / 2.0 * blowup_bits
-        - 2.0 * lde_size_bits
-        - 7.0 * (m + 0.5).log2()) as u32;
-
-    // compute security we get by executing multiple query rounds
-    let security_per_query = 0.5 * blowup_plus_bits - (1.0 + 1.0 / (2.0 * m)).log2();
-    let mut query_security = (security_per_query * num_fri_queries) as u32;
+    let m = m as f64;
+    let rho = 1.0 / options.blowup_factor() as f64;
+    let alpha = (1.0 + 0.5 / m) * rho.sqrt();
+    let theta = 1.0 - alpha;
+    let max_deg = options.blowup_factor() as f64;
+
+    let lde_domain_size = lde_domain_size as f64;
+    let trace_domain_size = trace_domain_size as f64;
+
+    // Computes FRI commit-phase (i.e., pre-query) soundness error.
+    // This considers only the first term given in eq. 7 in https://eprint.iacr.org/2022/1216.pdf,
+    // i.e. 0.5 * (m + 0.5)^7 * n^2 / (rho^1.5.q) as all other terms are negligible in comparison.
+    let fri_commit_err_bits = extension_field_bits
+        - ((0.5 * (m + 0.5).powf(7.0) / rho.powf(1.5)) * lde_domain_size.powf(2.0)).log2();
+
+    // Compute FRI query-phase soundness error
+    let fri_queries_err_bits =
+        options.grinding_factor() as f64 - ((1.0 - theta).powf(num_fri_queries)).log2();
+
+    // Combined error for FRI
+    let fri_err_bits = cmp::min(fri_commit_err_bits as u64, fri_queries_err_bits as u64);
+    if fri_err_bits < 1 {
+        return 0;
+    }
+    let fri_err_bits = fri_err_bits - 1;
+
+    // To apply Theorem 8 in https://eprint.iacr.org/2022/1216.pdf, we need to apply FRI with
+    // a slightly larger agreement parameter alpha.
+    // More concretely, we need alpha > rho_plus.sqrt() where rho_plus is the rate in function field
+    // F(Z) and defined as (trace_domain_size + 2.0) / lde_domain_size .
+    // This means that the range of m needs to be restricted in order to ensure that
+    // alpha := 1 - theta := rho.sqrt() * (1 + 1/2m) is greater than rho_plus.sqrt().
+    // Determining the range of m is the responsibility of the calling function.
+    // Now, once m is fixed, we need to make sure that we choose an m_plus such that
+    // alpha <= rho_plus.sqrt() * (1 + 1/2m_plus). This m_plus will be used to define
+    // the list-decoding list size in F(Z).
+
+    // Modified rate in function field F(Z)
+    let rho_plus = (trace_domain_size + 2.0) / lde_domain_size;
+    // New proximity parameter m_plus, corresponding to rho_plus, needed to make sure that
+    //  alpha < rho_plus.sqrt() * (1 + 1 / (2 * m_plus))
+    let m_plus = (1.0 / (2.0 * (alpha / rho_plus.sqrt() - 1.0))).ceil();
+
+    // List size
+    let l_plus = (2.0 * m_plus + 1.0) / (2.0 * rho_plus.sqrt());
+
+    // ALI related soundness error. Note that C here is equal to 1 because of our use of
+    // linear batching.
+    let ali_err_bits = -l_plus.log2() + extension_field_bits;
+
+    // DEEP related soundness error. Note that this uses that the denominator |F| - |D ∪ H|
+    // can be approximated by |F| for all practical domain sizes.
+    let deep_err_bits =
+        -(l_plus * (max_deg * (trace_domain_size + 1.0) + (trace_domain_size - 1.0))).log2()
+            + extension_field_bits;
+
+    let min = cmp::min(cmp::min(fri_err_bits, ali_err_bits as u64), deep_err_bits as u64);
+    if min < 1 {
+        return 0;
+    }
 
-    query_security += options.grinding_factor();
+    min - 1
+}
 
-    cmp::min(cmp::min(pre_query_security, query_security) - 1, collision_resistance)
+/// Computes the largest proximity parameter m needed for Theorem 8
+/// in <https://eprint.iacr.org/2022/1216.pdf> to work.
+#[cfg(feature = "std")]
+fn compute_upper_m(h: u64) -> f64 {
+    let h = h as f64;
+    let m_max = (0.25 * h * (1.0 + (1.0 + 2.0 / h).sqrt())).ceil();
+
+    // We cap the range to 1000 as the optimal m value will be in the lower range of [m_min, m_max]
+    // since increasing m too much will lead to a deterioration in the FRI commit soundness making
+    // any benefit gained in the FRI query soundess mute.
+    cmp::min(m_max as u64, MAX_PROXIMITY_PARAMETER) as f64
 }