diff --git a/crates/formality-rust/src/check/fns.rs b/crates/formality-rust/src/check/fns.rs
index a790c7e91..9c015634e 100644
--- a/crates/formality-rust/src/check/fns.rs
+++ b/crates/formality-rust/src/check/fns.rs
@@ -2,6 +2,7 @@ use crate::check::borrow_check::env::TypeckEnv;
 use crate::check::borrow_check::flow_state::FlowState;
 use crate::check::borrow_check::nll::borrow_check;
 use crate::check::prove_goal;
+use crate::check::return_check::check_fn_returns;
 use crate::check::where_clauses::prove_where_clauses_well_formed;
 use crate::grammar::{CrateId, FnBody, MaybeFnBody, Relation, Wcs};
 use crate::prove::{Env, Program};
@@ -84,6 +85,7 @@ judgment_fn! {
         )
 
         (
+            (check_fn_returns(output_ty, block) => ())
             // Type-check an expression body via the borrow checker.
             (let typeck_env = TypeckEnv::for_fn_body(env, program, output_ty))
             (let initial_state = FlowState::for_fn_body(env, input_args)?)
diff --git a/crates/formality-rust/src/check/mod.rs b/crates/formality-rust/src/check/mod.rs
index a45d7a3b8..5a815a1b9 100644
--- a/crates/formality-rust/src/check/mod.rs
+++ b/crates/formality-rust/src/check/mod.rs
@@ -26,6 +26,7 @@ mod coherence;
 mod core_crate;
 mod fns;
 mod impls;
+mod return_check;
 mod traits;
 mod where_clauses;
 
diff --git a/crates/formality-rust/src/check/return_check.rs b/crates/formality-rust/src/check/return_check.rs
new file mode 100644
index 000000000..8923c8dcf
--- /dev/null
+++ b/crates/formality-rust/src/check/return_check.rs
@@ -0,0 +1,660 @@
+use crate::grammar::Fallible;
+use crate::grammar::{
+    expr::{Block, LabelId, Stmt},
+    Ty,
+};
+use anyhow::bail;
+use formality_core::judgment::ProofTree;
+use formality_core::{judgment_fn, term, Set};
+
+#[term]
+struct ControlFlow {
+    can_fall_through: bool,
+    breaks: Set<LabelId>,
+    continues: Set<LabelId>,
+}
+
+impl ControlFlow {
+    fn fallthrough() -> Self {
+        Self {
+            can_fall_through: true,
+            breaks: Set::new(),
+            continues: Set::new(),
+        }
+    }
+
+    fn returns() -> Self {
+        Self {
+            can_fall_through: false,
+            breaks: Set::new(),
+            continues: Set::new(),
+        }
+    }
+
+    fn break_to(label: LabelId) -> Self {
+        let mut breaks = Set::new();
+        breaks.insert(label);
+
+        Self {
+            can_fall_through: false,
+            breaks,
+            continues: Set::new(),
+        }
+    }
+
+    fn continue_to(label: LabelId) -> Self {
+        let mut continues = Set::new();
+        continues.insert(label);
+
+        Self {
+            can_fall_through: false,
+            breaks: Set::new(),
+            continues,
+        }
+    }
+
+    fn then(&self, next: &Self) -> Self {
+        if !self.can_fall_through {
+            return self.clone();
+        }
+
+        Self {
+            can_fall_through: next.can_fall_through,
+            breaks: self.breaks.union(&next.breaks).cloned().collect(),
+            continues: self.continues.union(&next.continues).cloned().collect(),
+        }
+    }
+
+    fn join(&self, other: &Self) -> Self {
+        Self {
+            can_fall_through: self.can_fall_through || other.can_fall_through,
+            breaks: self.breaks.union(&other.breaks).cloned().collect(),
+            continues: self.continues.union(&other.continues).cloned().collect(),
+        }
+    }
+
+    fn exit_block(&self, label: Option<&LabelId>) -> Self {
+        let mut breaks = self.breaks.clone();
+        let matching_break = label.is_some_and(|label| breaks.remove(label));
+
+        Self {
+            can_fall_through: self.can_fall_through || matching_break,
+            breaks,
+            continues: self.continues.clone(),
+        }
+    }
+
+    fn exit_loop(&self, label: Option<&LabelId>) -> Self {
+        let mut breaks = self.breaks.clone();
+        let mut continues = self.continues.clone();
+
+        let matching_break = if let Some(label) = label {
+            let matching_breaks = breaks.remove(label);
+            continues.remove(label);
+
+            matching_breaks
+        } else {
+            false
+        };
+
+        Self {
+            can_fall_through: matching_break,
+            breaks,
+            continues,
+        }
+    }
+}
+
+fn check_no_fallthrough(flow: &ControlFlow) -> Fallible<ProofTree> {
+    if flow.can_fall_through {
+        bail!("function may not return a value");
+    }
+
+    Ok(ProofTree::leaf("function does not fall through"))
+}
+
+judgment_fn! {
+  /// Checks whether every required path through a function returns a value.
+  pub(crate) fn check_fn_returns( output_ty: Ty, block: Block) => () {
+    debug(output_ty, block)
+
+    (
+      (if output_ty == &Ty::unit())
+      ---------------------------------------------------- ("unit")
+      (check_fn_returns(output_ty, block) => ())
+    )
+
+    (
+      (if output_ty != &Ty::unit())
+      (control_flow_block(block) => flow)
+      (check_no_fallthrough(flow) => ())
+      ---------------------------------------------------- ("non-unit return")
+      (check_fn_returns(output_ty, block) => ())
+    )
+  }
+}
+
+judgment_fn! {
+  /// Computes the control flow that can emerge from a block.
+  fn control_flow_block( block: Block) => ControlFlow {
+    debug(block)
+
+    (
+      (let flow = ControlFlow::fallthrough())
+        (for_all(i in 0..stmts.len()) with(flow)
+          (control_flow_stmt(&stmts[i]) => statement_flow)
+            (let flow = flow.then(&statement_flow)))
+      (let flow = flow.exit_block(label.as_ref().map(|label| &label.id)))
+      ----------------------------------------------------- ("block")
+      (control_flow_block(Block { label, stmts }) => flow)
+    )
+  }
+}
+
+judgment_fn! {
+  /// Computes the control flow that can emerge from a statement.
+  fn control_flow_stmt( stmt: Stmt) => ControlFlow {
+    debug(stmt)
+
+    (
+      (let flow = ControlFlow::returns())
+      ----------------------------------------------------- ("return")
+      (control_flow_stmt(Stmt::Return { expr: _ }) => flow)
+    )
+
+    (
+      (let flow = ControlFlow::break_to(label.clone()))
+      ----------------------------------------------------- ("break")
+      (control_flow_stmt(Stmt::Break { label }) => flow)
+    )
+
+    (
+      (let flow = ControlFlow::continue_to(label.clone()))
+      ----------------------------------------------------- ("continue")
+      (control_flow_stmt(Stmt::Continue { label }) => flow)
+    )
+
+    (
+      (let flow = ControlFlow::fallthrough())
+      ----------------------------------------------------- ("expression")
+      (control_flow_stmt(Stmt::Expr { expr: _ }) => flow)
+    )
+
+    (
+      (let flow = ControlFlow::fallthrough())
+      ----------------------------------------------------- ("print")
+      (control_flow_stmt(Stmt::Print { expr: _ }) => flow)
+    )
+
+    (
+      (let flow = ControlFlow::fallthrough())
+      ----------------------------------------------------- ("let")
+      (control_flow_stmt(Stmt::Let { label: _, id: _, ty: _, init: _ }) => flow)
+    )
+
+    (
+      (control_flow_block(block) => flow)
+      ----------------------------------------------------- ("block")
+      (control_flow_stmt(Stmt::Block(block)) => flow)
+    )
+
+    (
+      (control_flow_block(then_block) => then_flow)
+      (control_flow_block(&else_block.block) => else_flow)
+      (let flow = then_flow.join(else_flow))
+      ----------------------------------------------------- ("if")
+      (control_flow_stmt(Stmt::If { condition: _, then_block, else_block }) => flow)
+    )
+
+    (
+      (control_flow_block(body) => body_flow)
+      (let flow = body_flow.exit_loop(label.as_ref().map(|label| &label.id)))
+      ----------------------------------------------------- ("loop")
+      (control_flow_stmt(Stmt::Loop { label, body}) => flow)
+    )
+
+    (
+      (let block = binder.peek())
+      (control_flow_block(block) => flow)
+      ----------------------------------------------------- ("exists")
+      (control_flow_stmt(Stmt::Exists { binder }) => flow)
+    )
+  }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::grammar::expr::Expr;
+
+    #[test]
+    fn then_ignores_unreachable_breaks() {
+        let returned = ControlFlow::returns();
+        let unreachable_break = ControlFlow::break_to(LabelId::new("'break"));
+
+        let result = returned.then(&unreachable_break);
+
+        assert!(!result.can_fall_through);
+        assert!(result.breaks.is_empty());
+        assert!(result.continues.is_empty());
+    }
+
+    #[test]
+    fn then_preserves_reachable_breaks() {
+        let label = LabelId::new("'rb");
+        let fallthrough = ControlFlow::fallthrough();
+        let break_flow = ControlFlow::break_to(label.clone());
+
+        let result = fallthrough.then(&break_flow);
+
+        assert!(!result.can_fall_through);
+        assert!(result.breaks.contains(&label));
+        assert!(result.continues.is_empty());
+    }
+
+    #[test]
+    fn then_ignores_unreachable_continues() {
+        let returned = ControlFlow::returns();
+        let unreachable_continue = ControlFlow::continue_to(LabelId::new("'cont"));
+
+        let result = returned.then(&unreachable_continue);
+
+        assert!(!result.can_fall_through);
+        assert!(result.breaks.is_empty());
+        assert!(result.continues.is_empty());
+    }
+
+    #[test]
+    fn join_unions_break_and_continue_targets_from_both_branches() {
+        let break_label = LabelId::new("'bl");
+        let break_flow = ControlFlow::break_to(break_label.clone());
+        let continue_label = LabelId::new("'cl");
+        let continue_flow = ControlFlow::continue_to(continue_label.clone());
+
+        let result = break_flow.join(&continue_flow);
+
+        assert!(!result.can_fall_through);
+        assert!(result.breaks.contains(&break_label));
+        assert!(result.continues.contains(&continue_label));
+    }
+
+    #[test]
+    fn join_allows_fallthrough_when_either_branch_falls_through() {
+        let label = LabelId::new("'jb");
+        let break_flow = ControlFlow::break_to(label.clone());
+        let fallthrough = ControlFlow::fallthrough();
+
+        let result = fallthrough.join(&break_flow);
+
+        assert!(result.can_fall_through);
+        assert!(result.breaks.contains(&label));
+        assert!(result.continues.is_empty());
+    }
+
+    #[test]
+    fn matching_break_exits_block() {
+        let break_label = LabelId::new("'bl");
+        let break_flow = ControlFlow::break_to(break_label.clone());
+
+        let result = break_flow.exit_block(Some(&break_label));
+
+        assert!(result.can_fall_through);
+        assert!(result.breaks.is_empty());
+        assert!(result.continues.is_empty());
+    }
+
+    #[test]
+    fn continues_propagate_through_block() {
+        let block_label = LabelId::new("'inner");
+        let continue_label = LabelId::new("'outer");
+        let continue_flow = ControlFlow::continue_to(continue_label.clone());
+
+        let result = continue_flow.exit_block(Some(&block_label));
+
+        assert!(!result.can_fall_through);
+        assert!(result.breaks.is_empty());
+        assert!(result.continues.contains(&continue_label));
+    }
+
+    #[test]
+    fn matching_break_does_exit_loop() {
+        let break_label = LabelId::new("'bl");
+        let break_flow = ControlFlow::break_to(break_label.clone());
+
+        let result = break_flow.exit_loop(Some(&break_label));
+
+        assert!(result.can_fall_through);
+        assert!(result.breaks.is_empty());
+        assert!(result.continues.is_empty());
+    }
+
+    #[test]
+    fn matching_continue_does_not_exit_loop() {
+        let loop_label = LabelId::new("'inner");
+        let continue_flow = ControlFlow::continue_to(loop_label.clone());
+
+        let result = continue_flow.exit_loop(Some(&loop_label));
+
+        assert!(!result.can_fall_through);
+        assert!(result.breaks.is_empty());
+        assert!(result.continues.is_empty());
+    }
+
+    #[test]
+    fn non_matching_break_propagates_through_blocks() {
+        let block_label = LabelId::new("'inner");
+        let break_label = LabelId::new("'outer");
+        let break_flow = ControlFlow::break_to(break_label.clone());
+
+        let result = break_flow.exit_block(Some(&block_label));
+
+        assert!(!result.can_fall_through);
+        assert!(result.breaks.contains(&break_label));
+        assert!(result.continues.is_empty());
+    }
+
+    #[test]
+    fn body_fallthrough_does_not_exit_loop() {
+        let block_label = LabelId::new("'loop");
+        let fallthrough = ControlFlow::fallthrough();
+
+        let result = fallthrough.exit_loop(Some(&block_label));
+
+        assert!(!result.can_fall_through);
+        assert!(result.breaks.is_empty());
+        assert!(result.continues.is_empty());
+    }
+
+    #[test]
+    fn break_targeting_outer_label_propagates_through_inner_loop() {
+        let loop_label = LabelId::new("'inner");
+        let break_label = LabelId::new("'outer");
+        let break_flow = ControlFlow::break_to(break_label.clone());
+
+        let result = break_flow.exit_loop(Some(&loop_label));
+
+        assert!(!result.can_fall_through);
+        assert!(result.breaks.contains(&break_label));
+        assert!(result.continues.is_empty());
+    }
+
+    #[test]
+    fn continues_targeting_outer_label_propagates_through_inner_loop() {
+        let loop_label = LabelId::new("'inner");
+        let continue_label = LabelId::new("'outer");
+        let continue_flow = ControlFlow::continue_to(continue_label.clone());
+
+        let result = continue_flow.exit_loop(Some(&loop_label));
+
+        assert!(!result.can_fall_through);
+        assert!(result.breaks.is_empty());
+        assert!(result.continues.contains(&continue_label));
+    }
+
+    #[test]
+    fn return_statement_does_not_fall_through() {
+        let stmt = Stmt::Return { expr: Expr::True };
+
+        let (flow, _) = control_flow_stmt(stmt)
+            .into_singleton()
+            .expect("return statement should produce one control flow");
+
+        assert!(!flow.can_fall_through);
+        assert!(flow.breaks.is_empty());
+        assert!(flow.continues.is_empty());
+    }
+
+    #[test]
+    fn break_statement_records_its_target() {
+        let label = LabelId::new("'block");
+        let stmt = Stmt::Break {
+            label: label.clone(),
+        };
+
+        let (flow, _) = control_flow_stmt(stmt)
+            .into_singleton()
+            .expect("break statement should produce one control flow");
+
+        assert!(!flow.can_fall_through);
+        assert_eq!(flow.breaks.len(), 1);
+        assert!(flow.breaks.contains(&label));
+        assert!(flow.continues.is_empty());
+    }
+
+    #[test]
+    fn continue_statement_records_its_target() {
+        let label = LabelId::new("'block");
+        let stmt = Stmt::Continue {
+            label: label.clone(),
+        };
+
+        let (flow, _) = control_flow_stmt(stmt)
+            .into_singleton()
+            .expect("continue statement should produce one control flow");
+
+        assert!(!flow.can_fall_through);
+        assert!(flow.breaks.is_empty());
+        assert_eq!(flow.continues.len(), 1);
+        assert!(flow.continues.contains(&label));
+    }
+
+    #[test]
+    fn expression_statement_can_fall_through() {
+        let stmt = Stmt::Expr { expr: Expr::True };
+
+        let (flow, _) = control_flow_stmt(stmt)
+            .into_singleton()
+            .expect("expression statements should produce one control-flow result");
+
+        assert!(flow.can_fall_through);
+        assert!(flow.breaks.is_empty());
+        assert!(flow.continues.is_empty());
+    }
+
+    #[test]
+    fn print_statement_can_fall_through() {
+        let stmt = Stmt::Print { expr: Expr::True };
+
+        let (flow, _) = control_flow_stmt(stmt)
+            .into_singleton()
+            .expect("print statements should produce one control-flow result");
+
+        assert!(flow.can_fall_through);
+        assert!(flow.breaks.is_empty());
+        assert!(flow.continues.is_empty());
+    }
+
+    #[test]
+    fn let_statement_can_fall_through() {
+        let stmt: Stmt = crate::rust::term("let x: bool;");
+
+        let (flow, _) = control_flow_stmt(stmt)
+            .into_singleton()
+            .expect("let statements should produce one control-flow result");
+
+        assert!(flow.can_fall_through);
+        assert!(flow.breaks.is_empty());
+        assert!(flow.continues.is_empty());
+    }
+
+    #[test]
+    fn empty_block_can_fall_through() {
+        let (flow, _) = control_flow_block(Block::empty())
+            .into_singleton()
+            .expect("empty block should produce one control-flow result");
+
+        assert!(flow.can_fall_through);
+        assert!(flow.breaks.is_empty());
+        assert!(flow.continues.is_empty());
+    }
+
+    #[test]
+    fn return_after_fall_through_prevents_block_fall_through() {
+        let block = Block {
+            label: None,
+            stmts: vec![
+                Stmt::Expr { expr: Expr::True },
+                Stmt::Return { expr: Expr::True },
+                Stmt::Break {
+                    label: LabelId::new("'test"),
+                },
+            ],
+        };
+
+        let (flow, _) = control_flow_block(block)
+            .into_singleton()
+            .expect("block should produce one control-flow result");
+
+        assert!(!flow.can_fall_through);
+        assert!(flow.breaks.is_empty());
+        assert!(flow.continues.is_empty());
+    }
+
+    #[test]
+    fn matching_break_makes_labeled_block_fall_through() {
+        let block: Block = crate::rust::term(
+            "'block: {
+            break 'block;
+          }",
+        );
+
+        let (flow, _) = control_flow_block(block)
+            .into_singleton()
+            .expect("labeled block should produce one control-flow result");
+
+        assert!(flow.can_fall_through);
+        assert!(flow.breaks.is_empty());
+        assert!(flow.continues.is_empty());
+    }
+
+    #[test]
+    fn nested_block_propagates_return_flow() {
+        let stmt = Stmt::Block(Block {
+            label: None,
+            stmts: vec![Stmt::Return { expr: Expr::True }],
+        });
+
+        let (flow, _) = control_flow_stmt(stmt)
+            .into_singleton()
+            .expect("nested block should produce one control-flow result");
+
+        assert!(!flow.can_fall_through);
+        assert!(flow.breaks.is_empty());
+        assert!(flow.continues.is_empty());
+    }
+
+    #[test]
+    fn if_with_two_returning_branches_does_not_fall_through() {
+        let stmt: Stmt = crate::rust::term(
+            " if true {
+            return true;
+          } else {
+            return false;
+          }
+        ",
+        );
+
+        let (flow, _) = control_flow_stmt(stmt)
+            .into_singleton()
+            .expect("if statement should produce one control-flow result");
+
+        assert!(!flow.can_fall_through);
+        assert!(flow.breaks.is_empty());
+        assert!(flow.continues.is_empty());
+    }
+
+    #[test]
+    fn if_without_an_else_branch_fall_through() {
+        let stmt: Stmt = crate::rust::term(
+            "if true {
+            return true;
+        }",
+        );
+
+        let (flow, _) = control_flow_stmt(stmt)
+            .into_singleton()
+            .expect("if statement should produce one control-flow result");
+
+        assert!(flow.can_fall_through);
+        assert!(flow.breaks.is_empty());
+        assert!(flow.continues.is_empty());
+    }
+
+    #[test]
+    fn loop_with_fallthrough_body_does_not_fall_through() {
+        let stmt: Stmt = crate::rust::term(
+            "loop {
+              true;
+            }",
+        );
+
+        let (flow, _) = control_flow_stmt(stmt)
+            .into_singleton()
+            .expect("loop statement should produce one control-flow result");
+
+        assert!(!flow.can_fall_through);
+        assert!(flow.breaks.is_empty());
+        assert!(flow.continues.is_empty());
+    }
+
+    #[test]
+    fn matching_break_makes_loop_fall_through() {
+        let stmt: Stmt = crate::rust::term(
+            "'outer: loop {
+            break 'outer;
+          }",
+        );
+
+        let (flow, _) = control_flow_stmt(stmt)
+            .into_singleton()
+            .expect("loop statement should produce one control-flow result");
+
+        assert!(flow.can_fall_through);
+        assert!(flow.breaks.is_empty());
+        assert!(flow.continues.is_empty());
+    }
+
+    #[test]
+    fn exists_statement_propagates_inner_return() {
+        let stmt: Stmt = crate::rust::term(
+            "exists<'r> {
+              return true;
+            }",
+        );
+
+        let (flow, _) = control_flow_stmt(stmt)
+            .into_singleton()
+            .expect("exists statement should produce one control-flow result");
+
+        assert!(!flow.can_fall_through);
+        assert!(flow.breaks.is_empty());
+        assert!(flow.continues.is_empty());
+    }
+
+    #[test]
+    fn unit_returning_function_may_fall_through() {
+        check_fn_returns(Ty::unit(), Block::empty())
+            .into_singleton()
+            .expect("unit-returning functions should be allowed to fall through");
+    }
+
+    #[test]
+    fn non_unit_function_with_return_is_accepted() {
+        let block: Block = crate::rust::term(
+            " {
+            return true;
+        }",
+        );
+
+        check_fn_returns(Ty::bool(), block)
+            .into_singleton()
+            .expect("non-unit returning functions should not be allowed to fall through");
+    }
+
+    #[test]
+    fn non_unit_function_that_can_fall_through_is_rejected() {
+        check_fn_returns(Ty::bool(), Block::empty())
+            .into_singleton()
+            .expect_err("non-unit returning function that can fall through should be rejected.");
+    }
+}
diff --git a/tests/return_validation.rs b/tests/return_validation.rs
index c919ca2d3..814143d94 100644
--- a/tests/return_validation.rs
+++ b/tests/return_validation.rs
@@ -1,6 +1,6 @@
 use a_mir_formality::{crates, FormalityTest};
 
-/// Tests for issue #209: ensuring functions return a value on all paths.
+/// Tests for issues #209 and #392: ensuring functions return a value on all paths.
 ///
 /// These tests verify that a-mir-formality matches rustc's behavior
 /// for return validation. All error cases have been verified against
@@ -10,14 +10,17 @@ use a_mir_formality::{crates, FormalityTest};
 /// should be an error — no value is returned.
 /// rustc: "implicitly returns `()` as its body has no tail or `return` expression"
 #[test]
-#[ignore = "needs return validation (#209)"]
 fn empty_body_non_unit_return() {
     FormalityTest::new(crates![crate Foo {
         fn foo() -> u32 {
         }
     }])
-    .rustc_err(expect_test::expect![[r#""#]])
-    .err(expect_test::expect![[r#"function may not return a value"#]])
+    .err(expect_test::expect![[r#"
+        the rule "non-unit return" at (return_check.rs) failed because
+          function may not return a value
+
+        the rule "unit" at (return_check.rs) failed because
+          condition evaluated to false: `output_ty == &Ty::unit()`"#]])
 }
 
 /// A function returning () with an empty body is fine — unit is implicit.
@@ -55,7 +58,6 @@ fn if_else_both_branches_return() {
 /// without returning, so this should be an error.
 /// rustc: "expected `u32`, found `()`"
 #[test]
-#[ignore = "needs return validation (#209)"]
 fn if_else_one_branch_returns() {
     FormalityTest::new(crates![crate Foo {
         fn foo(b: bool) -> u32 {
@@ -65,8 +67,12 @@ fn if_else_one_branch_returns() {
             }
         }
     }])
-    .rustc_err(expect_test::expect![[r#""#]])
-    .err(expect_test::expect![[r#"function may not return a value"#]])
+    .err(expect_test::expect![[r#"
+        the rule "non-unit return" at (return_check.rs) failed because
+          function may not return a value
+
+        the rule "unit" at (return_check.rs) failed because
+          condition evaluated to false: `output_ty == &Ty::unit()`"#]])
 }
 
 /// An infinite loop never terminates, so it never needs to return.
@@ -88,7 +94,6 @@ fn infinite_loop_no_return_needed() {
 /// This should be an error.
 /// rustc: "expected `u32`, found `()`"
 #[test]
-#[ignore = "needs return validation (#209)"]
 fn loop_with_break_no_return() {
     FormalityTest::new(crates![crate Foo {
         fn foo() -> u32 {
@@ -97,8 +102,12 @@ fn loop_with_break_no_return() {
             }
         }
     }])
-    .rustc_err(expect_test::expect![[r#""#]])
-    .err(expect_test::expect![[r#"function may not return a value"#]])
+    .err(expect_test::expect![[r#"
+        the rule "non-unit return" at (return_check.rs) failed because
+          function may not return a value
+
+        the rule "unit" at (return_check.rs) failed because
+          condition evaluated to false: `output_ty == &Ty::unit()`"#]])
 }
 
 /// A loop with break followed by a return is fine — all paths return.
@@ -131,3 +140,107 @@ fn simple_return() {
     .rustc_ok()
     .ok()
 }
+
+/// A break in dead code must not make the loop exit reachable.
+#[test]
+fn unreachable_break_after_return_does_not_revive_loop_exit() {
+    FormalityTest::new(crates![crate Foo {
+        fn foo() -> u32 {
+            'a: loop {
+                return 1_u32;
+                break 'a;
+            }
+        }
+    }])
+    .skip_execute()
+    .ok()
+}
+
+/// A reachable break on one branch means the loop can fall through.
+#[test]
+fn loop_with_conditional_break_can_fall_through() {
+    FormalityTest::new(crates![crate Foo {
+        fn foo(b: bool) -> u32 {
+            'a: loop {
+                if b {
+                    return 1_u32;
+                } else {
+                    break 'a;
+                }
+            }
+        }
+    }])
+    .err(expect_test::expect![[r#"
+        the rule "non-unit return" at (return_check.rs) failed because
+          function may not return a value
+
+        the rule "unit" at (return_check.rs) failed because
+          condition evaluated to false: `output_ty == &Ty::unit()`"#]])
+}
+
+#[test]
+fn if_without_else_is_rejected_for_non_unit_function() {
+    FormalityTest::new(crates![crate Foo {
+      fn foo(a: bool) -> u32 {
+        if a {
+          return 1_u32;
+        }
+      }
+    }])
+    .err(expect_test::expect![[r#"
+        the rule "non-unit return" at (return_check.rs) failed because
+          function may not return a value
+
+        the rule "unit" at (return_check.rs) failed because
+          condition evaluated to false: `output_ty == &Ty::unit()`"#]])
+}
+
+#[test]
+fn loop_with_matching_continue_does_not_fall_through() {
+    FormalityTest::new(crates![crate Foo {
+      fn foo(a: bool) -> u32 {
+        'a: loop {
+          continue 'a;
+        }
+      }
+    }])
+    .skip_execute()
+    .rustc_ok()
+    .ok();
+}
+
+/// A break targeting an outer block propagates through the inner loop
+/// and makes execution continue after the outer block.
+#[test]
+fn break_targeting_outer_block_makes_fall_through() {
+    FormalityTest::new(crates![crate Foo {
+      fn foo() -> u32 {
+        'outer: {
+          'inner: loop {
+            break 'outer;
+          }
+        }
+      }
+    }])
+    .err(expect_test::expect![[r#"
+        the rule "non-unit return" at (return_check.rs) failed because
+          function may not return a value
+
+        the rule "unit" at (return_check.rs) failed because
+          condition evaluated to false: `output_ty == &Ty::unit()`"#]])
+}
+
+#[test]
+fn exists_with_return_is_accepted() {
+    FormalityTest::new(crates![crate Foo {
+      fn foo() -> i32 {
+
+       exists<'a> {
+          return 1_i32;
+       }
+     }
+    }])
+    .skip_execute()
+    .rustc_ok()
+    .ok();
+}