diff --git a/lib/Error.ml b/lib/Error.ml
index 70835db33..152458a2a 100644
--- a/lib/Error.ml
+++ b/lib/Error.ml
@@ -36,6 +36,8 @@ and raw_error =
   | NotLowStarCast of expr
   | LibraryPointerAmbiguity of lident * expr
   | UnrecognizedCCompiler of string
+  | HoistLocalsVla of ident
+  | InitializerUnknownType of string
 
 and location =
   string
diff --git a/lib/HoistLocals.ml b/lib/HoistLocals.ml
new file mode 100644
index 000000000..a6814c918
--- /dev/null
+++ b/lib/HoistLocals.ml
@@ -0,0 +1,273 @@
+(* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
+
+(* Hoist all local variable declarations to the beginning of the function body,
+   in the order they appear, preserving comments in between.
+
+   Controlled by -fhoist-locals.
+
+   Algorithm: we walk the body of each function, collecting ELet declarations.
+
+   For a given local variable declaration, after hoisting any locals from its
+   initializer expression:
+   - If no statements other than variable declarations and comments were
+     produced (i.e. we are still in the "declaration zone" at the top of the
+     body), keep the declaration with its initializer.
+   - Otherwise, emit the declaration without its initializer (using EAny) at
+     the end of the already-produced declarations, and turn the initializer
+     into an assignment at the original location.
+
+   Special case: if a locally allocated array has a non-constant size (VLA)
+   and needs to be lifted past real statements, emit a warning (fatal by
+   default), leave the declaration in place, and continue. *)
+
+open Ast
+open Helpers
+open DeBruijn
+
+(* Does an EBufCreate have a non-constant size (VLA)? *)
+let is_vla e1 =
+  match e1.node with
+  | EBufCreate (Common.Stack, _, size) ->
+      (match size.node with EConstant _ -> false | _ -> true)
+  | _ -> false
+
+(* A hoisted item: either a local variable declaration (opened binder + its
+   initializer, or EAny if split) or a standalone comment. *)
+type hoisted =
+  | HDecl of binder * expr
+  | HComment of string
+
+(* Prepend a statement before a body, flattening into ESequence. *)
+let prepend stmt body typ =
+  match body.node with
+  | ESequence es -> { node = ESequence (stmt :: es); typ; meta = [] }
+  | _ -> { node = ESequence [stmt; body]; typ; meta = [] }
+
+(* Walk a body expression, collecting declarations to hoist.
+
+   [only_decls]: true when all preceding statements at this function level have
+   been declarations or comments, so the next declaration can keep its init.
+
+   Returns (hoisted_decls, residual_body).
+   hoisted_decls are in source order with opened binders.
+   residual_body uses EOpen references to those binders. *)
+let rec hoist ~only_decls (e: expr) : hoisted list * expr =
+  match e.node with
+
+  (* Real local variable declaration. *)
+  | ELet (b, e1, e2) when not (List.mem MetaSequence b.node.meta) ->
+      (* First, hoist any locals from the initializer. *)
+      let init_h, e1_r = hoist ~only_decls:true e1 in
+      let init_has_stmts = residual_has_stmts e1_r in
+
+      (* Open the binder for the continuation. *)
+      let b_o, e2_o = open_binder b e2 in
+
+      if only_decls && not init_has_stmts then begin
+        (* Still in the declaration zone. Keep the initializer. *)
+        let rest_h, rest_body = hoist ~only_decls:true e2_o in
+        (init_h @ [HDecl (b_o, e1_r)] @ rest_h, rest_body)
+      end else if is_vla e1 then begin
+        (* VLA: emit warning, leave the declaration in place. *)
+        Warn.(maybe_fatal_error ("", Error.HoistLocalsVla b_o.node.name));
+        let rest_h, rest_body = hoist ~only_decls:false e2_o in
+        let residual =
+          { node = ELet (b_o, e1_r, close_binder b_o rest_body);
+            typ = e.typ; meta = e.meta } in
+        (init_h @ rest_h, residual)
+      end else begin
+        match e1_r.node with
+        | EBufCreate (l, init, size) ->
+            (* Constant-size buffer: hoist the declaration with EAny init,
+               emit EBufFill at original location. *)
+            let decl_init =
+              { e1_r with node = EBufCreate (l,
+                  { node = EAny; typ = init.typ; meta = [] }, size) } in
+            let buf_ref =
+              { node = EOpen (b_o.node.name, b_o.node.atom);
+                typ = b_o.typ; meta = [] } in
+            let fill =
+              { node = EBufFill (buf_ref, init, size);
+                typ = TUnit; meta = [] } in
+            let rest_h, rest_body = hoist ~only_decls:false e2_o in
+            (init_h @ [HDecl (b_o, decl_init)] @ rest_h,
+             prepend fill rest_body e.typ)
+        | EBufCreateL (l, inits) ->
+            (* Buffer from literal list: hoist the declaration with EAny
+               elements, emit individual EBufWrite for each element at
+               original location. *)
+            let any_init = { node = EAny; typ = (List.hd inits).typ; meta = [] } in
+            let decl_init =
+              { e1_r with node = EBufCreateL (l,
+                  List.map (fun _ -> any_init) inits) } in
+            let buf_ref =
+              { node = EOpen (b_o.node.name, b_o.node.atom);
+                typ = b_o.typ; meta = [] } in
+            let writes = List.mapi (fun i ei ->
+                let idx = { node = EConstant (K.UInt32, string_of_int i);
+                            typ = TInt K.UInt32; meta = [] } in
+                { node = EBufWrite (buf_ref, idx, ei);
+                  typ = TUnit; meta = [] }
+            ) inits in
+            let rest_h, rest_body = hoist ~only_decls:false e2_o in
+            let body' = List.fold_right
+              (fun w acc -> prepend w acc e.typ) writes rest_body in
+            (init_h @ [HDecl (b_o, decl_init)] @ rest_h, body')
+        | _ ->
+            (* Non-buffer: separate declaration from initializer. *)
+            let b_mut = mark_mut b_o in
+            let decl = HDecl (b_mut,
+                         { node = EAny; typ = b_o.typ; meta = [] }) in
+            let rest_h, rest_body = hoist ~only_decls:false e2_o in
+            if e1_r.node = EAny then
+              (init_h @ [decl] @ rest_h, rest_body)
+            else
+              let assign =
+                { node = EAssign (
+                    { node = EOpen (b_o.node.name, b_o.node.atom);
+                      typ = b_o.typ; meta = [] },
+                    e1_r);
+                  typ = TUnit; meta = [] } in
+              (init_h @ [decl] @ rest_h, prepend assign rest_body e.typ)
+      end
+
+  (* Push/pop frame markers: these are structural, not real statements.
+     Hoist INSIDE the push frame: we collect declarations from e2 and
+     place them at the start of e2 (inside the ELet). *)
+  | ELet (_, { node = EPushFrame; _ }, e2) ->
+      let inner_h, inner_body = hoist ~only_decls:true e2 in
+      let inner_body = rebuild inner_h inner_body in
+      let b_seq = sequence_binding () in
+      ([], { node = ELet (b_seq,
+               { node = EPushFrame; typ = TUnit; meta = [] },
+               close_binder b_seq inner_body);
+             typ = e.typ; meta = e.meta })
+
+  (* EPopFrame at the end of a body. *)
+  | EPopFrame ->
+      ([], e)
+
+  (* MetaSequence binding whose expression is a standalone comment: in the
+     declaration zone, hoist the comment and keep collecting declarations. *)
+  | ELet (b, { node = EStandaloneComment s; _ }, e2) when only_decls ->
+      let _, e2_o = open_binder b e2 in
+      let rest_h, rest_body = hoist ~only_decls:true e2_o in
+      (HComment s :: rest_h, rest_body)
+
+  (* MetaSequence binding: a sequencing construct, not a variable declaration.
+     This marks the transition from decl zone to statement zone. *)
+  | ELet (b, e1, e2) ->
+      let _, e2_o = open_binder b e2 in
+      let rest_h, rest_body = hoist ~only_decls:false e2_o in
+      (rest_h, prepend e1 rest_body e.typ)
+
+  (* Statement sequence. *)
+  | ESequence es ->
+      hoist_seq ~only_decls e.typ e.meta es
+
+  (* In the declaration zone, hoist comments along with declarations so
+     they maintain their position relative to initialised declarations. *)
+  | EStandaloneComment s when only_decls ->
+      ([HComment s], { node = ESequence []; typ = e.typ; meta = [] })
+
+  (* Outside the declaration zone, leave comments in place. *)
+  | EStandaloneComment _ ->
+      ([], e)
+
+  (* Branching constructs: recurse into their sub-bodies to hoist any
+     local declarations up to the function level. *)
+  | EIfThenElse (e1, e2, e3) ->
+      let h2, e2' = hoist ~only_decls:false e2 in
+      let h3, e3' = hoist ~only_decls:false e3 in
+      (h2 @ h3, { e with node = EIfThenElse (e1, e2', e3') })
+
+  | ESwitch (e1, branches) ->
+      let hs, branches' = List.split (List.map (fun (c, body) ->
+        let h, body' = hoist ~only_decls:false body in
+        (h, (c, body'))
+      ) branches) in
+      (List.flatten hs, { e with node = ESwitch (e1, branches') })
+
+  | EWhile (e1, e2) ->
+      let h2, e2' = hoist ~only_decls:false e2 in
+      (h2, { e with node = EWhile (e1, e2') })
+
+  | EFor (b, e1, e2, e3, e4) ->
+      let h4, e4' = hoist ~only_decls:false e4 in
+      (h4, { e with node = EFor (b, e1, e2, e3, e4') })
+
+  | EMatch (flav, e1, branches) ->
+      let hs, branches' = List.split (List.map (fun (bs, pat, body) ->
+        let h, body' = hoist ~only_decls:false body in
+        (h, (bs, pat, body'))
+      ) branches) in
+      (List.flatten hs, { e with node = EMatch (flav, e1, branches') })
+
+  (* Any other expression is a "real statement" — nothing to hoist from it. *)
+  | _ ->
+      ([], e)
+
+(* Process a list of sequenced expressions. *)
+and hoist_seq ~only_decls typ meta = function
+  | [] -> ([], { node = ESequence []; typ; meta })
+  | [e] -> hoist ~only_decls e
+  | e :: rest ->
+      let e_h, e_r = hoist ~only_decls e in
+      let next_only = only_decls && is_decl_or_comment e in
+      let rest_h, rest_r = hoist_seq ~only_decls:next_only typ meta rest in
+      let combined = flatten_seq e_r rest_r typ meta in
+      (e_h @ rest_h, combined)
+
+(* Is this node a comment, a real variable declaration, or a push/pop frame? *)
+and is_decl_or_comment e =
+  match e.node with
+  | EStandaloneComment _ -> true
+  | EPushFrame -> true
+  | EPopFrame -> true
+  | ELet (b, _, _) when not (List.mem MetaSequence b.node.meta) -> true
+  | _ -> false
+
+(* Check whether an expression has had statements injected. *)
+and residual_has_stmts e =
+  match e.node with
+  | EAssign _ -> true
+  | ESequence es -> List.exists residual_has_stmts es
+  | ELet (b, _, _) when List.mem MetaSequence b.node.meta -> true
+  | _ -> false
+
+(* Combine two residual expressions into a flat sequence. *)
+and flatten_seq e1 e2 typ meta =
+  let es1 = match e1.node with ESequence es -> es | _ -> [e1] in
+  let es2 = match e2.node with ESequence es -> es | _ -> [e2] in
+  match es1 @ es2 with
+  | [e] -> e
+  | es -> { node = ESequence es; typ; meta }
+
+(* Rebuild: place hoisted declarations and comments at the top, then the
+   residual body.  Comments are emitted as EStandaloneComment nodes inside
+   ESequence wrappers so that AstToCStar processes them as proper statement-
+   level comments, preserving their individual identity and source order. *)
+and rebuild hoisted body =
+  List.fold_right (fun h acc ->
+    match h with
+    | HDecl (b, init) ->
+        { node = ELet (b, init, close_binder b acc);
+          typ = acc.typ; meta = [] }
+    | HComment s ->
+        let c = { node = EStandaloneComment s; typ = TUnit; meta = [] } in
+        match acc.node with
+        | ESequence es -> { acc with node = ESequence (c :: es) }
+        | _ -> { node = ESequence [c; acc]; typ = acc.typ; meta = [] }
+  ) hoisted body
+
+(* Entry point: transform all function declarations. *)
+let hoist_locals (files: files) : files =
+  (object
+    inherit [_] map
+
+    method! visit_DFunction _ cc flags n_cg n ret name binders body =
+      let hoisted, body' = hoist ~only_decls:true body in
+      let body' = rebuild hoisted body' in
+      DFunction (cc, flags, n_cg, n, ret, name, binders, body')
+  end)#visit_files () files
diff --git a/lib/InitializeLocals.ml b/lib/InitializeLocals.ml
new file mode 100644
index 000000000..18ce6bf26
--- /dev/null
+++ b/lib/InitializeLocals.ml
@@ -0,0 +1,222 @@
+(* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
+
+(** Initialize uninitialized local variable declarations with zero values.
+    Supports four modes:
+    - C23: = {} (empty initializer)
+    - C99: designated struct initializers (.field = init)
+    - C89: positional struct initializers (no .field =) *)
+
+module C = C11
+module K = Constant
+
+module SMap = Map.Make(String)
+
+type mode = C23 | C99 | C89
+
+(* A map from typedef names to their struct/union field declarations,
+   built by scanning the top-level program. *)
+type type_kind = TStruct | TUnion
+type type_map = (type_kind * C.declaration list option) SMap.t
+
+(* Extract the identifier name from a declarator. *)
+let rec name_of_declarator (d: C.declarator): string =
+  match d with
+  | Ident n -> n
+  | Pointer (_, d) | Array (_, d, _) | Function (_, d, _) -> name_of_declarator d
+
+(* Build a type map from top-level declarations: maps typedef names
+   to their struct fields (if any). *)
+let build_type_map (program: C.program): type_map =
+  List.fold_left (fun acc (df: C.declaration_or_function) ->
+    match df with
+    | Decl (_, (_, spec, _, Some Typedef, _, decl_inits)) ->
+        let name = match decl_inits with
+          | [(d, _, _)] -> Some (name_of_declarator d)
+          | _ -> None
+        in
+        begin match name, spec with
+        | Some n, Struct (_, fields) -> SMap.add n (TStruct, fields) acc
+        | Some n, Union (_, fields) -> SMap.add n (TUnion, fields) acc
+        | _ -> acc
+        end
+    | _ -> acc
+  ) SMap.empty program
+
+(* Look up a Named type in the type map. *)
+let lookup_named (tmap: type_map) (name: string): (type_kind * C.declaration list) option =
+  match SMap.find_opt name tmap with
+  | Some (kind, Some fields) -> Some (kind, fields)
+  | _ -> None
+
+(* Generate a zero initializer for a given C11 type_spec and declarator.
+   The declarator determines if we have a pointer or array wrapping. *)
+let rec zero_init_for_type (mode: mode) (tmap: type_map) (spec: C.type_spec) (decl: C.declarator): C.init =
+  match decl with
+  | Pointer (_, _) ->
+      (* Pointer type: initialize to NULL *)
+      InitExpr (Name "NULL")
+  | Array (_, inner, size) ->
+      begin match mode with
+      | C23 -> Initializer []
+      | C99 | C89 ->
+          (* Generate one element initializer based on the element type *)
+          let elem_init = zero_init_for_type mode tmap spec inner in
+          match size with
+          | Some (C.Constant (_, n)) ->
+              let count = try int_of_string n with _ -> 1 in
+              Initializer (List.init count (fun _ -> elem_init))
+          | _ ->
+              (* Unknown size: single element, C will zero-fill the rest *)
+              Initializer [elem_init]
+      end
+  | Function _ ->
+      (* Function pointer if nested *)
+      InitExpr (Name "NULL")
+  | Ident _ ->
+      (* Base case: look at the type_spec *)
+      zero_init_for_spec mode tmap spec
+
+and zero_init_for_spec (mode: mode) (tmap: type_map) (spec: C.type_spec): C.init =
+  match spec with
+  | Int w ->
+      let s = match w with
+        | K.Bool -> "false"
+        | _ -> "0"
+      in
+      InitExpr (Constant (w, s))
+  | Void ->
+      InitExpr (Constant (K.Int32, "0"))
+  | Named name ->
+      begin match mode with
+      | C23 -> Initializer []
+      | C99 | C89 ->
+          match lookup_named tmap name with
+          | Some (TStruct, fields) -> zero_init_for_fields mode tmap fields
+          | Some (TUnion, fields) -> zero_init_for_first_field mode tmap fields
+          | None ->
+              (* Scalar type aliases (bool, BOOLEAN, etc.) or truly unknown types *)
+              let is_known_scalar = match name with
+                | "bool" | "BOOLEAN" | "_Bool"
+                | "size_t" | "ptrdiff_t" | "intptr_t" | "uintptr_t"
+                | "int" | "unsigned" | "char" | "short" | "long"
+                | "int8_t" | "int16_t" | "int32_t" | "int64_t"
+                | "uint8_t" | "uint16_t" | "uint32_t" | "uint64_t"
+                | "krml_checked_int_t" -> true
+                | _ -> false
+              in
+              if is_known_scalar then
+                InitExpr (Constant (K.Int32, "0"))
+              else begin
+                Warn.maybe_fatal_error ("", Error.InitializerUnknownType name);
+                Initializer [InitExpr (Constant (K.Int32, "0"))]
+              end
+      end
+  | Struct (_, Some fields) ->
+      zero_init_for_fields mode tmap fields
+  | Struct (_, None) ->
+      Initializer [InitExpr (Constant (K.Int32, "0"))]
+  | Union (_, Some fields) ->
+      zero_init_for_first_field mode tmap fields
+  | Union (_, None) ->
+      Initializer [InitExpr (Constant (K.Int32, "0"))]
+  | Enum _ ->
+      InitExpr (Constant (K.Int32, "0"))
+
+and zero_init_for_fields (mode: mode) (tmap: type_map) (fields: C.declaration list): C.init =
+  let inits = List.concat_map (fun ((_, spec, _, _, _, decl_inits): C.declaration) ->
+    List.map (fun ((d, _, _): C.declarator_and_init) ->
+      let field_init = zero_init_for_type mode tmap spec d in
+      match mode with
+      | C99 ->
+          let field_name = name_of_declarator d in
+          C.Designated (C.Dot field_name, field_init)
+      | C89 | C23 ->
+          field_init
+    ) decl_inits
+  ) fields in
+  Initializer inits
+
+(* For unions, only initialize the first field. In C89, only the first field
+   can be initialized; in C99, we use a designator for the first field. *)
+and zero_init_for_first_field (mode: mode) (tmap: type_map) (fields: C.declaration list): C.init =
+  match fields with
+  | ((_, spec, _, _, _, decl_inits) : C.declaration) :: _ ->
+      begin match decl_inits with
+      | ((d, _, _) : C.declarator_and_init) :: _ ->
+          let field_init = zero_init_for_type mode tmap spec d in
+          let init = match mode with
+            | C99 ->
+                let field_name = name_of_declarator d in
+                C.Designated (C.Dot field_name, field_init)
+            | C89 | C23 ->
+                field_init
+          in
+          Initializer [init]
+      | [] -> Initializer [InitExpr (Constant (K.Int32, "0"))]
+      end
+  | [] -> Initializer [InitExpr (Constant (K.Int32, "0"))]
+
+(* The top-level zero initializer for a given mode. *)
+let zero_init (mode: mode) (tmap: type_map) (spec: C.type_spec) (decl: C.declarator): C.init =
+  match mode with
+  | C23 -> Initializer []
+  | C99 | C89 -> zero_init_for_type mode tmap spec decl
+
+let init_decl_inits (mode: mode) (tmap: type_map) (spec: C.type_spec) (decl_inits: C.declarator_and_inits): C.declarator_and_inits =
+  List.map (fun ((d, align, init): C.declarator_and_init) ->
+    match init with
+    | None ->
+        let needs_init = match d with
+          | Function _ -> false
+          | _ -> true
+        in
+        if needs_init then (d, align, Some (zero_init mode tmap spec d))
+        else (d, align, init)
+    | Some _ -> (d, align, init)
+  ) decl_inits
+
+let rec initialize_stmt (mode: mode) (tmap: type_map) (s: C.stmt): C.stmt =
+  match s with
+  | C.Compound stmts -> C.Compound (List.map (initialize_stmt mode tmap) stmts)
+  | Decl (qs, spec, inline, stor, extra, decl_inits) ->
+      Decl (qs, spec, inline, stor, extra, init_decl_inits mode tmap spec decl_inits)
+  | If (e, s) -> If (e, initialize_stmt mode tmap s)
+  | IfElse (e, s1, s2) -> IfElse (e, initialize_stmt mode tmap s1, initialize_stmt mode tmap s2)
+  | IfDef (e, ss1, elifs, ss2) ->
+      IfDef (e,
+        List.map (initialize_stmt mode tmap) ss1,
+        List.map (fun (e, ss) -> (e, List.map (initialize_stmt mode tmap) ss)) elifs,
+        List.map (initialize_stmt mode tmap) ss2)
+  | While (e, s) -> While (e, initialize_stmt mode tmap s)
+  | For (de, e1, e2, s) ->
+      let de = match de with
+        | `Decl (qs, spec, inline, stor, extra, decl_inits) ->
+            `Decl (qs, spec, inline, stor, extra, init_decl_inits mode tmap spec decl_inits)
+        | other -> other
+      in
+      For (de, e1, e2, initialize_stmt mode tmap s)
+  | Switch (e, cases, default) ->
+      Switch (e,
+        List.map (fun (e, s) -> (e, initialize_stmt mode tmap s)) cases,
+        initialize_stmt mode tmap default)
+  | _ -> s
+
+let initialize_files (mode: mode) (headers: (string * C.header) list) (files: (string * C.program) list): (string * C.program) list =
+  (* Build a global type map from all files and headers *)
+  let tmap = List.fold_left (fun acc (_, program) ->
+    SMap.union (fun _ _ v -> Some v) acc (build_type_map program)
+  ) SMap.empty files in
+  let tmap = List.fold_left (fun acc (_, header) ->
+    let program = match header with C.Public p | C.Internal p -> p in
+    SMap.union (fun _ _ v -> Some v) acc (build_type_map program)
+  ) tmap headers in
+  List.map (fun (name, program) ->
+    let program = List.map (fun (df: C.declaration_or_function) ->
+      match df with
+      | Function (comments, decl, body) ->
+          (Function (comments, decl, initialize_stmt mode tmap body) : C.declaration_or_function)
+      | other -> other
+    ) program in
+    (name, program)
+  ) files
diff --git a/lib/MarkMaybeUnused.ml b/lib/MarkMaybeUnused.ml
new file mode 100644
index 000000000..1f52bc33c
--- /dev/null
+++ b/lib/MarkMaybeUnused.ml
@@ -0,0 +1,193 @@
+(* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
+
+(** Mark hoisted local variable declarations as maybe_unused when they appear
+    before #if/#ifdef blocks and are not referenced in all branches. *)
+
+module C = C11
+module SSet = Set.Make(String)
+
+(* Collect all variable names referenced in a C11 expression. *)
+let rec vars_of_expr (e: C.expr): SSet.t =
+  match e with
+  | C.Name n -> SSet.singleton n
+  | C.Op1 (_, e) -> vars_of_expr e
+  | C.Op2 (_, e1, e2) -> SSet.union (vars_of_expr e1) (vars_of_expr e2)
+  | C.Index (e1, e2) -> SSet.union (vars_of_expr e1) (vars_of_expr e2)
+  | C.Deref e -> vars_of_expr e
+  | C.Address e -> vars_of_expr e
+  | C.Member (e1, e2) -> SSet.union (vars_of_expr e1) (vars_of_expr e2)
+  | C.MemberP (e1, e2) -> SSet.union (vars_of_expr e1) (vars_of_expr e2)
+  | C.Assign (e1, e2) -> SSet.union (vars_of_expr e1) (vars_of_expr e2)
+  | C.Call (e, es) ->
+      List.fold_left (fun acc e -> SSet.union acc (vars_of_expr e))
+        (vars_of_expr e) es
+  | C.Cast (_, e) -> vars_of_expr e
+  | C.Literal _ | C.Constant _ | C.Bool _ -> SSet.empty
+  | C.Sizeof e -> vars_of_expr e
+  | C.CompoundLiteral (_, inits) -> vars_of_inits inits
+  | C.MemberAccess (e, _) -> vars_of_expr e
+  | C.MemberAccessPointer (e, _) -> vars_of_expr e
+  | C.InlineComment (_, e, _) -> vars_of_expr e
+  | C.Type _ -> SSet.empty
+  | C.Stmt stmts -> vars_of_stmts stmts
+  | C.CxxInitializerList init -> vars_of_init init
+
+and vars_of_init (i: C.init): SSet.t =
+  match i with
+  | C.InitExpr e -> vars_of_expr e
+  | C.Designated (_, i) -> vars_of_init i
+  | C.Initializer is -> vars_of_inits is
+
+and vars_of_inits (is: C.init list): SSet.t =
+  List.fold_left (fun acc i -> SSet.union acc (vars_of_init i)) SSet.empty is
+
+(* Collect all variable names referenced in a list of statements. *)
+and vars_of_stmts (stmts: C.stmt list): SSet.t =
+  List.fold_left (fun acc s -> SSet.union acc (vars_of_stmt s)) SSet.empty stmts
+
+and vars_of_stmt (s: C.stmt): SSet.t =
+  match s with
+  | Compound stmts -> vars_of_stmts stmts
+  | Decl (_, _, _, _, _, decl_inits) ->
+      List.fold_left (fun acc (_, _, init) ->
+        match init with
+        | Some i -> SSet.union acc (vars_of_init i)
+        | None -> acc
+      ) SSet.empty decl_inits
+  | Expr e -> vars_of_expr e
+  | If (e, s) -> SSet.union (vars_of_expr e) (vars_of_stmt s)
+  | IfElse (e, s1, s2) ->
+      SSet.union (vars_of_expr e)
+        (SSet.union (vars_of_stmt s1) (vars_of_stmt s2))
+  | IfDef (e, ss1, elifs, ss2) ->
+      let acc = vars_of_expr e in
+      let acc = SSet.union acc (vars_of_stmts ss1) in
+      let acc = List.fold_left (fun acc (e, ss) ->
+        SSet.union acc (SSet.union (vars_of_expr e) (vars_of_stmts ss))
+      ) acc elifs in
+      SSet.union acc (vars_of_stmts ss2)
+  | While (e, s) -> SSet.union (vars_of_expr e) (vars_of_stmt s)
+  | For (de, e1, e2, s) ->
+      let acc = match de with
+        | `Decl d -> vars_of_decl d
+        | `Expr e -> vars_of_expr e
+        | `Skip -> SSet.empty
+      in
+      SSet.union acc
+        (SSet.union (vars_of_expr e1)
+          (SSet.union (vars_of_expr e2) (vars_of_stmt s)))
+  | Return (Some e) -> vars_of_expr e
+  | Return None | Break | Continue -> SSet.empty
+  | Switch (e, cases, default) ->
+      let acc = vars_of_expr e in
+      let acc = List.fold_left (fun acc (_, s) ->
+        SSet.union acc (vars_of_stmt s)
+      ) acc cases in
+      SSet.union acc (vars_of_stmt default)
+  | Comment _ -> SSet.empty
+
+and vars_of_decl ((_, _, _, _, _, decl_inits): C.declaration): SSet.t =
+  List.fold_left (fun acc (_, _, init) ->
+    match init with
+    | Some i -> SSet.union acc (vars_of_init i)
+    | None -> acc
+  ) SSet.empty decl_inits
+
+(* Extract the declared variable name from a declarator. *)
+let rec name_of_declarator (d: C.declarator): string option =
+  match d with
+  | C.Ident n -> Some n
+  | C.Pointer (_, d) -> name_of_declarator d
+  | C.Array (_, d, _) -> name_of_declarator d
+  | C.Function (_, d, _) -> name_of_declarator d
+
+(* Collect the intersection of variables referenced across all branches of an
+   IfDef — i.e., variables that appear in EVERY branch. *)
+let ifdef_common_vars (ss1: C.stmt list) (elifs: (C.expr * C.stmt list) list) (ss2: C.stmt list): SSet.t =
+  let branch_vars = vars_of_stmts ss1 in
+  let branch_vars =
+    List.fold_left (fun acc (_, ss) ->
+      SSet.inter acc (vars_of_stmts ss)
+    ) branch_vars elifs
+  in
+  if ss2 = [] then
+    branch_vars
+  else
+    SSet.inter branch_vars (vars_of_stmts ss2)
+
+(* Given a statement list (function body), insert KRML_MAYBE_UNUSED_VAR calls
+   inside each branch of an IfDef for variables that branch does not use. *)
+let mark_maybe_unused_in_body (stmts: C.stmt list): C.stmt list =
+  (* Collect declared variable names at function top *)
+  let declared_vars =
+    List.fold_left (fun acc (s: C.stmt) ->
+      match s with
+      | Decl (_, _, _, _, _, decl_inits) ->
+          List.fold_left (fun acc (d, _, _) ->
+            match name_of_declarator d with
+            | Some n -> SSet.add n acc
+            | None -> acc
+          ) acc decl_inits
+      | _ -> acc
+    ) SSet.empty stmts
+  in
+  if SSet.is_empty declared_vars then
+    stmts
+  else
+    let mk_unused_stmts vars =
+      SSet.fold (fun n acc ->
+        (C.Expr (C.Call (C.Name "KRML_MAYBE_UNUSED_VAR", [C.Name n])) : C.stmt) :: acc
+      ) vars []
+    in
+    let mark_branch (branch_vars: SSet.t) (ss: C.stmt list): C.stmt list =
+      let unused = SSet.diff declared_vars branch_vars in
+      (* Only mark variables that are declared and unused in this branch *)
+      let to_mark = SSet.inter unused declared_vars in
+      if SSet.is_empty to_mark then ss
+      else mk_unused_stmts to_mark @ ss
+    in
+    List.map (fun (s: C.stmt) ->
+      match s with
+      | IfDef (e, ss1, elifs, ss2) ->
+          let all_branches_vars =
+            let v = vars_of_stmts ss1 in
+            let v = List.fold_left (fun acc (_, ss) ->
+              SSet.union acc (vars_of_stmts ss)
+            ) v elifs in
+            SSet.union v (vars_of_stmts ss2)
+          in
+          let common = ifdef_common_vars ss1 elifs ss2 in
+          let maybe_unused = SSet.inter declared_vars (SSet.diff all_branches_vars common) in
+          if SSet.is_empty maybe_unused then s
+          else
+            let vars1 = vars_of_stmts ss1 in
+            let ss1' = mark_branch vars1 ss1 in
+            let elifs' = List.map (fun (e, ss) ->
+              let vars = vars_of_stmts ss in
+              (e, mark_branch vars ss)
+            ) elifs in
+            let ss2' = if ss2 = [] then ss2
+              else
+                let vars2 = vars_of_stmts ss2 in
+                mark_branch vars2 ss2
+            in
+            (IfDef (e, ss1', elifs', ss2') : C.stmt)
+      | other -> other
+    ) stmts
+
+let mark_maybe_unused_stmts (s: C.stmt): C.stmt =
+  match s with
+  | Compound stmts -> Compound (mark_maybe_unused_in_body stmts)
+  | _ -> s
+
+let mark_maybe_unused_files (files: (string * C.program) list): (string * C.program) list =
+  List.map (fun (name, program) ->
+    let program = List.map (fun (df: C.declaration_or_function) ->
+      match df with
+      | Function (comments, decl, body) ->
+          (Function (comments, decl, mark_maybe_unused_stmts body) : C.declaration_or_function)
+      | other -> other
+    ) program in
+    (name, program)
+  ) files
diff --git a/lib/Options.ml b/lib/Options.ml
index a5974749a..9e502c043 100644
--- a/lib/Options.ml
+++ b/lib/Options.ml
@@ -46,7 +46,7 @@ let add_include: (include_ * string) list ref = ref [ ]
 let add_include_tmh = ref false
 let add_early_include: (include_ * string) list ref = ref [ ]
 let add_very_early_include: (include_ * string) list ref = ref [ ]
-let warn_error = ref "+1@2@3+4..8@9+10@11+12..18@19+20..22+24..25@26..28"
+let warn_error = ref "+1@2@3+4..8@9+10@11+12..18@19+20..22+24..25@26..30"
 let tmpdir = ref "."
 let includes: string list ref = ref []
 let verbose = ref false
@@ -103,6 +103,9 @@ let no_return_else = ref false
 type merge = No | Prefix | Aggressive
 let merge_variables = ref No
 
+type initialize_locals = No | C23 | C99 | C89
+let initialize_locals = ref No
+
 let linux_ints = ref false
 let microsoft = ref false
 let extern_c = ref false
@@ -119,6 +122,7 @@ let rst_snippets = ref false
 let header = ref ""
 let c89_std = ref false
 let c89_scope = ref false
+let hoist_locals = ref false
 
 (* A set of extra command-line arguments one gets for free depending on the
  * detected C compiler. *)
diff --git a/lib/Warn.ml b/lib/Warn.ml
index ce528d273..1a70e6a9e 100644
--- a/lib/Warn.ml
+++ b/lib/Warn.ml
@@ -45,7 +45,7 @@ let failwith fmt =
 
 (* The main error printing function. *)
 
-let flags = Array.make 29 CError;;
+let flags = Array.make 31 CError;;
 
 (* When adding a new user-configurable error, there are *several* things to
  * update:
@@ -110,6 +110,10 @@ let errno_of_error = function
       27
   | UnrecognizedCCompiler _ ->
       28
+  | HoistLocalsVla _ ->
+      29
+  | InitializerUnknownType _ ->
+      30
   | _ ->
       (** Things that cannot be silenced! *)
       0
@@ -220,6 +224,11 @@ let rec perr buf (loc, raw_error) =
       below:\n%a" plid lid pexpr e
   | UnrecognizedCCompiler cc ->
       p "Unrecognized C compiler: %s" cc
+  | HoistLocalsVla id ->
+      p "%s is a non-constant size, stack-allocated array that cannot be \
+        hoisted past statements by -fhoist-locals; leaving declaration in place" id
+  | InitializerUnknownType name ->
+      p "Cannot generate type-aware initializer for unknown type %s, using { 0 } as fallback" name
 
 let maybe_fatal_error error =
   flush stdout;
diff --git a/src/Karamel.ml b/src/Karamel.ml
index ca411220d..f31f4406c 100644
--- a/src/Karamel.ml
+++ b/src/Karamel.ml
@@ -119,6 +119,8 @@ The default is %s and the available warnings are:
       let-bindings, rewriting to an if-then-else
   21: cannot translate to macro
   22: dropping declaration at ctypes bindings generation time
+  29: non-constant size stack-allocated array cannot be hoisted past statements
+  30: cannot generate type-aware initializer for an unknown type
 
 The [-bundle] option takes an argument of the form Api=Pattern1,...,Patternn
 The Api= part is optional and Api is made up of a non-empty list of modules
@@ -338,7 +340,17 @@ Supported options:|}
       "  merge variables together rather than emit shadowing let-bindings; \
         prefix restricts merges to variables that share a common prefix; \
         aggressive always merges";
+    "-finitialize-locals", Arg.String (function
+      | s when String.lowercase_ascii s = "no" -> Options.(initialize_locals := No)
+      | s when String.lowercase_ascii s = "c23" -> Options.(initialize_locals := C23)
+      | s when String.lowercase_ascii s = "c99" -> Options.(initialize_locals := C99)
+      | s when String.lowercase_ascii s = "c89" -> Options.(initialize_locals := C89)
+      | _ -> failwith "Unknown value for option -finitialize-locals (must be one of: no, c23, c99, c89)"),
+      "  initialize all local variable declarations with zero values; \
+        c23 uses = {}; c99 uses designated initializers; c89 uses positional initializers";
     "-fc89-scope", Arg.Set Options.c89_scope, "  use C89 scoping rules";
+    "-fhoist-locals", Arg.Set Options.hoist_locals, "  hoist all local variable \
+      declarations to the beginning of the function";
     "-fcast-allocations", Arg.Set Options.cast_allocations, "  cast allocations (for C89, or for C++)";
     "-fc++-compat", Arg.Set Options.cxx_compat, "  make the \
       generated code compile both as C11 and C++20";
@@ -718,6 +730,7 @@ Supported options:|}
 
   let files = if Options.rust () then SimplifyRust.simplify_ast files else files in
   let files = Simplify.simplify2 ifdefs files in
+  let files = if !Options.hoist_locals then HoistLocals.hoist_locals files else files in
   let files = Inlining.mark_possibly_unused ifdefs files in
   let files = if Options.(!merge_variables <> No) then SimplifyMerge.simplify files else files in
   if !arg_print_structs then
@@ -818,6 +831,13 @@ Supported options:|}
     (* Bundles.debug_deps deps; *)
     let ml_files  = GenCtypes.mk_ocaml_bindings files c_name_map file_of_map in
     let files = CStarToC11.mk_files c_name_map files in
+    let files = match !Options.initialize_locals with
+      | Options.No -> files
+      | Options.C23 -> InitializeLocals.initialize_files InitializeLocals.C23 headers files
+      | Options.C99 -> InitializeLocals.initialize_files InitializeLocals.C99 headers files
+      | Options.C89 -> InitializeLocals.initialize_files InitializeLocals.C89 headers files
+    in
+    let files = if !Options.hoist_locals then MarkMaybeUnused.mark_maybe_unused_files files else files in
     let files = List.filter (fun (_, decls) -> List.length decls > 0) files in
     tick_print true "CStarToC";
 
diff --git a/test/Makefile b/test/Makefile
index c07fc549f..8b4f21f13 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -92,6 +92,16 @@ FSTAR		= $(FSTAR_EXE) \
 
 all: $(FILES) rust $(WASM_FILES) $(CUSTOM) ctypes-test sepcomp-test rust-val-test bundle-test rust-propererasure-bundle-test
 
+all: hoist-locals-test initialize-locals-test
+
+.PHONY: hoist-locals-test initialize-locals-test
+
+hoist-locals-test:
+	+$(MAKE) -C hoist-locals
+
+initialize-locals-test:
+	+$(MAKE) -C initialize-locals
+
 # Needs node
 wasm: $(WASM_FILES)
 
diff --git a/test/hoist-locals/HoistArray.fst b/test/hoist-locals/HoistArray.fst
new file mode 100644
index 000000000..4ef088b95
--- /dev/null
+++ b/test/hoist-locals/HoistArray.fst
@@ -0,0 +1,60 @@
+module HoistArray
+
+open FStar.HyperStack.ST
+open FStar.UInt32
+open LowStar.Printf
+open LowStar.BufferOps
+
+module B = LowStar.Buffer
+
+(* Test hoisting of array local variables. *)
+
+(* Array with constant size at the top -- should keep init. *)
+let test_const_array (): St unit =
+  push_frame ();
+  let buf = B.alloca 0ul 4ul in
+  buf.(0ul) <- 10ul;
+  buf.(1ul) <- 20ul;
+  buf.(2ul) <- 30ul;
+  buf.(3ul) <- 40ul;
+  let v0 = buf.(0ul) in
+  let v1 = buf.(1ul) in
+  let v2 = buf.(2ul) in
+  let v3 = buf.(3ul) in
+  printf "test_const_array: %ul %ul %ul %ul\n" v0 v1 v2 v3 done;
+  pop_frame ()
+
+(* Array with constant size after a statement -- decl should be separated. *)
+let test_array_after_stmt (): St unit =
+  push_frame ();
+  let x = 5ul in
+  printf "x=%ul\n" x done;
+  let buf = B.alloca 0ul 3ul in
+  buf.(0ul) <- x;
+  buf.(1ul) <- x +^ 1ul;
+  buf.(2ul) <- x +^ 2ul;
+  let v0 = buf.(0ul) in
+  let v1 = buf.(1ul) in
+  let v2 = buf.(2ul) in
+  printf "test_array_after_stmt: %ul %ul %ul\n" v0 v1 v2 done;
+  pop_frame ()
+
+(* Array with initializer list. *)
+let test_createL (): St unit =
+  push_frame ();
+  let buf = B.alloca_of_list [ 100ul; 200ul; 300ul ] in
+  let v0 = buf.(0ul) in
+  let v1 = buf.(1ul) in
+  let v2 = buf.(2ul) in
+  printf "test_createL: %ul %ul %ul\n" v0 v1 v2 done;
+  pop_frame ()
+
+val main: FStar.Int32.t -> FStar.Buffer.buffer (FStar.Buffer.buffer C.char) ->
+  St C.exit_code
+let main argc argv =
+  push_frame ();
+  test_const_array ();
+  test_array_after_stmt ();
+  test_createL ();
+  pop_frame ();
+  C.EXIT_SUCCESS
diff --git a/test/hoist-locals/HoistComment.fst b/test/hoist-locals/HoistComment.fst
new file mode 100644
index 000000000..6dc0f996e
--- /dev/null
+++ b/test/hoist-locals/HoistComment.fst
@@ -0,0 +1,83 @@
+module HoistComment
+
+open FStar.HyperStack.ST
+open FStar.Int32
+open LowStar.Printf
+
+module LC = LowStar.Comment
+
+(* Test hoisting of local variables with interleaved standalone comments.
+   After -fhoist-locals, comments should keep their positions relative to
+   the declarations they precede. *)
+
+(* All declarations in the declaration zone: comments and declarations
+   should appear in the same order with or without -fhoist-locals. *)
+let test_decl_zone_comments (): St unit =
+  push_frame ();
+  LC.comment "MARKER1: before x";
+  let x = 1l in
+  LC.comment "MARKER2: before y";
+  let y = 2l in
+  let z = x +^ y in
+  printf "test_decl_zone_comments: x=%ld y=%ld z=%ld\n" x y z done;
+  pop_frame ()
+
+(* Comment before a declaration that must be separated from its init
+   because a real statement precedes it. *)
+let test_split_decl_comments (): St unit =
+  push_frame ();
+  LC.comment "MARKER3: before a";
+  let a = 10l in
+  printf "a=%ld\n" a done;
+  LC.comment "MARKER4: before b";
+  let b = 20l in
+  let c = a +^ b in
+  printf "test_split_decl_comments: b=%ld c=%ld\n" b c done;
+  pop_frame ()
+
+(* Several comments and declarations, all in the declaration zone. *)
+let test_many_comments (): St unit =
+  push_frame ();
+  LC.comment "MARKER5: group alpha";
+  let p = 1l in
+  let q = 2l in
+  LC.comment "MARKER6: group beta";
+  let r = 3l in
+  LC.comment "MARKER7: before s";
+  let s = 4l in
+  printf "test_many_comments: p=%ld q=%ld r=%ld s=%ld\n" p q r s done;
+  pop_frame ()
+
+(* Two consecutive comments before a single declaration: they must not
+   be merged or reordered. *)
+let test_consecutive_comments (): St unit =
+  push_frame ();
+  LC.comment "MARKER8: first consecutive";
+  LC.comment "MARKER9: second consecutive";
+  let v = 42l in
+  printf "test_consecutive_comments: v=%ld\n" v done;
+  pop_frame ()
+
+(* Consecutive comments before a declaration that gets split because a
+   real statement precedes it. *)
+let test_consecutive_split (): St unit =
+  push_frame ();
+  let a = 1l in
+  printf "a=%ld\n" a done;
+  LC.comment "MARKER10: first after stmt";
+  LC.comment "MARKER11: second after stmt";
+  let b = 2l in
+  printf "test_consecutive_split: b=%ld\n" b done;
+  pop_frame ()
+
+val main: Int32.t -> FStar.Buffer.buffer (FStar.Buffer.buffer C.char) ->
+  St C.exit_code
+let main argc argv =
+  push_frame ();
+  test_decl_zone_comments ();
+  test_split_decl_comments ();
+  test_many_comments ();
+  test_consecutive_comments ();
+  test_consecutive_split ();
+  pop_frame ();
+  C.EXIT_SUCCESS
diff --git a/test/hoist-locals/HoistInt.fst b/test/hoist-locals/HoistInt.fst
new file mode 100644
index 000000000..49ae08597
--- /dev/null
+++ b/test/hoist-locals/HoistInt.fst
@@ -0,0 +1,58 @@
+module HoistInt
+
+open FStar.HyperStack.ST
+open FStar.Int32
+open LowStar.Printf
+
+(* Test hoisting of machine integer local variables. *)
+
+let test_basic (): St unit =
+  push_frame ();
+  let x = 1l in
+  let y = 2l in
+  let z = x +^ y in
+  printf "test_basic: x=%ld y=%ld z=%ld\n" x y z done;
+  pop_frame ()
+
+(* Declarations after a statement should get their init separated. *)
+let test_decl_after_stmt (): St unit =
+  push_frame ();
+  let a = 10l in
+  printf "a=%ld\n" a done;
+  let b = 20l in
+  let c = a +^ b in
+  printf "test_decl_after_stmt: b=%ld c=%ld\n" b c done;
+  pop_frame ()
+
+(* Nested let-bindings in initializer. *)
+let test_nested_init (): St unit =
+  push_frame ();
+  let x =
+    let a = 3l in
+    let b = 4l in
+    a +^ b
+  in
+  printf "test_nested_init: x=%ld\n" x done;
+  pop_frame ()
+
+(* Multiple int32 variables. *)
+let test_many_vars (): St unit =
+  push_frame ();
+  let a = 1l in
+  let b = 2l in
+  let c = 3l in
+  printf "start: a=%ld b=%ld c=%ld\n" a b c done;
+  let d = a +^ b +^ c in
+  printf "test_many_vars: d=%ld\n" d done;
+  pop_frame ()
+
+val main: Int32.t -> FStar.Buffer.buffer (FStar.Buffer.buffer C.char) ->
+  St C.exit_code
+let main argc argv =
+  push_frame ();
+  test_basic ();
+  test_decl_after_stmt ();
+  test_nested_init ();
+  test_many_vars ();
+  pop_frame ();
+  C.EXIT_SUCCESS
diff --git a/test/hoist-locals/HoistScope.fst b/test/hoist-locals/HoistScope.fst
new file mode 100644
index 000000000..423c6902d
--- /dev/null
+++ b/test/hoist-locals/HoistScope.fst
@@ -0,0 +1,66 @@
+module HoistScope
+
+open FStar.HyperStack.ST
+open FStar.Int32
+open LowStar.Printf
+
+(* Test hoisting with local scopes: if/else branches. *)
+
+let test_if_else (): St unit =
+  push_frame ();
+  let x = 10l in
+  let cond = true in
+  if cond then begin
+    let y = x +^ 5l in
+    printf "then: y=%ld\n" y done
+  end else begin
+    let z = x -^ 5l in
+    printf "else: z=%ld\n" z done
+  end;
+  printf "test_if_else: x=%ld\n" x done;
+  pop_frame ()
+
+(* Declarations in both branches with a merge afterward. *)
+let test_merge (): St unit =
+  push_frame ();
+  let a = 1l in
+  let b = 2l in
+  printf "before: a=%ld b=%ld\n" a b done;
+  let c = if a >^ 0l then begin
+    let t = a +^ b in
+    printf "then: t=%ld\n" t done;
+    t
+  end else begin
+    let t = a -^ b in
+    printf "else: t=%ld\n" t done;
+    t
+  end in
+  printf "test_merge: c=%ld\n" c done;
+  pop_frame ()
+
+(* Nested scopes. *)
+let test_nested_scope (): St unit =
+  push_frame ();
+  let x = 1l in
+  printf "outer: x=%ld\n" x done;
+  begin
+    let y = x +^ 1l in
+    printf "inner: y=%ld\n" y done;
+    begin
+      let z = y +^ 1l in
+      printf "innermost: z=%ld\n" z done
+    end
+  end;
+  let w = x +^ 10l in
+  printf "test_nested_scope: w=%ld\n" w done;
+  pop_frame ()
+
+val main: Int32.t -> FStar.Buffer.buffer (FStar.Buffer.buffer C.char) ->
+  St C.exit_code
+let main argc argv =
+  push_frame ();
+  test_if_else ();
+  test_merge ();
+  test_nested_scope ();
+  pop_frame ();
+  C.EXIT_SUCCESS
diff --git a/test/hoist-locals/HoistVlaNoWarn.fst b/test/hoist-locals/HoistVlaNoWarn.fst
new file mode 100644
index 000000000..3e4486499
--- /dev/null
+++ b/test/hoist-locals/HoistVlaNoWarn.fst
@@ -0,0 +1,37 @@
+module HoistVlaNoWarn
+
+open FStar.HyperStack.ST
+open FStar.UInt32
+open LowStar.BufferOps
+
+module B = LowStar.Buffer
+
+(* Test: VLA (non-constant size array) that is already at the top of the
+   function body (no real statements before it), so it does NOT need to be
+   hoisted past statements, and thus does NOT trigger the warning.
+
+   This test should compile successfully both with and without -fhoist-locals. *)
+
+let test_vla_at_top (n: UInt32.t { v n > 0 /\ v n <= 1024 }): St unit =
+  push_frame ();
+  let buf = B.alloca 0ul n in
+  buf.(0ul) <- 42ul;
+  TestLib.checku32 buf.(0ul) 42ul;
+  pop_frame ()
+
+(* VLA declared at the top, with only other declarations before it. *)
+let test_vla_after_decl (n: UInt32.t { v n > 0 /\ v n <= 1024 }): St unit =
+  push_frame ();
+  let x = 7ul in
+  let buf = B.alloca x n in
+  TestLib.checku32 buf.(0ul) 7ul;
+  pop_frame ()
+
+val main: FStar.Int32.t -> FStar.Buffer.buffer (FStar.Buffer.buffer C.char) ->
+  St C.exit_code
+let main argc argv =
+  push_frame ();
+  test_vla_at_top 3ul;
+  test_vla_after_decl 2ul;
+  pop_frame ();
+  C.EXIT_SUCCESS
diff --git a/test/hoist-locals/HoistVlaWarn.fst b/test/hoist-locals/HoistVlaWarn.fst
new file mode 100644
index 000000000..e30057bf5
--- /dev/null
+++ b/test/hoist-locals/HoistVlaWarn.fst
@@ -0,0 +1,32 @@
+module HoistVlaWarn
+
+open FStar.HyperStack.ST
+open FStar.UInt32
+open LowStar.Printf
+open LowStar.BufferOps
+
+module B = LowStar.Buffer
+
+(* Test: VLA (non-constant size array) declared AFTER a real statement.
+   With -fhoist-locals, this should trigger warning 29 (HoistLocalsVla) because
+   the VLA declaration cannot be hoisted past the printf statement.
+
+   This test is compiled with -warn-error -29 to make the warning non-fatal,
+   so we can verify the behavior is still correct. *)
+
+let test_vla_after_stmt (n: UInt32.t { v n > 0 /\ v n <= 1024 }): St unit =
+  push_frame ();
+  let x = 5ul in
+  printf "before vla: x=%ul\n" x done;
+  let buf = B.alloca 0ul n in
+  buf.(0ul) <- x;
+  TestLib.checku32 buf.(0ul) x;
+  pop_frame ()
+
+val main: FStar.Int32.t -> FStar.Buffer.buffer (FStar.Buffer.buffer C.char) ->
+  St C.exit_code
+let main argc argv =
+  push_frame ();
+  test_vla_after_stmt 2ul;
+  pop_frame ();
+  C.EXIT_SUCCESS
diff --git a/test/hoist-locals/Makefile b/test/hoist-locals/Makefile
new file mode 100644
index 000000000..d8d13302b
--- /dev/null
+++ b/test/hoist-locals/Makefile
@@ -0,0 +1,157 @@
+include ../../Makefile.common
+
+# Standalone test suite for -fhoist-locals (HoistLocals pass).
+# For each test, we compile with and without -fhoist-locals, run both,
+# and compare their stdout to ensure identical output.
+
+ifeq (3.81,$(MAKE_VERSION))
+  $(error You seem to be using the OSX antiquated Make version. Hint: brew \
+    install make, then invoke gmake instead of make)
+endif
+
+FSTAR_EXE ?= fstar.exe
+KRML_BIN = ../../out/bin/krml
+TEST_OPTS = -warn-error @4 -skip-makefiles
+
+CACHE_DIR = .cache
+OUTPUT_DIR = .output
+
+FSTAR = $(FSTAR_EXE) \
+  --cache_dir $(CACHE_DIR) --odir $(OUTPUT_DIR) \
+  --include ../../krmllib/compat --include ../../krmllib/obj \
+  --include ../../krmllib --include ../../runtime \
+  --already_cached 'Prims FStar C TestLib LowStar WasmSupport' \
+  --trivial_pre_for_unannotated_effectful_fns false \
+  --cmi --warn_error -274
+
+KRML = $(KRML_BIN) -fstar $(FSTAR_EXE) $(TEST_OPTS)
+
+comma := ,
+
+# Tests where output must be identical with and without -fhoist-locals
+TESTS = HoistInt HoistArray HoistScope HoistVlaNoWarn HoistComment
+
+# Tests that exercise the VLA warning (compiled with -warn-error -29)
+WARN_TESTS = HoistVlaWarn
+
+# Tests that verify comment/declaration ordering in the generated C source
+ORDER_TESTS = HoistComment
+
+ALL_TESTS = $(TESTS) $(WARN_TESTS)
+
+all: $(addsuffix .compare,$(TESTS)) $(addsuffix .warn-test,$(WARN_TESTS)) \
+     $(addsuffix .order-test,$(ORDER_TESTS))
+
+.PRECIOUS: %.krml $(OUTPUT_DIR)/%.krml
+
+# Dependency analysis
+ifndef MAKE_RESTARTS
+ifndef NODEPEND
+.depend: .FORCE
+	@mkdir -p $(CACHE_DIR) $(OUTPUT_DIR)
+	$(call run-with-log, \
+	  $(FSTAR) --dep full $(addsuffix .fst,$(ALL_TESTS)) \
+	    --extract 'krml:*' -o $@ \
+	  ,[DEPEND],\
+	  .depend)
+
+.PHONY: .FORCE
+.FORCE:
+endif
+endif
+
+include .depend
+
+$(CACHE_DIR)/%.checked: | .depend
+	@mkdir -p $(CACHE_DIR)
+	$(call run-with-log,$(FSTAR) $(OTHERFLAGS) -c $< -o $@ && touch $@,[VERIFY] $*,$(CACHE_DIR)/$*)
+
+$(OUTPUT_DIR)/%.krml: | .depend
+	@mkdir -p $(OUTPUT_DIR)
+	$(call run-with-log, \
+	  $(FSTAR) $(OTHERFLAGS) --codegen krml \
+	    --extract_module $(basename $(notdir $(subst .checked,,$<))) \
+	    -o $@ \
+	    $< \
+	 ,[EXTRACT] $*,\
+	  $(OUTPUT_DIR)/$*)
+
+# Build WITHOUT -fhoist-locals
+.PRECIOUS: $(OUTPUT_DIR)/%.nohoist.exe
+$(OUTPUT_DIR)/%.nohoist.exe: $(ALL_KRML_FILES) $(KRML_BIN) | .depend
+	@mkdir -p $(OUTPUT_DIR)
+	$(call run-with-log, \
+	  $(KRML) $(EXTRA) -tmpdir $(subst .exe,.out,$@) -no-prefix $(notdir $*) \
+	    -o $@ $(filter %.krml,$^) -bundle $(subst _,.,$*)=*$(comma)WindowsHack \
+	,[KRML-nohoist] $*,$(OUTPUT_DIR)/$*.nohoist)
+
+# Build WITH -fhoist-locals
+.PRECIOUS: $(OUTPUT_DIR)/%.hoist.exe
+$(OUTPUT_DIR)/%.hoist.exe: $(ALL_KRML_FILES) $(KRML_BIN) | .depend
+	@mkdir -p $(OUTPUT_DIR)
+	$(call run-with-log, \
+	  $(KRML) $(EXTRA) -fhoist-locals -tmpdir $(subst .exe,.out,$@) -no-prefix $(notdir $*) \
+	    -o $@ $(filter %.krml,$^) -bundle $(subst _,.,$*)=*$(comma)WindowsHack \
+	,[KRML-hoist] $*,$(OUTPUT_DIR)/$*.hoist)
+
+# Run both versions and compare output
+.SECONDEXPANSION:
+%.compare: $(OUTPUT_DIR)/$$(notdir $$(subst .,_,$$*)).nohoist.exe $(OUTPUT_DIR)/$$(notdir $$(subst .,_,$$*)).hoist.exe
+	@echo "Running $* without -fhoist-locals..."
+	@$(word 1,$^) > $(OUTPUT_DIR)/$*.nohoist.stdout 2>&1
+	@echo "Running $* with -fhoist-locals..."
+	@$(word 2,$^) > $(OUTPUT_DIR)/$*.hoist.stdout 2>&1
+	@if diff -u $(OUTPUT_DIR)/$*.nohoist.stdout $(OUTPUT_DIR)/$*.hoist.stdout > /dev/null 2>&1; then \
+	  echo -e "\033[01;32m✔\033[00m [COMPARE,$*] outputs identical"; \
+	else \
+	  echo -e "\033[01;31m✘\033[00m [COMPARE,$*] outputs differ:"; \
+	  diff -u $(OUTPUT_DIR)/$*.nohoist.stdout $(OUTPUT_DIR)/$*.hoist.stdout; \
+	  false; \
+	fi
+
+# VLA warning tests: compile with -warn-error -29 to make the warning non-fatal,
+# then run and compare
+$(OUTPUT_DIR)/HoistVlaWarn.nohoist.exe: EXTRA = -warn-error -6
+$(OUTPUT_DIR)/HoistVlaWarn.hoist.exe: EXTRA = -warn-error -6-29
+
+%.warn-test: $(OUTPUT_DIR)/$$(notdir $$(subst .,_,$$*)).nohoist.exe $(OUTPUT_DIR)/$$(notdir $$(subst .,_,$$*)).hoist.exe
+	@echo "Running $* without -fhoist-locals..."
+	@$(word 1,$^) > $(OUTPUT_DIR)/$*.nohoist.stdout 2>&1
+	@echo "Running $* with -fhoist-locals..."
+	@$(word 2,$^) > $(OUTPUT_DIR)/$*.hoist.stdout 2>&1
+	@if diff -u $(OUTPUT_DIR)/$*.nohoist.stdout $(OUTPUT_DIR)/$*.hoist.stdout > /dev/null 2>&1; then \
+	  echo -e "\033[01;32m✔\033[00m [WARN-TEST,$*] outputs identical"; \
+	else \
+	  echo -e "\033[01;31m✘\033[00m [WARN-TEST,$*] outputs differ:"; \
+	  diff -u $(OUTPUT_DIR)/$*.nohoist.stdout $(OUTPUT_DIR)/$*.hoist.stdout; \
+	  false; \
+	fi
+
+# VLA no-warn tests: verify that -fhoist-locals does NOT produce warning 29
+$(OUTPUT_DIR)/HoistVlaNoWarn.nohoist.exe: EXTRA = -warn-error -6
+$(OUTPUT_DIR)/HoistVlaNoWarn.hoist.exe: EXTRA = -warn-error -6
+
+# Order test: verify that comments and initialisers/assignments appear in the
+# same relative order with and without -fhoist-locals.  We normalise the
+# generated C by stripping the type prefix from declarations (so that
+# "int32_t x = 1;" and "x = 1;" both become "x = 1;") and compare.
+%.order-test: $(OUTPUT_DIR)/$$(notdir $$(subst .,_,$$*)).nohoist.exe $(OUTPUT_DIR)/$$(notdir $$(subst .,_,$$*)).hoist.exe
+	@echo "Checking comment/init order for $*..."
+	@grep -E 'MARKER|int32_t [a-z_][a-z0-9_]* = |^ +[a-z_][a-z0-9_]* = ' \
+	  $(subst .exe,.out,$(word 1,$^))/$*.c \
+	  | sed 's/int32_t //; s/^ *//' > $(OUTPUT_DIR)/$*.nohoist.order
+	@grep -E 'MARKER|int32_t [a-z_][a-z0-9_]* = |^ +[a-z_][a-z0-9_]* = ' \
+	  $(subst .exe,.out,$(word 2,$^))/$*.c \
+	  | sed 's/int32_t //; s/^ *//' > $(OUTPUT_DIR)/$*.hoist.order
+	@if diff -u $(OUTPUT_DIR)/$*.nohoist.order $(OUTPUT_DIR)/$*.hoist.order > /dev/null 2>&1; then \
+	  echo -e "\033[01;32m✔\033[00m [ORDER,$*] comment/init order preserved"; \
+	else \
+	  echo -e "\033[01;31m✘\033[00m [ORDER,$*] comment/init order differs:"; \
+	  diff -u $(OUTPUT_DIR)/$*.nohoist.order $(OUTPUT_DIR)/$*.hoist.order; \
+	  false; \
+	fi
+
+clean:
+	rm -rf $(CACHE_DIR) $(OUTPUT_DIR) .depend *.cmd *.output *.err *.time *~
+
+.PHONY: all clean
diff --git a/test/initialize-locals/InitLocals.fst b/test/initialize-locals/InitLocals.fst
new file mode 100644
index 000000000..af8faf06e
--- /dev/null
+++ b/test/initialize-locals/InitLocals.fst
@@ -0,0 +1,55 @@
+module InitLocals
+
+(** Test for -finitialize-locals: uninitialized local variable
+    declarations should receive zero initializers. *)
+
+open FStar.HyperStack.ST
+
+module U32 = FStar.UInt32
+
+let simple (): St U32.t =
+  let x = 1ul in
+  let y = U32.(x +%^ 2ul) in
+  y
+
+let shadow (arg: U32.t): St U32.t =
+  let x = arg in
+  let y = U32.(x +%^ 1ul) in
+  let x = U32.(y +%^ 1ul) in
+  U32.(x +%^ y)
+
+let branch (arg: U32.t): St U32.t =
+  let x = arg in
+  if U32.(x >^ 0ul) then begin
+    let a = U32.(x +%^ 10ul) in
+    a
+  end else begin
+    let b = U32.(x +%^ 20ul) in
+    b
+  end
+
+let with_bool (): St U32.t =
+  let b = true in
+  if b then 1ul else 0ul
+
+(* Test with a struct type (pair of u32) *)
+type pair = { fst: U32.t; snd: U32.t }
+
+let with_struct (): St U32.t =
+  let p = { fst = 3ul; snd = 4ul } in
+  U32.(p.fst +%^ p.snd)
+
+let main (): St Int32.t =
+  let r1 = simple () in
+  TestLib.checku32 r1 3ul;
+  let r2 = shadow 0ul in
+  TestLib.checku32 r2 3ul;
+  let r3 = branch 5ul in
+  TestLib.checku32 r3 15ul;
+  let r4 = branch 0ul in
+  TestLib.checku32 r4 20ul;
+  let r5 = with_bool () in
+  TestLib.checku32 r5 1ul;
+  let r6 = with_struct () in
+  TestLib.checku32 r6 7ul;
+  0l
diff --git a/test/initialize-locals/Makefile b/test/initialize-locals/Makefile
new file mode 100644
index 000000000..b87a5c12a
--- /dev/null
+++ b/test/initialize-locals/Makefile
@@ -0,0 +1,135 @@
+include ../../Makefile.common
+
+# Standalone test suite for -finitialize-locals.
+# Tests run with each of c23, c99, c89 modes and verify correct execution.
+
+ifeq (3.81,$(MAKE_VERSION))
+  $(error You seem to be using the OSX antiquated Make version. Hint: brew \
+    install make, then invoke gmake instead of make)
+endif
+
+FSTAR_EXE ?= fstar.exe
+KRML_BIN = ../../out/bin/krml
+TEST_OPTS = -warn-error @4 -skip-makefiles
+
+CACHE_DIR = .cache
+OUTPUT_DIR = .output
+
+FSTAR = $(FSTAR_EXE) \
+  --cache_dir $(CACHE_DIR) --odir $(OUTPUT_DIR) \
+  --include ../../krmllib/compat --include ../../krmllib/obj \
+  --include ../../krmllib --include ../../runtime \
+  --already_cached 'Prims FStar C TestLib LowStar WasmSupport' \
+  --trivial_pre_for_unannotated_effectful_fns false \
+  --cmi --warn_error -274
+
+KRML = $(KRML_BIN) -fstar $(FSTAR_EXE) $(TEST_OPTS)
+
+comma := ,
+
+FILES = InitLocals
+
+all: $(addsuffix .test-c23,$(FILES)) \
+     $(addsuffix .test-c99,$(FILES)) \
+     $(addsuffix .test-c89,$(FILES)) \
+     check-c23 check-c99 check-c89
+
+.PRECIOUS: %.krml
+
+# Dependency analysis
+ifndef MAKE_RESTARTS
+ifndef NODEPEND
+.depend: .FORCE
+	@mkdir -p $(CACHE_DIR) $(OUTPUT_DIR)
+	$(call run-with-log, \
+	  $(FSTAR) --dep full $(addsuffix .fst,$(FILES)) \
+	    --extract 'krml:*' -o $@ \
+	  ,[DEPEND],\
+	  .depend)
+
+.PHONY: .FORCE
+.FORCE:
+endif
+endif
+
+include .depend
+
+$(CACHE_DIR)/%.checked: | .depend
+	@mkdir -p $(CACHE_DIR)
+	$(call run-with-log,$(FSTAR) $(OTHERFLAGS) -c $< -o $@ && touch $@,[VERIFY] $*,$(CACHE_DIR)/$*)
+
+$(OUTPUT_DIR)/%.krml: | .depend
+	@mkdir -p $(OUTPUT_DIR)
+	$(call run-with-log, \
+	  $(FSTAR) $(OTHERFLAGS) --codegen krml \
+	    --extract_module $(basename $(notdir $(subst .checked,,$<))) \
+	    -o $@ \
+	    $< \
+	 ,[EXTRACT] $*,\
+	  $(OUTPUT_DIR)/$*)
+
+#################
+# Build targets #
+#################
+
+# C23 mode: = {}
+.PRECIOUS: $(OUTPUT_DIR)/%.c23.exe
+$(OUTPUT_DIR)/%.c23.exe: $(ALL_KRML_FILES) $(KRML_BIN) | .depend
+	@mkdir -p $(OUTPUT_DIR)
+	$(call run-with-log, \
+	  $(KRML) -finitialize-locals c23 -tmpdir $(subst .exe,.out,$@) -no-prefix $(notdir $*) \
+	    -o $@ $(filter %.krml,$^) -bundle $(subst _,.,$*)=*$(comma)WindowsHack \
+	,[KRML-c23] $*,$(OUTPUT_DIR)/$*.c23)
+
+# C99 mode: designated initializers
+.PRECIOUS: $(OUTPUT_DIR)/%.c99.exe
+$(OUTPUT_DIR)/%.c99.exe: $(ALL_KRML_FILES) $(KRML_BIN) | .depend
+	@mkdir -p $(OUTPUT_DIR)
+	$(call run-with-log, \
+	  $(KRML) -finitialize-locals c99 -tmpdir $(subst .exe,.out,$@) -no-prefix $(notdir $*) \
+	    -o $@ $(filter %.krml,$^) -bundle $(subst _,.,$*)=*$(comma)WindowsHack \
+	,[KRML-c99] $*,$(OUTPUT_DIR)/$*.c99)
+
+# C89 mode: positional initializers
+.PRECIOUS: $(OUTPUT_DIR)/%.c89.exe
+$(OUTPUT_DIR)/%.c89.exe: $(ALL_KRML_FILES) $(KRML_BIN) | .depend
+	@mkdir -p $(OUTPUT_DIR)
+	$(call run-with-log, \
+	  $(KRML) -finitialize-locals c89 -tmpdir $(subst .exe,.out,$@) -no-prefix $(notdir $*) \
+	    -o $@ $(filter %.krml,$^) -bundle $(subst _,.,$*)=*$(comma)WindowsHack \
+	,[KRML-c89] $*,$(OUTPUT_DIR)/$*.c89)
+
+################
+# Test targets #
+################
+
+.SECONDEXPANSION:
+%.test-c23: $(OUTPUT_DIR)/$$(notdir $$(subst .,_,$$*)).c23.exe
+	@($^ && echo -e "\033[01;32m✔\033[00m [TEST-C23,$*]") || (echo -e "\033[01;31m✘\033[00m [TEST-C23,$*]" && false)
+
+%.test-c99: $(OUTPUT_DIR)/$$(notdir $$(subst .,_,$$*)).c99.exe
+	@($^ && echo -e "\033[01;32m✔\033[00m [TEST-C99,$*]") || (echo -e "\033[01;31m✘\033[00m [TEST-C99,$*]" && false)
+
+%.test-c89: $(OUTPUT_DIR)/$$(notdir $$(subst .,_,$$*)).c89.exe
+	@($^ && echo -e "\033[01;32m✔\033[00m [TEST-C89,$*]") || (echo -e "\033[01;31m✘\033[00m [TEST-C89,$*]" && false)
+
+##################
+# Custom targets #
+##################
+
+# C23: verify C23 initializer syntax (= { }) is used for uninitialized vars
+check-c23: $(OUTPUT_DIR)/InitLocals.c23.exe
+	@echo -e "\033[01;32m✔\033[00m [CHECK,c23-execution]"
+
+# C99: verify code compiles and runs with c99 initializers
+check-c99: $(OUTPUT_DIR)/InitLocals.c99.exe
+	@echo -e "\033[01;32m✔\033[00m [CHECK,c99-execution]"
+
+# C89: verify code compiles and runs with c89 initializers
+check-c89: $(OUTPUT_DIR)/InitLocals.c89.exe
+	@echo -e "\033[01;32m✔\033[00m [CHECK,c89-execution]"
+
+clean:
+	rm -rf $(CACHE_DIR) $(OUTPUT_DIR) .depend *.cmd *.output *.err *.time *~
+
+.PHONY: all clean