diff --git a/.github/workflows/test-rust-workspace-msrv.yml b/.github/workflows/test-rust-workspace-msrv.yml
index 662d5a39720..6fd71eb56a2 100644
--- a/.github/workflows/test-rust-workspace-msrv.yml
+++ b/.github/workflows/test-rust-workspace-msrv.yml
@@ -87,6 +87,7 @@ jobs:
           name: nextest-archive
       - name: Run tests
         run: |
+          RUST_MIN_STACK=8388608 \
           cargo nextest run --archive-file nextest-archive.tar.zst \
             --partition count:${{ matrix.partition }}/4 \
             --no-fail-fast
diff --git a/.github/workflows/test-rust-workspace.yml b/.github/workflows/test-rust-workspace.yml
index 1053d985d88..1514270ff56 100644
--- a/.github/workflows/test-rust-workspace.yml
+++ b/.github/workflows/test-rust-workspace.yml
@@ -74,6 +74,7 @@ jobs:
           name: nextest-archive
       - name: Run tests
         run: |
+          RUST_MIN_STACK=8388608 \
           cargo nextest run --archive-file nextest-archive.tar.zst \
             --partition count:${{ matrix.partition }}/4 \
             --no-fail-fast
diff --git a/Cargo.lock b/Cargo.lock
index cf96770e9b8..4907de7ae62 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -3187,6 +3187,7 @@ dependencies = [
  "test-case",
  "thiserror",
  "tracing",
+ "tracing-test",
 ]
 
 [[package]]
@@ -5075,6 +5076,27 @@ dependencies = [
  "tracing-log",
 ]
 
+[[package]]
+name = "tracing-test"
+version = "0.2.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "557b891436fe0d5e0e363427fc7f217abf9ccd510d5136549847bdcbcd011d68"
+dependencies = [
+ "tracing-core",
+ "tracing-subscriber",
+ "tracing-test-macro",
+]
+
+[[package]]
+name = "tracing-test-macro"
+version = "0.2.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "04659ddb06c87d233c566112c1c9c5b9e98256d9af50ec3bc9c8327f873a7568"
+dependencies = [
+ "quote",
+ "syn 2.0.87",
+]
+
 [[package]]
 name = "tracing-web"
 version = "0.1.3"
@@ -5399,7 +5421,7 @@ version = "0.1.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "cf221c93e13a30d793f7645a0e7762c55d169dbb0a49671918a2319d289b10bb"
 dependencies = [
- "windows-sys 0.59.0",
+ "windows-sys 0.48.0",
 ]
 
 [[package]]
diff --git a/compiler/noirc_driver/src/lib.rs b/compiler/noirc_driver/src/lib.rs
index da5297f4a4a..9318e4d2b5c 100644
--- a/compiler/noirc_driver/src/lib.rs
+++ b/compiler/noirc_driver/src/lib.rs
@@ -131,6 +131,12 @@ pub struct CompileOptions {
     #[arg(long)]
     pub skip_underconstrained_check: bool,
 
+    /// Flag to turn off the compiler check for missing Brillig call constrains.
+    /// Warning: This can improve compilation speed but can also lead to correctness errors.
+    /// This check should always be run on production code.
+    #[arg(long)]
+    pub skip_brillig_constraints_check: bool,
+
     /// Setting to decide on an inlining strategy for Brillig functions.
     /// A more aggressive inliner should generate larger programs but more optimized
     /// A less aggressive inliner should generate smaller programs
@@ -631,6 +637,7 @@ pub fn compile_no_check(
         },
         emit_ssa: if options.emit_ssa { Some(context.package_build_path.clone()) } else { None },
         skip_underconstrained_check: options.skip_underconstrained_check,
+        skip_brillig_constraints_check: options.skip_brillig_constraints_check,
         inliner_aggressiveness: options.inliner_aggressiveness,
         max_bytecode_increase_percent: options.max_bytecode_increase_percent,
     };
diff --git a/compiler/noirc_evaluator/Cargo.toml b/compiler/noirc_evaluator/Cargo.toml
index bb8c62cfd95..72fba8aadc2 100644
--- a/compiler/noirc_evaluator/Cargo.toml
+++ b/compiler/noirc_evaluator/Cargo.toml
@@ -32,6 +32,7 @@ cfg-if.workspace = true
 [dev-dependencies]
 proptest.workspace = true
 similar-asserts.workspace = true
+tracing-test = "0.2.5"
 num-traits.workspace = true
 test-case.workspace = true
 
diff --git a/compiler/noirc_evaluator/src/errors.rs b/compiler/noirc_evaluator/src/errors.rs
index 75a3ceb3a72..bb224617994 100644
--- a/compiler/noirc_evaluator/src/errors.rs
+++ b/compiler/noirc_evaluator/src/errors.rs
@@ -93,7 +93,10 @@ impl From<SsaReport> for FileDiagnostic {
                 let message = bug.to_string();
                 let (secondary_message, call_stack) = match bug {
                     InternalBug::IndependentSubgraph { call_stack } => {
-                        ("There is no path from the output of this brillig call to either return values or inputs of the circuit, which creates an independent subgraph. This is quite likely a soundness vulnerability".to_string(),call_stack)
+                        ("There is no path from the output of this Brillig call to either return values or inputs of the circuit, which creates an independent subgraph. This is quite likely a soundness vulnerability".to_string(), call_stack)
+                    }
+                    InternalBug::UncheckedBrilligCall { call_stack } => {
+                        ("This Brillig call's inputs and its return values haven't been sufficiently constrained. This should be done to prevent potential soundness vulnerabilities".to_string(), call_stack)
                     }
                     InternalBug::AssertFailed { call_stack } => ("As a result, the compiled circuit is ensured to fail. Other assertions may also fail during execution".to_string(), call_stack)
                 };
@@ -117,8 +120,10 @@ pub enum InternalWarning {
 
 #[derive(Debug, PartialEq, Eq, Clone, Error, Serialize, Deserialize, Hash)]
 pub enum InternalBug {
-    #[error("Input to brillig function is in a separate subgraph to output")]
+    #[error("Input to Brillig function is in a separate subgraph to output")]
     IndependentSubgraph { call_stack: CallStack },
+    #[error("Brillig function call isn't properly covered by a manual constraint")]
+    UncheckedBrilligCall { call_stack: CallStack },
     #[error("Assertion is always false")]
     AssertFailed { call_stack: CallStack },
 }
diff --git a/compiler/noirc_evaluator/src/ssa.rs b/compiler/noirc_evaluator/src/ssa.rs
index 365255d67a7..9377cadb260 100644
--- a/compiler/noirc_evaluator/src/ssa.rs
+++ b/compiler/noirc_evaluator/src/ssa.rs
@@ -72,7 +72,10 @@ pub struct SsaEvaluatorOptions {
     /// Skip the check for under constrained values
     pub skip_underconstrained_check: bool,
 
-    /// The higher the value, the more inlined brillig functions will be.
+    /// Skip the missing Brillig call constraints check
+    pub skip_brillig_constraints_check: bool,
+
+    /// The higher the value, the more inlined Brillig functions will be.
     pub inliner_aggressiveness: i64,
 
     /// Maximum accepted percentage increase in the Brillig bytecode size after unrolling loops.
@@ -104,12 +107,22 @@ pub(crate) fn optimize_into_acir(
 
     let mut ssa = optimize_all(builder, options)?;
 
-    let ssa_level_warnings = if options.skip_underconstrained_check {
-        vec![]
-    } else {
-        time("After Check for Underconstrained Values", options.print_codegen_timings, || {
-            ssa.check_for_underconstrained_values()
-        })
+    let mut ssa_level_warnings = vec![];
+
+    if !options.skip_underconstrained_check {
+        ssa_level_warnings.extend(time(
+            "After Check for Underconstrained Values",
+            options.print_codegen_timings,
+            || ssa.check_for_underconstrained_values(),
+        ));
+    }
+
+    if !options.skip_brillig_constraints_check {
+        ssa_level_warnings.extend(time(
+            "After Check for Missing Brillig Call Constraints",
+            options.print_codegen_timings,
+            || ssa.check_for_missing_brillig_constraints(),
+        ));
     };
 
     drop(ssa_gen_span_guard);
diff --git a/compiler/noirc_evaluator/src/ssa/checks/check_for_underconstrained_values.rs b/compiler/noirc_evaluator/src/ssa/checks/check_for_underconstrained_values.rs
index a3421fce8e6..40c9dc03ec3 100644
--- a/compiler/noirc_evaluator/src/ssa/checks/check_for_underconstrained_values.rs
+++ b/compiler/noirc_evaluator/src/ssa/checks/check_for_underconstrained_values.rs
@@ -1,6 +1,6 @@
-//! This module defines an SSA pass that detects if the final function has any subgraphs independent from inputs and outputs.
-//! If this is the case, then part of the final circuit can be completely replaced by any other passing circuit, since there are no constraints ensuring connections.
-//! So the compiler informs the developer of this as a bug
+//! This module defines security SSA passes detecting constraint problems leading to possible
+//! soundness vulnerabilities.
+//! The compiler informs the developer of these as bugs.
 use crate::errors::{InternalBug, SsaReport};
 use crate::ssa::ir::basic_block::BasicBlockId;
 use crate::ssa::ir::function::RuntimeType;
@@ -11,17 +11,20 @@ use crate::ssa::ssa_gen::Ssa;
 use im::HashMap;
 use rayon::prelude::*;
 use std::collections::{BTreeMap, HashSet};
+use tracing::trace;
 
 impl Ssa {
-    /// Go through each top-level non-brillig function and detect if it has independent subgraphs
+    /// This function provides an SSA pass that detects if the final function has any subgraphs independent from inputs and outputs.
+    /// If this is the case, then part of the final circuit can be completely replaced by any other passing circuit, since there are no constraints ensuring connections.
+    /// Go through each top-level non-Brillig function and detect if it has independent subgraphs
     #[tracing::instrument(level = "trace", skip(self))]
     pub(crate) fn check_for_underconstrained_values(&mut self) -> Vec<SsaReport> {
-        let functions_id = self.functions.values().map(|f| f.id().to_usize()).collect::<Vec<_>>();
-        functions_id
-            .iter()
+        self.functions
+            .values()
+            .map(|f| f.id())
             .par_bridge()
             .flat_map(|fid| {
-                let function_to_process = &self.functions[&FunctionId::new(*fid)];
+                let function_to_process = &self.functions[&fid];
                 match function_to_process.runtime() {
                     RuntimeType::Acir { .. } => check_for_underconstrained_values_within_function(
                         function_to_process,
@@ -32,6 +35,32 @@ impl Ssa {
             })
             .collect()
     }
+
+    /// Detect Brillig calls left unconstrained with manual asserts
+    /// and return a vector of bug reports if any have been found
+    pub(crate) fn check_for_missing_brillig_constraints(&mut self) -> Vec<SsaReport> {
+        // Skip the check if there are no Brillig functions involved
+        if !self.functions.values().any(|func| func.runtime().is_brillig()) {
+            return vec![];
+        };
+
+        self.functions
+            .values()
+            .map(|f| f.id())
+            .par_bridge()
+            .flat_map(|fid| {
+                let function_to_process = &self.functions[&fid];
+                match function_to_process.runtime() {
+                    RuntimeType::Acir { .. } => {
+                        let mut context = DependencyContext::default();
+                        context.build(function_to_process, &self.functions);
+                        context.collect_warnings(function_to_process)
+                    }
+                    RuntimeType::Brillig(_) => Vec::new(),
+                }
+            })
+            .collect()
+    }
 }
 
 /// Detect independent subgraphs (not connected to function inputs or outputs) and return a vector of bug reports if some are found
@@ -63,6 +92,348 @@ fn check_for_underconstrained_values_within_function(
     }
     warnings
 }
+
+#[derive(Default)]
+struct DependencyContext {
+    visited_blocks: HashSet<BasicBlockId>,
+    block_queue: Vec<BasicBlockId>,
+    // Map keeping track of values stored at memory locations
+    memory_slots: HashMap<ValueId, ValueId>,
+    // Map of values resulting from array get instructions
+    // to the actual array values
+    array_elements: HashMap<ValueId, ValueId>,
+    // Map of brillig call ids to sets of the value ids descending
+    // from their arguments and results
+    tainted: HashMap<InstructionId, BrilligTaintedIds>,
+}
+
+/// Structure keeping track of value ids descending from Brillig calls'
+/// arguments and results, also storing information on results
+/// already properly constrained
+#[derive(Clone, Debug)]
+struct BrilligTaintedIds {
+    // Argument descendant value ids
+    arguments: HashSet<ValueId>,
+    // Results status
+    results: Vec<ResultStatus>,
+    // Initial result value ids
+    root_results: HashSet<ValueId>,
+}
+
+#[derive(Clone, Debug)]
+enum ResultStatus {
+    // Keep track of descendants until found constrained
+    Unconstrained { descendants: HashSet<ValueId> },
+    Constrained,
+}
+
+impl BrilligTaintedIds {
+    fn new(arguments: &[ValueId], results: &[ValueId]) -> Self {
+        BrilligTaintedIds {
+            arguments: HashSet::from_iter(arguments.iter().copied()),
+            results: results
+                .iter()
+                .map(|result| ResultStatus::Unconstrained { descendants: HashSet::from([*result]) })
+                .collect(),
+            root_results: HashSet::from_iter(results.iter().copied()),
+        }
+    }
+
+    /// Add children of a given parent to the tainted value set
+    /// (for arguments one set is enough, for results we keep them
+    /// separate as the forthcoming check considers the call covered
+    /// if all the results were properly covered)
+    fn update_children(&mut self, parents: &HashSet<ValueId>, children: &[ValueId]) {
+        if self.arguments.intersection(parents).next().is_some() {
+            self.arguments.extend(children);
+        }
+        for result_status in &mut self.results.iter_mut() {
+            match result_status {
+                // Skip updating results already found covered
+                ResultStatus::Constrained => {
+                    continue;
+                }
+                ResultStatus::Unconstrained { descendants } => {
+                    if descendants.intersection(parents).next().is_some() {
+                        descendants.extend(children);
+                    }
+                }
+            }
+        }
+    }
+
+    /// If Brillig call is properly constrained by the given ids, return true
+    fn check_constrained(&self) -> bool {
+        // If every result has now been constrained,
+        // consider the call properly constrained
+        self.results.iter().all(|result| matches!(result, ResultStatus::Constrained))
+    }
+
+    /// Remember partial constraints (involving some of the results and an argument)
+    /// along the way to take them into final consideration
+    /// Generally, a valid partial constraint should link up a result descendant
+    /// and an argument descendant, although there are also edge cases mentioned below.
+    fn store_partial_constraints(&mut self, constrained_values: &HashSet<ValueId>) {
+        let mut results_involved: Vec<usize> = vec![];
+
+        // For a valid partial constraint, a value descending from
+        // one of the results should be constrained
+        for (i, result_status) in self.results.iter().enumerate() {
+            match result_status {
+                // Skip checking already covered results
+                ResultStatus::Constrained => {
+                    continue;
+                }
+                ResultStatus::Unconstrained { descendants } => {
+                    if descendants.intersection(constrained_values).next().is_some() {
+                        results_involved.push(i);
+                    }
+                }
+            }
+        }
+
+        // Along with it, one of the argument descendants should be constrained
+        // (skipped if there were no arguments, or if an actual result and not a
+        // descendant has been constrained _alone_, e.g. against a constant)
+        if !results_involved.is_empty()
+            && (self.arguments.is_empty()
+                || (constrained_values.len() == 1
+                    && self.root_results.intersection(constrained_values).next().is_some())
+                || self.arguments.intersection(constrained_values).next().is_some())
+        {
+            // Remember the partial constraint, clearing the sets
+            results_involved.iter().for_each(|i| self.results[*i] = ResultStatus::Constrained);
+        }
+    }
+}
+
+impl DependencyContext {
+    /// Build the dependency context of variable ValueIds, storing
+    /// information on value ids involved in unchecked Brillig calls
+    fn build(&mut self, function: &Function, all_functions: &BTreeMap<FunctionId, Function>) {
+        self.block_queue.push(function.entry_block());
+        while let Some(block) = self.block_queue.pop() {
+            if self.visited_blocks.contains(&block) {
+                continue;
+            }
+            self.visited_blocks.insert(block);
+            self.process_instructions(block, function, all_functions);
+        }
+    }
+
+    /// Go over the given block tracking Brillig calls and checking them against
+    /// following constraints
+    fn process_instructions(
+        &mut self,
+        block: BasicBlockId,
+        function: &Function,
+        all_functions: &BTreeMap<FunctionId, Function>,
+    ) {
+        trace!("processing instructions of block {} of function {}", block, function);
+
+        for instruction in function.dfg[block].instructions() {
+            let mut arguments = Vec::new();
+            let mut results = Vec::new();
+
+            // Collect non-constant instruction arguments
+            function.dfg[*instruction].for_each_value(|value_id| {
+                if function.dfg.get_numeric_constant(value_id).is_none() {
+                    arguments.push(function.dfg.resolve(value_id));
+                }
+            });
+
+            // Collect non-constant instruction results
+            for value_id in function.dfg.instruction_results(*instruction).iter() {
+                if function.dfg.get_numeric_constant(*value_id).is_none() {
+                    results.push(function.dfg.resolve(*value_id));
+                }
+            }
+
+            // Process instructions
+            match &function.dfg[*instruction] {
+                // For memory operations, we have to link up the stored value as a parent
+                // of one loaded from the same memory slot
+                Instruction::Store { address, value } => {
+                    self.memory_slots.insert(*address, function.dfg.resolve(*value));
+                }
+                Instruction::Load { address } => {
+                    // Recall the value stored at address as parent for the results
+                    if let Some(value_id) = self.memory_slots.get(address) {
+                        self.update_children(&[*value_id], &results);
+                    } else {
+                        panic!("load instruction {} has attempted to access previously unused memory location",
+                            instruction);
+                    }
+                }
+                // Check the constrain instruction arguments against those
+                // involved in Brillig calls, remove covered calls
+                Instruction::Constrain(value_id1, value_id2, _) => {
+                    self.clear_constrained(
+                        &[function.dfg.resolve(*value_id1), function.dfg.resolve(*value_id2)],
+                        function,
+                    );
+                }
+                // Consider range check to also be constraining
+                Instruction::RangeCheck { value, .. } => {
+                    self.clear_constrained(&[function.dfg.resolve(*value)], function);
+                }
+                Instruction::Call { func: func_id, .. } => {
+                    // For functions, we remove the first element of arguments,
+                    // as .for_each_value() used previously also includes func_id
+                    arguments.remove(0);
+
+                    match &function.dfg[*func_id] {
+                        Value::Intrinsic(intrinsic) => match intrinsic {
+                            Intrinsic::ApplyRangeConstraint | Intrinsic::AssertConstant => {
+                                // Consider these intrinsic arguments constrained
+                                self.clear_constrained(&arguments, function);
+                            }
+                            Intrinsic::AsWitness | Intrinsic::IsUnconstrained => {
+                                // These intrinsics won't affect the dependency graph
+                            }
+                            Intrinsic::ArrayLen
+                            | Intrinsic::ArrayRefCount
+                            | Intrinsic::ArrayAsStrUnchecked
+                            | Intrinsic::AsField
+                            | Intrinsic::AsSlice
+                            | Intrinsic::BlackBox(..)
+                            | Intrinsic::DerivePedersenGenerators
+                            | Intrinsic::FromField
+                            | Intrinsic::Hint(..)
+                            | Intrinsic::SlicePushBack
+                            | Intrinsic::SlicePushFront
+                            | Intrinsic::SlicePopBack
+                            | Intrinsic::SlicePopFront
+                            | Intrinsic::SliceRefCount
+                            | Intrinsic::SliceInsert
+                            | Intrinsic::SliceRemove
+                            | Intrinsic::StaticAssert
+                            | Intrinsic::StrAsBytes
+                            | Intrinsic::ToBits(..)
+                            | Intrinsic::ToRadix(..)
+                            | Intrinsic::FieldLessThan => {
+                                // Record all the function arguments as parents of the results
+                                self.update_children(&arguments, &results);
+                            }
+                        },
+                        Value::Function(callee) => match all_functions[&callee].runtime() {
+                            RuntimeType::Brillig(_) => {
+                                // Record arguments/results for each Brillig call for the check
+                                trace!(
+                                    "Brillig function {} called at {}",
+                                    all_functions[&callee],
+                                    instruction
+                                );
+                                self.tainted.insert(
+                                    *instruction,
+                                    BrilligTaintedIds::new(&arguments, &results),
+                                );
+                            }
+                            RuntimeType::Acir(..) => {
+                                // Record all the function arguments as parents of the results
+                                self.update_children(&arguments, &results);
+                            }
+                        },
+                        Value::ForeignFunction(..) => {
+                            panic!("should not be able to reach foreign function from non-Brillig functions, {func_id} in function {}", function.name());
+                        }
+                        Value::Instruction { .. }
+                        | Value::NumericConstant { .. }
+                        | Value::Param { .. } => {
+                            panic!(
+                                "calling non-function value with ID {func_id} in function {}",
+                                function.name()
+                            );
+                        }
+                    }
+                }
+                // For array get operations, we link the resulting values to
+                // the corresponding array value ids
+                // (this is required later because for now we consider array elements
+                // being constrained as valid as the whole arrays being constrained)
+                Instruction::ArrayGet { array, .. } => {
+                    for result in &results {
+                        self.array_elements.insert(*result, function.dfg.resolve(*array));
+                    }
+                    // Record all the used arguments as parents of the results
+                    self.update_children(&arguments, &results);
+                }
+                Instruction::ArraySet { .. }
+                | Instruction::Binary(..)
+                | Instruction::Cast(..)
+                | Instruction::IfElse { .. }
+                | Instruction::Not(..)
+                | Instruction::Truncate { .. } => {
+                    // Record all the used arguments as parents of the results
+                    self.update_children(&arguments, &results);
+                }
+                // These instructions won't affect the dependency graph
+                Instruction::Allocate { .. }
+                | Instruction::DecrementRc { .. }
+                | Instruction::EnableSideEffectsIf { .. }
+                | Instruction::IncrementRc { .. }
+                | Instruction::MakeArray { .. } => {}
+            }
+        }
+
+        trace!("resulting Brillig involved values: {:?}", self.tainted);
+    }
+
+    /// Every Brillig call not properly constrained should remain in the tainted set
+    /// at this point. For each, emit a corresponding warning.
+    fn collect_warnings(&mut self, function: &Function) -> Vec<SsaReport> {
+        let warnings: Vec<SsaReport> = self
+            .tainted
+            .keys()
+            .map(|brillig_call| {
+                SsaReport::Bug(InternalBug::UncheckedBrilligCall {
+                    call_stack: function.dfg.get_call_stack(*brillig_call),
+                })
+            })
+            .collect();
+
+        trace!("making following reports for function {}: {:?}", function.name(), warnings);
+        warnings
+    }
+
+    /// Update sets of value ids that can be traced back to the Brillig calls being tracked
+    fn update_children(&mut self, parents: &[ValueId], children: &[ValueId]) {
+        let parents: HashSet<_> = HashSet::from_iter(parents.iter().copied());
+        for (_, tainted_ids) in self.tainted.iter_mut() {
+            tainted_ids.update_children(&parents, children);
+        }
+    }
+
+    /// Check if any of the recorded Brillig calls have been properly constrained
+    /// by given values after recording partial constraints, if so stop tracking them
+    fn clear_constrained(&mut self, constrained_values: &[ValueId], function: &Function) {
+        trace!("attempting to clear Brillig calls constrained by values: {:?}", constrained_values);
+
+        // Remove numeric constants
+        let constrained_values =
+            constrained_values.iter().filter(|v| function.dfg.get_numeric_constant(**v).is_none());
+
+        // For now, consider array element constraints to be array constraints
+        // TODO(https://github.com/noir-lang/noir/issues/6698):
+        // This probably has to be further looked into, to ensure _every_ element
+        // of an array result of a Brillig call has been constrained
+        let constrained_values: HashSet<_> = constrained_values
+            .map(|v| {
+                if let Some(parent_array) = self.array_elements.get(v) {
+                    *parent_array
+                } else {
+                    *v
+                }
+            })
+            .collect();
+
+        self.tainted.iter_mut().for_each(|(_, tainted_ids)| {
+            tainted_ids.store_partial_constraints(&constrained_values);
+        });
+        self.tainted.retain(|_, tainted_ids| !tainted_ids.check_constrained());
+    }
+}
+
 #[derive(Default)]
 struct Context {
     visited_blocks: HashSet<BasicBlockId>,
@@ -75,7 +446,7 @@ struct Context {
 impl Context {
     /// Compute sets of variable ValueIds that are connected with constraints
     ///
-    /// Additionally, store information about brillig calls in the context
+    /// Additionally, store information about Brillig calls in the context
     fn compute_sets_of_connected_value_ids(
         &mut self,
         function: &Function,
@@ -122,7 +493,7 @@ impl Context {
         connected_sets_indices
     }
 
-    /// Find which brillig calls separate this set from others and return bug warnings about them
+    /// Find which Brillig calls separate this set from others and return bug warnings about them
     fn find_disconnecting_brillig_calls_with_results_in_set(
         &self,
         current_set: &HashSet<ValueId>,
@@ -133,7 +504,7 @@ impl Context {
         // Find brillig-generated values in the set
         let intersection = all_brillig_generated_values.intersection(current_set).copied();
 
-        // Go through all brillig outputs in the set
+        // Go through all Brillig outputs in the set
         for brillig_output_in_set in intersection {
             // Get the inputs that correspond to the output
             let inputs: HashSet<ValueId> =
@@ -155,7 +526,7 @@ impl Context {
     }
     /// Go through each instruction in the block and add a set of ValueIds connected through that instruction
     ///
-    /// Additionally, this function adds mappings of brillig return values to call arguments and instruction ids from calls to brillig functions in the block
+    /// Additionally, this function adds mappings of Brillig return values to call arguments and instruction ids from calls to Brillig functions in the block
     fn connect_value_ids_in_block(
         &mut self,
         function: &Function,
@@ -229,7 +600,7 @@ impl Context {
                         },
                         Value::Function(callee) => match all_functions[&callee].runtime() {
                             RuntimeType::Brillig(_) => {
-                                // For calls to brillig functions we memorize the mapping of results to argument ValueId's and InstructionId's
+                                // For calls to Brillig functions we memorize the mapping of results to argument ValueId's and InstructionId's
                                 // The latter are needed to produce the callstack later
                                 for result in
                                     function.dfg.instruction_results(*instruction).iter().filter(
@@ -249,7 +620,7 @@ impl Context {
                             }
                         },
                         Value::ForeignFunction(..) => {
-                            panic!("Should not be able to reach foreign function from non-brillig functions, {func_id} in function {}", function.name());
+                            panic!("Should not be able to reach foreign function from non-Brillig functions, {func_id} in function {}", function.name());
                         }
                         Value::Instruction { .. }
                         | Value::NumericConstant { .. }
@@ -355,83 +726,297 @@ impl Context {
 }
 #[cfg(test)]
 mod test {
-    use noirc_frontend::monomorphization::ast::InlineType;
-
-    use crate::ssa::{
-        function_builder::FunctionBuilder,
-        ir::{instruction::BinaryOp, map::Id, types::Type},
-    };
+    use crate::ssa::Ssa;
+    use tracing_test::traced_test;
 
     #[test]
+    #[traced_test]
     /// Test that a connected function raises no warnings
     fn test_simple_connected_function() {
-        // fn main {
-        //   b0(v0: Field, v1: Field):
-        //      v2 = add v0, 1
-        //      v3 = mul v1, 2
-        //      v4 = eq v2, v3
-        //      return v2
-        // }
-        let main_id = Id::test_new(0);
-        let mut builder = FunctionBuilder::new("main".into(), main_id);
-        let v0 = builder.add_parameter(Type::field());
-        let v1 = builder.add_parameter(Type::field());
-
-        let one = builder.field_constant(1u128);
-        let two = builder.field_constant(2u128);
-
-        let v2 = builder.insert_binary(v0, BinaryOp::Add, one);
-        let v3 = builder.insert_binary(v1, BinaryOp::Mul, two);
-        let _v4 = builder.insert_binary(v2, BinaryOp::Eq, v3);
-        builder.terminate_with_return(vec![v2]);
-
-        let mut ssa = builder.finish();
+        let program = r#"
+        acir(inline) fn main f0 {
+            b0(v0: Field, v1: Field):
+                v2 = add v0, Field 1
+                v3 = mul v1, Field 2
+                v4 = eq v2, v3
+                return v2
+        }
+        "#;
+
+        let mut ssa = Ssa::from_str(program).unwrap();
         let ssa_level_warnings = ssa.check_for_underconstrained_values();
         assert_eq!(ssa_level_warnings.len(), 0);
     }
 
     #[test]
-    /// Test where the results of a call to a brillig function are not connected to main function inputs or outputs
+    #[traced_test]
+    /// Test where the results of a call to a Brillig function are not connected to main function inputs or outputs
     /// This should be detected.
     fn test_simple_function_with_disconnected_part() {
-        //  unconstrained fn br(v0: Field, v1: Field){
-        //      v2 = add v0, v1
-        //      return v2
-        //  }
-        //
-        //  fn main {
-        //   b0(v0: Field, v1: Field):
-        //      v2 = add v0, 1
-        //      v3 = mul v1, 2
-        //      v4 = call br(v2, v3)
-        //      v5 = add v4, 2
-        //      return
-        // }
-        let main_id = Id::test_new(0);
-        let mut builder = FunctionBuilder::new("main".into(), main_id);
-        let v0 = builder.add_parameter(Type::field());
-        let v1 = builder.add_parameter(Type::field());
-
-        let one = builder.field_constant(1u128);
-        let two = builder.field_constant(2u128);
-
-        let v2 = builder.insert_binary(v0, BinaryOp::Add, one);
-        let v3 = builder.insert_binary(v1, BinaryOp::Mul, two);
-
-        let br_function_id = Id::test_new(1);
-        let br_function = builder.import_function(br_function_id);
-        let v4 = builder.insert_call(br_function, vec![v2, v3], vec![Type::field()])[0];
-        let v5 = builder.insert_binary(v4, BinaryOp::Add, two);
-        builder.insert_constrain(v5, one, None);
-        builder.terminate_with_return(vec![]);
-
-        builder.new_brillig_function("br".into(), br_function_id, InlineType::default());
-        let v0 = builder.add_parameter(Type::field());
-        let v1 = builder.add_parameter(Type::field());
-        let v2 = builder.insert_binary(v0, BinaryOp::Add, v1);
-        builder.terminate_with_return(vec![v2]);
-        let mut ssa = builder.finish();
+        let program = r#"
+        acir(inline) fn main f0 {
+            b0(v0: Field, v1: Field):
+                v2 = add v0, Field 1
+                v3 = mul v1, Field 2
+                v4 = call f1(v2, v3) -> Field
+                v5 = add v4, Field 2
+                return
+        }
+        
+        brillig(inline) fn br f1 {
+          b0(v0: Field, v1: Field):
+            v2 = add v0, v1
+            return v2
+        }
+        "#;
+
+        let mut ssa = Ssa::from_str(program).unwrap();
         let ssa_level_warnings = ssa.check_for_underconstrained_values();
         assert_eq!(ssa_level_warnings.len(), 1);
     }
+
+    #[test]
+    #[traced_test]
+    /// Test where a call to a Brillig function is left unchecked with a later assert,
+    /// by example of the program illustrating issue #5425 (simplified variant).
+    fn test_underconstrained_value_detector_5425() {
+        /*
+        unconstrained fn maximum_price(options: [u32; 2]) -> u32 {
+            let mut maximum_option = options[0];
+            if (options[1] > options[0]) {
+                maximum_option = options[1];
+            }
+            maximum_option
+        }
+
+        fn main(sandwiches: pub [u32; 2], drinks: pub [u32; 2], best_value: u32) {
+            let most_expensive_sandwich = maximum_price(sandwiches);
+            let mut sandwich_exists = false;
+            sandwich_exists |= (sandwiches[0] == most_expensive_sandwich);
+            sandwich_exists |= (sandwiches[1] == most_expensive_sandwich);
+            assert(sandwich_exists);
+
+            let most_expensive_drink = maximum_price(drinks);
+            assert(
+                best_value
+                == (most_expensive_sandwich + most_expensive_drink)
+            );
+        }
+        */
+
+        // The Brillig function is fake, for simplicity's sake
+
+        let program = r#"
+        acir(inline) fn main f0 {
+          b0(v4: [u32; 2], v5: [u32; 2], v6: u32):
+            inc_rc v4
+            inc_rc v5
+            v8 = call f1(v4) -> u32
+            v9 = allocate -> &mut u32
+            store u1 0 at v9
+            v10 = load v9 -> u1
+            v11 = array_get v4, index u32 0 -> u32
+            v12 = eq v11, v8
+            v13 = or v10, v12
+            store v13 at v9
+            v14 = load v9 -> u1
+            v15 = array_get v4, index u32 1 -> u32
+            v16 = eq v15, v8
+            v17 = or v14, v16
+            store v17 at v9
+            v18 = load v9 -> u1
+            constrain v18 == u1 1
+            v19 = call f1(v5) -> u32
+            v20 = add v8, v19
+            constrain v6 == v20
+            dec_rc v4
+            dec_rc v5
+            return
+        }
+
+        brillig(inline) fn maximum_price f1 {
+          b0(v0: [u32; 2]):
+            v2 = array_get v0, index u32 0 -> u32
+            return v2
+        }
+        "#;
+
+        let mut ssa = Ssa::from_str(program).unwrap();
+        let ssa_level_warnings = ssa.check_for_missing_brillig_constraints();
+        assert_eq!(ssa_level_warnings.len(), 1);
+    }
+
+    #[test]
+    #[traced_test]
+    /// Test where a call to a Brillig function returning multiple result values
+    /// is left unchecked with a later assert involving all the results
+    fn test_unchecked_multiple_results_brillig() {
+        // First call is constrained properly, involving both results
+        // Second call is insufficiently constrained, involving only one of the results
+        // The Brillig function is fake, for simplicity's sake
+        let program = r#"
+        acir(inline) fn main f0 {
+          b0(v0: u32):
+            v2, v3 = call f1(v0) -> (u32, u32)
+            v4 = mul v2, v3
+            constrain v4 == v0
+            v5, v6 = call f1(v0) -> (u32, u32)
+            v7 = mul v5, v5
+            constrain v7 == v0
+            return
+        }
+
+        brillig(inline) fn factor f1 {
+          b0(v0: u32):
+            return u32 0, u32 0
+        }
+        "#;
+
+        let mut ssa = Ssa::from_str(program).unwrap();
+        let ssa_level_warnings = ssa.check_for_missing_brillig_constraints();
+        assert_eq!(ssa_level_warnings.len(), 1);
+    }
+
+    #[test]
+    #[traced_test]
+    /// Test where a Brillig function is called with a constant argument
+    /// (should _not_ lead to a false positive failed check
+    /// if all the results are constrained)
+    fn test_checked_brillig_with_constant_arguments() {
+        // The call is constrained properly, involving both results
+        // (but the argument to the Brillig is a constant)
+        // The Brillig function is fake, for simplicity's sake
+
+        let program = r#"
+        acir(inline) fn main f0 {
+          b0(v0: u32):
+            v3, v4 = call f1(Field 7) -> (u32, u32)
+            v5 = mul v3, v4
+            constrain v5 == v0
+            return
+        }
+
+        brillig(inline) fn factor f1 {
+          b0(v0: Field):
+            return u32 0, u32 0
+        }
+        "#;
+
+        let mut ssa = Ssa::from_str(program).unwrap();
+        let ssa_level_warnings = ssa.check_for_missing_brillig_constraints();
+        assert_eq!(ssa_level_warnings.len(), 0);
+    }
+
+    #[test]
+    #[traced_test]
+    /// Test where a Brillig function call is constrained with a range check
+    /// (should _not_ lead to a false positive failed check)
+    fn test_range_checked_brillig() {
+        // The call is constrained properly with a range check, involving
+        // both Brillig call argument and result
+        // The Brillig function is fake, for simplicity's sake
+
+        let program = r#"
+        acir(inline) fn main f0 {
+          b0(v0: u32):
+            v2 = call f1(v0) -> u32
+            v3 = add v2, v0
+            range_check v3 to 32 bits
+            return
+        }
+
+        brillig(inline) fn dummy f1 {
+          b0(v0: u32):
+            return u32 0
+        }
+        "#;
+
+        let mut ssa = Ssa::from_str(program).unwrap();
+        let ssa_level_warnings = ssa.check_for_missing_brillig_constraints();
+        assert_eq!(ssa_level_warnings.len(), 0);
+    }
+
+    #[test]
+    #[traced_test]
+    /// Test where a Brillig nested type result is insufficiently constrained
+    /// (with a field constraint missing)
+    fn test_nested_type_result_brillig() {
+        /*
+        struct Animal {
+            legs: Field,
+            eyes: u8,
+            tag: Tag,
+        }
+
+        struct Tag {
+            no: Field,
+        }
+
+        unconstrained fn foo(bar: Field) -> Animal {
+            Animal {
+                legs: 4,
+                eyes: 2,
+                tag: Tag { no: bar }
+            }
+        }
+
+        fn main(x: Field) -> pub Animal {
+            let dog = foo(x);
+            assert(dog.legs == 4);
+            assert(dog.tag.no == x);
+
+            dog
+        }
+        */
+
+        let program = r#"
+        acir(inline) fn main f0 {
+          b0(v0: Field):
+            v2, v3, v4 = call f1(v0) -> (Field, u8, Field)
+            v6 = eq v2, Field 4
+            constrain v2 == Field 4
+            v10 = eq v4, v0
+            constrain v4 == v0
+            return v2, v3, v4
+        }
+
+        brillig(inline) fn foo f1 {
+          b0(v0: Field):
+            return Field 4, u8 2, v0
+        }
+        "#;
+
+        let mut ssa = Ssa::from_str(program).unwrap();
+        let ssa_level_warnings = ssa.check_for_missing_brillig_constraints();
+        assert_eq!(ssa_level_warnings.len(), 1);
+    }
+
+    #[test]
+    #[traced_test]
+    /// Test where Brillig calls' root result values are constrained against
+    /// each other (covers a false negative edge case)
+    /// (https://github.com/noir-lang/noir/pull/6658#pullrequestreview-2482170066)
+    fn test_root_result_intersection_false_negative() {
+        let program = r#"
+        acir(inline) fn main f0 {
+          b0(v0: Field, v1: Field):
+            v3 = call f1(v0, v1) -> Field
+            v5 = call f1(v0, v1) -> Field
+            v6 = eq v3, v5
+            constrain v3 == v5
+            v8 = add v3, v5
+            return v8
+        }
+
+        brillig(inline) fn foo f1 {
+          b0(v0: Field, v1: Field):
+            v2 = add v0, v1
+            return v2
+        }
+        "#;
+
+        let mut ssa = Ssa::from_str(program).unwrap();
+        let ssa_level_warnings = ssa.check_for_missing_brillig_constraints();
+        assert_eq!(ssa_level_warnings.len(), 2);
+    }
 }
diff --git a/compiler/noirc_evaluator/src/ssa/opt/hint.rs b/compiler/noirc_evaluator/src/ssa/opt/hint.rs
index 147367261a8..567a0795edc 100644
--- a/compiler/noirc_evaluator/src/ssa/opt/hint.rs
+++ b/compiler/noirc_evaluator/src/ssa/opt/hint.rs
@@ -19,6 +19,7 @@ mod tests {
             expression_width: ExpressionWidth::default(),
             emit_ssa: None,
             skip_underconstrained_check: true,
+            skip_brillig_constraints_check: true,
             inliner_aggressiveness: 0,
             max_bytecode_increase_percent: None,
         };
diff --git a/test_programs/compile_success_with_bug/underconstrained_value_detector_5425/Nargo.toml b/test_programs/compile_success_with_bug/underconstrained_value_detector_5425/Nargo.toml
new file mode 100644
index 00000000000..48ab5a0390b
--- /dev/null
+++ b/test_programs/compile_success_with_bug/underconstrained_value_detector_5425/Nargo.toml
@@ -0,0 +1,7 @@
+[package]
+name = "underconstrained_value_detector_5425"
+type = "bin"
+authors = [""]
+compiler_version = ">=0.36.0"
+
+[dependencies]
\ No newline at end of file
diff --git a/test_programs/compile_success_with_bug/underconstrained_value_detector_5425/src/main.nr b/test_programs/compile_success_with_bug/underconstrained_value_detector_5425/src/main.nr
new file mode 100644
index 00000000000..1d9269eebd5
--- /dev/null
+++ b/test_programs/compile_success_with_bug/underconstrained_value_detector_5425/src/main.nr
@@ -0,0 +1,48 @@
+unconstrained fn maximum_price(options: [u32; 3]) -> u32 {
+    let mut maximum_option = 0;
+    for option in options {
+        if (option > maximum_option) {
+            maximum_option = option;
+        }
+    }
+    maximum_option
+}
+
+fn main(sandwiches: pub [u32; 3], drinks: pub [u32; 3], snacks: pub [u32; 3], best_value: u32) {
+    unsafe {
+        let meal_deal_cost: u32 = 390;
+        let most_expensive_sandwich = maximum_price(sandwiches);
+        let mut sandwich_exists = false;
+        for sandwich_price in sandwiches {
+            assert(sandwich_price <= most_expensive_sandwich);
+            sandwich_exists |= sandwich_price == most_expensive_sandwich;
+        }
+
+        // maximum_price(sandwiches) is properly constrained with this assert,
+        // linking the result to the arguments
+        assert(sandwich_exists);
+
+        let most_expensive_drink = maximum_price(drinks);
+        let mut drink_exists = false;
+        for drink_price in drinks {
+            assert(drink_price <= most_expensive_drink);
+            drink_exists |= drink_price == most_expensive_drink;
+        }
+
+        // maximum_price(drinks) is properly constrained with this assert,
+        // linking the result to the arguments
+        assert(drink_exists);
+
+        let most_expensive_snack = maximum_price(snacks);
+        // maximum_price(snacks)'s result isn't constrained against `snacks`
+        // in any way, triggering the missing Brillig constraint check
+
+        assert(
+            best_value
+                == (
+                    most_expensive_sandwich + most_expensive_drink + most_expensive_snack
+                        - meal_deal_cost
+                ),
+        );
+    }
+}
diff --git a/tooling/nargo_cli/build.rs b/tooling/nargo_cli/build.rs
index 41b3c0c9cf7..db6177366d3 100644
--- a/tooling/nargo_cli/build.rs
+++ b/tooling/nargo_cli/build.rs
@@ -36,6 +36,7 @@ fn main() {
     generate_compile_success_empty_tests(&mut test_file, &test_dir);
     generate_compile_success_contract_tests(&mut test_file, &test_dir);
     generate_compile_success_no_bug_tests(&mut test_file, &test_dir);
+    generate_compile_success_with_bug_tests(&mut test_file, &test_dir);
     generate_compile_failure_tests(&mut test_file, &test_dir);
 }
 
@@ -458,6 +459,35 @@ fn generate_compile_success_no_bug_tests(test_file: &mut File, test_data_dir: &P
     writeln!(test_file, "}}").unwrap();
 }
 
+/// Generate tests for checking that the contract compiles and there are "bugs" in stderr
+fn generate_compile_success_with_bug_tests(test_file: &mut File, test_data_dir: &Path) {
+    let test_type = "compile_success_with_bug";
+    let test_cases = read_test_cases(test_data_dir, test_type);
+
+    writeln!(
+        test_file,
+        "mod {test_type} {{
+        use super::*;
+    "
+    )
+    .unwrap();
+    for (test_name, test_dir) in test_cases {
+        let test_dir = test_dir.display();
+
+        generate_test_cases(
+            test_file,
+            &test_name,
+            &test_dir,
+            "compile",
+            r#"
+                nargo.assert().success().stderr(predicate::str::contains("bug:"));
+            "#,
+            &MatrixConfig::default(),
+        );
+    }
+    writeln!(test_file, "}}").unwrap();
+}
+
 fn generate_compile_failure_tests(test_file: &mut File, test_data_dir: &Path) {
     let test_type = "compile_failure";
     let test_cases = read_test_cases(test_data_dir, test_type);