diff --git a/src/mir/control_tree/normalized_shadow/builder.rs b/src/mir/control_tree/normalized_shadow/builder.rs
index 7cf47fde..aacef7f6 100644
--- a/src/mir/control_tree/normalized_shadow/builder.rs
+++ b/src/mir/control_tree/normalized_shadow/builder.rs
@@ -11,6 +11,7 @@ use crate::mir::control_tree::normalized_shadow::env_layout::{
     expected_env_field_count as calc_expected_env_fields, EnvLayout,
 };
 use crate::mir::control_tree::normalized_shadow::if_as_last_join_k::IfAsLastJoinKLowererBox;
+use crate::mir::control_tree::normalized_shadow::loop_true_break_once::LoopTrueBreakOnceBuilderBox; // Phase 131
 use crate::mir::control_tree::normalized_shadow::post_if_post_k::PostIfPostKBuilderBox; // Phase 129-C
 use crate::mir::control_tree::normalized_shadow::legacy::LegacyLowerer;
 use crate::mir::control_tree::step_tree::StepTree;
@@ -40,9 +41,11 @@ impl StepTreeNormalizedShadowLowererBox {
 
     /// Try to lower an if-only StepTree to normalized form
     ///
-    /// - `Ok(None)`: Out of scope (e.g., contains loops)
+    /// - `Ok(None)`: Out of scope (e.g., contains unsupported constructs)
     /// - `Ok(Some(...))`: Shadow generation succeeded
     /// - `Err(...)`: Should be supported but conversion failed (internal error)
+    ///
+    /// Phase 131: Also supports loop(true) break-once pattern
     pub fn try_lower_if_only(
         step_tree: &StepTree,
         available_inputs: &BTreeMap<String, ValueId>,
@@ -50,9 +53,13 @@ impl StepTreeNormalizedShadowLowererBox {
         let capability = check_if_only(step_tree);
         match capability {
             CapabilityCheckResult::Supported => {
+                // If-only path
                 Self::lower_if_only_to_normalized(step_tree, available_inputs)
             }
-            CapabilityCheckResult::Unsupported(_reason) => Ok(None),
+            CapabilityCheckResult::Unsupported(_reason) => {
+                // Phase 131: Try loop(true) break-once pattern
+                Self::lower_with_loop_support(step_tree, available_inputs)
+            }
         }
     }
 
@@ -78,6 +85,23 @@ impl StepTreeNormalizedShadowLowererBox {
         LegacyLowerer::lower_if_only_to_normalized(step_tree, &env_layout)
     }
 
+    /// Phase 131: Lower StepTree with loop support (loop(true) break-once only)
+    fn lower_with_loop_support(
+        step_tree: &StepTree,
+        available_inputs: &BTreeMap<String, ValueId>,
+    ) -> Result<Option<(JoinModule, JoinFragmentMeta)>, String> {
+        // Phase 126: EnvLayout 生成（available_inputs を使用）
+        let env_layout = EnvLayout::from_contract(&step_tree.contract, available_inputs);
+
+        // Phase 131: loop(true) break-once pattern
+        if let Some((module, meta)) = LoopTrueBreakOnceBuilderBox::lower(step_tree, &env_layout)? {
+            return Ok(Some((module, meta)));
+        }
+
+        // Not supported: fall back to legacy (returns Ok(None))
+        Ok(None)
+    }
+
     /// Dev log helper for out-of-scope cases
     pub fn get_status_string(step_tree: &StepTree) -> String {
         format!(
diff --git a/src/mir/control_tree/normalized_shadow/loop_true_break_once.rs b/src/mir/control_tree/normalized_shadow/loop_true_break_once.rs
new file mode 100644
index 00000000..6d2a5ce4
--- /dev/null
+++ b/src/mir/control_tree/normalized_shadow/loop_true_break_once.rs
@@ -0,0 +1,396 @@
+//! Phase 131 P0: loop(true) break-once Normalized lowering
+//!
+//! ## Responsibility
+//!
+//! - Lower `loop(true) { <assign>* ; break }` to Normalized JoinModule
+//! - One-time execution loop (condition is always true, breaks immediately)
+//! - PHI-free: all state passing via env arguments + continuations
+//!
+//! ## Contract
+//!
+//! - Input: StepTree with loop(true) { body ; break } pattern
+//! - Output: JoinModule with:
+//!   - main(env) → TailCall(loop_step, env)
+//!   - loop_step(env) → if true { TailCall(loop_body, env) } else { TailCall(k_exit, env) }
+//!   - loop_body(env) → <assign statements update env> → TailCall(k_exit, env)
+//!   - k_exit(env) → Ret(env[x]) or TailCall(post_k, env)
+//!
+//! ## Scope
+//!
+//! - Condition: Bool literal `true` only
+//! - Body: Assign(int literal/var/add) + LocalDecl only (Phase 130 baseline)
+//! - Exit: Break at end of body only (no continue, no return in body)
+//! - Post-loop: Simple return only (Phase 124-126 baseline)
+//!
+//! ## Fail-Fast
+//!
+//! - Out of scope → Ok(None) (fallback to legacy)
+//! - In scope but conversion failed → Err (with freeze_with_hint in strict mode)
+
+use super::env_layout::EnvLayout;
+use super::legacy::LegacyLowerer;
+use crate::ast::{ASTNode, LiteralValue};
+use crate::mir::control_tree::step_tree::{StepNode, StepStmtKind, StepTree};
+use crate::mir::join_ir::lowering::carrier_info::JoinFragmentMeta;
+use crate::mir::join_ir::lowering::error_tags;
+use crate::mir::join_ir::{ConstValue, JoinFunction, JoinFuncId, JoinInst, JoinModule, MirLikeInst};
+use crate::mir::ValueId;
+use std::collections::BTreeMap;
+
+/// Box-First: loop(true) break-once lowering to Normalized
+pub struct LoopTrueBreakOnceBuilderBox;
+
+impl LoopTrueBreakOnceBuilderBox {
+    /// Try to lower loop(true) break-once pattern to Normalized JoinModule.
+    ///
+    /// Returns:
+    /// - Ok(Some((module, meta))): Successfully lowered
+    /// - Ok(None): Out of scope (fallback to legacy)
+    /// - Err(msg): In scope but failed (internal error)
+    pub fn lower(
+        step_tree: &StepTree,
+        env_layout: &EnvLayout,
+    ) -> Result<Option<(JoinModule, JoinFragmentMeta)>, String> {
+        // Extract loop(true) pattern from root
+        let (prefix_nodes, loop_node, post_nodes) = match Self::extract_loop_true_pattern(&step_tree.root) {
+            Some(v) => v,
+            None => return Ok(None), // Not a loop(true) pattern
+        };
+
+        // Verify condition is Bool(true)
+        let (cond_ast, body_node) = match loop_node {
+            StepNode::Loop { cond_ast, body, .. } => (cond_ast, body.as_ref()),
+            _ => return Ok(None),
+        };
+
+        if !Self::is_bool_true_literal(&cond_ast.0) {
+            return Ok(None); // Condition is not Bool(true)
+        }
+
+        // Verify body ends with break
+        let body_stmts = match body_node {
+            StepNode::Block(stmts) => stmts,
+            _ => return Ok(None), // Body is not a block
+        };
+
+        if !Self::body_ends_with_break(body_stmts) {
+            return Ok(None); // Body doesn't end with break
+        }
+
+        // Extract body statements (excluding final break)
+        let body_prefix = &body_stmts[..body_stmts.len() - 1];
+
+        // Verify no return/continue in body
+        if Self::has_unsupported_exits(body_prefix) {
+            return Ok(None);
+        }
+
+        let env_fields = env_layout.env_fields();
+
+        fn alloc_value_id(next_value_id: &mut u32) -> ValueId {
+            let vid = ValueId(*next_value_id);
+            *next_value_id += 1;
+            vid
+        }
+
+        let alloc_env_params =
+            |fields: &[String], next_value_id: &mut u32| -> Vec<ValueId> {
+                fields
+                    .iter()
+                    .map(|_| alloc_value_id(next_value_id))
+                    .collect()
+            };
+
+        let build_env_map = |fields: &[String], params: &[ValueId]| -> BTreeMap<String, ValueId> {
+            let mut env = BTreeMap::new();
+            for (name, vid) in fields.iter().zip(params.iter()) {
+                env.insert(name.clone(), *vid);
+            }
+            env
+        };
+
+        let collect_env_args = |fields: &[String], env: &BTreeMap<String, ValueId>| -> Result<Vec<ValueId>, String> {
+            let mut args = Vec::with_capacity(fields.len());
+            for name in fields {
+                let vid = env.get(name).copied().ok_or_else(|| {
+                    error_tags::freeze_with_hint(
+                        "phase131/loop_true/env_missing",
+                        &format!("env missing required field '{name}'"),
+                        "ensure env layout and env map are built from the same SSOT field list",
+                    )
+                })?;
+                args.push(vid);
+            }
+            Ok(args)
+        };
+
+        let mut next_value_id: u32 = 1;
+
+        // Function IDs (stable, dev-only)
+        let main_id = JoinFuncId::new(0);
+        let loop_step_id = JoinFuncId::new(1);
+        let loop_body_id = JoinFuncId::new(2);
+        let k_exit_id = JoinFuncId::new(3);
+
+        // main(env): <prefix> → TailCall(loop_step, env)
+        let main_params = alloc_env_params(&env_fields, &mut next_value_id);
+        let mut env_main = build_env_map(&env_fields, &main_params);
+        let mut main_func = JoinFunction::new(main_id, "main".to_string(), main_params);
+
+        // Lower prefix (pre-loop) statements into main
+        for n in prefix_nodes {
+            match n {
+                StepNode::Stmt { kind, .. } => match kind {
+                    StepStmtKind::Assign { target, value_ast } => {
+                        if LegacyLowerer::lower_assign_stmt(
+                            target,
+                            value_ast,
+                            &mut main_func.body,
+                            &mut next_value_id,
+                            &mut env_main,
+                        )
+                        .is_err()
+                        {
+                            return Ok(None);
+                        }
+                    }
+                    StepStmtKind::LocalDecl { .. } => {}
+                    _ => {
+                        return Ok(None);
+                    }
+                },
+                _ => {
+                    return Ok(None);
+                }
+            }
+        }
+
+        // main → loop_step tailcall
+        let main_args = collect_env_args(&env_fields, &env_main)?;
+        main_func.body.push(JoinInst::Call {
+            func: loop_step_id,
+            args: main_args,
+            k_next: None,
+            dst: None,
+        });
+
+        // loop_step(env): if true { TailCall(loop_body, env) } else { TailCall(k_exit, env) }
+        let loop_step_params = alloc_env_params(&env_fields, &mut next_value_id);
+        let env_loop_step = build_env_map(&env_fields, &loop_step_params);
+        let mut loop_step_func = JoinFunction::new(loop_step_id, "loop_step".to_string(), loop_step_params);
+
+        // Generate condition: true
+        let cond_vid = alloc_value_id(&mut next_value_id);
+        loop_step_func.body.push(JoinInst::Compute(MirLikeInst::Const {
+            dst: cond_vid,
+            value: ConstValue::Bool(true),
+        }));
+
+        // Conditional jump: if true → loop_body, else → k_exit
+        let loop_step_args = collect_env_args(&env_fields, &env_loop_step)?;
+        loop_step_func.body.push(JoinInst::Jump {
+            cont: loop_body_id.as_cont(),
+            args: loop_step_args.clone(),
+            cond: Some(cond_vid),
+        });
+        loop_step_func.body.push(JoinInst::Jump {
+            cont: k_exit_id.as_cont(),
+            args: loop_step_args,
+            cond: None,
+        });
+
+        // loop_body(env): <assign statements> → TailCall(k_exit, env)
+        let loop_body_params = alloc_env_params(&env_fields, &mut next_value_id);
+        let mut env_loop_body = build_env_map(&env_fields, &loop_body_params);
+        let mut loop_body_func = JoinFunction::new(loop_body_id, "loop_body".to_string(), loop_body_params);
+
+        // Lower body statements
+        for n in body_prefix {
+            match n {
+                StepNode::Stmt { kind, .. } => match kind {
+                    StepStmtKind::Assign { target, value_ast } => {
+                        if LegacyLowerer::lower_assign_stmt(
+                            target,
+                            value_ast,
+                            &mut loop_body_func.body,
+                            &mut next_value_id,
+                            &mut env_loop_body,
+                        )
+                        .is_err()
+                        {
+                            return Ok(None);
+                        }
+                    }
+                    StepStmtKind::LocalDecl { .. } => {}
+                    _ => {
+                        return Ok(None);
+                    }
+                },
+                _ => {
+                    return Ok(None);
+                }
+            }
+        }
+
+        // loop_body → k_exit tailcall
+        let loop_body_args = collect_env_args(&env_fields, &env_loop_body)?;
+        loop_body_func.body.push(JoinInst::Call {
+            func: k_exit_id,
+            args: loop_body_args,
+            k_next: None,
+            dst: None,
+        });
+
+        // k_exit(env): handle post-loop or return
+        let k_exit_params = alloc_env_params(&env_fields, &mut next_value_id);
+        let env_k_exit = build_env_map(&env_fields, &k_exit_params);
+        let mut k_exit_func = JoinFunction::new(k_exit_id, "k_exit".to_string(), k_exit_params);
+
+        // Handle post-loop statements or return
+        if post_nodes.is_empty() {
+            // No post-loop: return void
+            k_exit_func.body.push(JoinInst::Ret { value: None });
+        } else if post_nodes.len() == 1 {
+            // Single post statement: check if it's a return
+            match &post_nodes[0] {
+                StepNode::Stmt { kind, .. } => match kind {
+                    StepStmtKind::Return { value_ast } => {
+                        if let Some(ast_handle) = value_ast {
+                            // Return variable from env
+                            if let Some(var_name) = Self::extract_variable_name(&ast_handle.0) {
+                                if let Some(vid) = env_k_exit.get(&var_name).copied() {
+                                    k_exit_func.body.push(JoinInst::Ret { value: Some(vid) });
+                                } else {
+                                    return Ok(None); // Variable not in env
+                                }
+                            } else {
+                                return Ok(None); // Return value is not a variable
+                            }
+                        } else {
+                            // Return void
+                            k_exit_func.body.push(JoinInst::Ret { value: None });
+                        }
+                    }
+                    _ => {
+                        return Ok(None); // Unsupported post statement
+                    }
+                },
+                _ => {
+                    return Ok(None);
+                }
+            }
+        } else {
+            return Ok(None); // Multiple post statements not supported
+        }
+
+        // Build module
+        let mut module = JoinModule::new();
+        module.add_function(main_func);
+        module.add_function(loop_step_func);
+        module.add_function(loop_body_func);
+        module.add_function(k_exit_func);
+        module.entry = Some(main_id);
+        module.mark_normalized();
+
+        Ok(Some((module, JoinFragmentMeta::empty())))
+    }
+
+    /// Extract loop(true) pattern from StepTree root
+    ///
+    /// Returns: (prefix_nodes, loop_node, post_nodes)
+    fn extract_loop_true_pattern(root: &StepNode) -> Option<(&[StepNode], &StepNode, &[StepNode])> {
+        match root {
+            StepNode::Loop { .. } => {
+                // Loop is the only statement
+                Some((&[][..], root, &[][..]))
+            }
+            StepNode::Block(nodes) => {
+                // Find loop in block
+                for (i, node) in nodes.iter().enumerate() {
+                    if matches!(node, StepNode::Loop { .. }) {
+                        let prefix = &nodes[..i];
+                        let post = &nodes[i + 1..];
+                        return Some((prefix, node, post));
+                    }
+                }
+                None
+            }
+            _ => None,
+        }
+    }
+
+    /// Check if AST node is Bool(true) literal
+    fn is_bool_true_literal(ast: &ASTNode) -> bool {
+        matches!(
+            ast,
+            ASTNode::Literal {
+                value: LiteralValue::Bool(true),
+                ..
+            }
+        )
+    }
+
+    /// Check if body ends with break statement
+    fn body_ends_with_break(stmts: &[StepNode]) -> bool {
+        if let Some(last) = stmts.last() {
+            matches!(
+                last,
+                StepNode::Stmt {
+                    kind: StepStmtKind::Break,
+                    ..
+                }
+            )
+        } else {
+            false
+        }
+    }
+
+    /// Check if body has unsupported exits (return/continue)
+    fn has_unsupported_exits(stmts: &[StepNode]) -> bool {
+        for stmt in stmts {
+            match stmt {
+                StepNode::Stmt { kind, .. } => match kind {
+                    StepStmtKind::Return { .. } | StepStmtKind::Continue => return true,
+                    _ => {}
+                },
+                StepNode::Block(inner) => {
+                    if Self::has_unsupported_exits(inner) {
+                        return true;
+                    }
+                }
+                StepNode::If { then_branch, else_branch, .. } => {
+                    if Self::has_unsupported_exits_in_node(then_branch) {
+                        return true;
+                    }
+                    if let Some(else_node) = else_branch {
+                        if Self::has_unsupported_exits_in_node(else_node) {
+                            return true;
+                        }
+                    }
+                }
+                _ => {}
+            }
+        }
+        false
+    }
+
+    fn has_unsupported_exits_in_node(node: &StepNode) -> bool {
+        match node {
+            StepNode::Stmt { kind, .. } => matches!(kind, StepStmtKind::Return { .. } | StepStmtKind::Continue),
+            StepNode::Block(stmts) => Self::has_unsupported_exits(stmts),
+            StepNode::If { then_branch, else_branch, .. } => {
+                Self::has_unsupported_exits_in_node(then_branch)
+                    || else_branch.as_ref().map_or(false, |n| Self::has_unsupported_exits_in_node(n))
+            }
+            _ => false,
+        }
+    }
+
+    /// Extract variable name from AST node
+    fn extract_variable_name(ast: &ASTNode) -> Option<String> {
+        match ast {
+            ASTNode::Variable { name, .. } => Some(name.clone()),
+            _ => None,
+        }
+    }
+}
diff --git a/src/mir/control_tree/normalized_shadow/mod.rs b/src/mir/control_tree/normalized_shadow/mod.rs
index 87c8bbf5..1e40c430 100644
--- a/src/mir/control_tree/normalized_shadow/mod.rs
+++ b/src/mir/control_tree/normalized_shadow/mod.rs
@@ -34,6 +34,7 @@ pub mod contracts;
 pub mod normalized_verifier;
 pub mod env_layout;
 pub mod if_as_last_join_k;
+pub mod loop_true_break_once; // Phase 131: loop(true) break-once
 pub mod post_if_post_k; // Phase 129-C: post-if with post_k continuation
 pub mod legacy;
 pub mod dev_pipeline;