diff --git a/CHANGELOG.md b/CHANGELOG.md
index 785a6c5af..cecbdf00c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,10 @@ All notable changes to Aver are documented here. Starting with 0.10.0, minor rel
 
 ## Unreleased
 
+### Added — certificates for list literals
+
+- **A function that builds a non-empty list literal can now be certified.** `[a, b, c]` used to leave the function source-level only. The compiler builds such a literal by calling its cons helper for the element type once per item, and the certificate now carries that helper as a planned function: the wall checks that its plan is exactly one `List.prepend` of its two parameters, so the literal's meaning is proved, not assumed. On the btc-listener corpus this certifies 58 more functions and gives 41 more of them a source bridge (a function that returns a literal is now bridged to its source); across the examples, projects and certificate fixtures, 27 more functions are certified. The wall identity rotates: packages produced by earlier versions must be produced again.
+
 ### Added — certificates for a match on a List
 
 - **A function that matches on a List can now be certified.** `match xs` with a `[]` arm and a `[head, ..tail]` arm, in either order, or one of them followed by `_`, used to leave the function source-level only. Such a function now gets a certificate for the bytes the compiler already emits, recursive ones included (`count(rest)` on the tail). On the btc-listener corpus this certifies 133 more functions, and 160 more across the examples, projects and certificate fixtures. A List argument has no source-bridge encoder yet, so these functions are certified against their plan and carry no bridge. The wall identity rotates: packages produced by earlier versions must be produced again.
diff --git a/aver-cert/assets/wall/current/AcceptanceSoundness.lean b/aver-cert/assets/wall/current/AcceptanceSoundness.lean
index cab000b01..163b8e057 100644
--- a/aver-cert/assets/wall/current/AcceptanceSoundness.lean
+++ b/aver-cert/assets/wall/current/AcceptanceSoundness.lean
@@ -46,6 +46,15 @@ theorem contracts_of {C : Nat} (S : CarrierSpec C) (h : HostFns) (hc : HostContr
   hCmp := hc.cmp
   hEq := hc.eq
 
+/-- A declared cons helper means `List.prepend` in the one model of all plans. -/
+theorem modelOf_cons (hf : PlanFacts s tt fns) :
+    ∀ t f, (mctxOf s tt fns).listCons t = some f → ∀ k h tl sv,
+      HasTy (mctxOf s tt fns) tl (.list t) → modelOf fns k f [h, tl] = some sv →
+        sv = .cons t h tl := by
+  intro t f hf' k h tl sv htl hm
+  obtain ⟨p, hp, hcp⟩ := hf.cons t f hf'
+  exact groupModel_consPlan _ (planOf fns) hp (isConsPlan_body hcp) k h tl sv htl hm
+
 /-- Every planned function is certified at the one model of all plans. -/
 theorem fns_certified (hf : PlanFacts s tt fns)
     (S : CarrierSpec (mctxOf s tt fns).carrier) (h : HostFns) (hc : HostContracts S h) :
@@ -64,6 +73,7 @@ theorem fns_certified (hf : PlanFacts s tt fns)
   refine fn_certified_group S (boxRef _) h.add h.sub h.mul h.cmp h.eq (fun _ => none)
     (contracts_of S h hc) (fun _ _ _ _ hr => by cases hr) _ _ (mctxOf s tt fns) rfl
     hBox hAdd hSub hMul hNeg hCmp hEq R (planOf fns) (fun _ _ _ => none) ?_ ?_
+    (modelOf_cons hf)
   · intro f sig hs hG
     simp [mctxOf, hG] at hs
   · intro f p hp
@@ -148,6 +158,12 @@ theorem obligation_total (hf : PlanFacts s tt fns) {e : FnEntry} (he : e ∈ fns
       have hp := hGP f p hg
       obtain ⟨e', he', rfl, rfl⟩ := planOf_some hp
       exact ⟨by simp [mctxOf, hp], hf.typed e' he', hClaims e' he', by simp [codeOf, hp]⟩)
+    (by
+      intro t f hf' k h tl sv htl hm
+      have hm' : groupModel (groupModel (fun _ _ _ => none) (planOf fns)) (groupOf ms) k f
+          [h, tl] = some sv := hm
+      rw [groupModel_restrict (planOf fns) (groupOf ms) hGP] at hm'
+      exact modelOf_cons hf t f hf' k h tl sv htl hm')
     (fun k _ _ => boxRef_total _ k) ht.add ht.sub ht.mul
     e.funcIdx e.plan (hGall (e.funcIdx, e.plan) (by
       simp only [ms, groupMembers]
@@ -234,7 +250,7 @@ theorem accepted_nonvacuous (artifact : ArtifactData)
   have hwf : declsWellFormed artifact.manifest.subject artifact.manifest.types
       artifact.manifest.fnPlans = true := by
     simp only [plansAccepted, Bool.and_eq_true] at hPlans
-    exact hPlans.2
+    exact hPlans.1.2
   have hti : typesInhabited (mctxOf artifact.manifest.subject artifact.manifest.types
       artifact.manifest.fnPlans) artifact.manifest.types artifact.manifest.fnPlans = true := by
     simp only [declsWellFormed, Bool.and_eq_true] at hwf
@@ -262,7 +278,7 @@ theorem refTest_exact_of_accepted (artifact : ArtifactData)
   intro M
   have hpin : S3Pin M d.tid d.ctors.length (grp.map (·.1)) = true := by
     simp only [plansAccepted, Bool.and_eq_true] at hPlans
-    have htt := hPlans.1.1.1.2
+    have htt := hPlans.1.1.1.1.2
     unfold typeTableConfirmed at htt
     simp only [hg, Bool.and_eq_true, List.all_eq_true] at htt
     have hs := htt.2.1.1.1.1.1.1.1.2 d hd
diff --git a/aver-cert/assets/wall/current/AcceptanceSoundnessCore.lean b/aver-cert/assets/wall/current/AcceptanceSoundnessCore.lean
index 5331ba79b..c18cdc29e 100644
--- a/aver-cert/assets/wall/current/AcceptanceSoundnessCore.lean
+++ b/aver-cert/assets/wall/current/AcceptanceSoundnessCore.lean
@@ -158,6 +158,8 @@ theorem groupModel_restrict (P G : Nat → Option FnPlan)
 structure PlanFacts (s : Subject) (tt : TypeTable) (fns : List FnEntry) : Prop where
   distinct : (roleIndices (mctxOf s tt fns) ++ fns.map (·.funcIdx)).Nodup
   typed : ∀ e ∈ fns, planTyped (mctxOf s tt fns) e.plan = true
+  cons : ∀ t f, (mctxOf s tt fns).listCons t = some f →
+    ∃ p, planOf fns f = some p ∧ isConsPlan p = true
 
 theorem PlanFacts.nodup {s : Subject} {tt : TypeTable} {fns : List FnEntry}
     (hf : PlanFacts s tt fns) : (fns.map (·.funcIdx)).Nodup :=
@@ -165,11 +167,21 @@ theorem PlanFacts.nodup {s : Subject} {tt : TypeTable} {fns : List FnEntry}
 
 theorem planFacts_of_accepted (artifact : ArtifactData) (h : plansAccepted artifact = true) :
     PlanFacts artifact.manifest.subject artifact.manifest.types artifact.manifest.fnPlans := by
-  simp only [plansAccepted, Bool.and_eq_true, List.all_eq_true] at h
-  obtain ⟨⟨⟨⟨⟨hd, he⟩, _⟩, _⟩, _⟩, _⟩ := h
-  refine ⟨of_decide_eq_true hd, fun e hm => ?_⟩
-  have := he e hm
-  simp only [entryAccepted, Bool.and_eq_true] at this
-  exact this.1.1
+  simp only [plansAccepted, consPinned, Bool.and_eq_true, List.all_eq_true] at h
+  obtain ⟨⟨⟨⟨⟨⟨hd, he⟩, _⟩, _⟩, _⟩, _⟩, hc⟩ := h
+  refine ⟨of_decide_eq_true hd, fun e hm => ?_, fun t f hf => ?_⟩
+  · have := he e hm
+    simp only [entryAccepted, Bool.and_eq_true] at this
+    exact this.1.1
+  · simp only [mctxOf, Option.map_eq_some_iff] at hf
+    obtain ⟨x, hx, rfl⟩ := hf
+    have hmem := hc x (List.mem_of_find?_eq_some hx)
+    revert hmem
+    split
+    · rename_i p hp
+      intro hmem
+      exact ⟨p, hp, hmem⟩
+    · intro hmem
+      cases hmem
 
 end AcceptanceSoundness
diff --git a/aver-cert/assets/wall/current/AcceptedArtifactCore.lean b/aver-cert/assets/wall/current/AcceptedArtifactCore.lean
index 4eafb0ad4..f0a68cd21 100644
--- a/aver-cert/assets/wall/current/AcceptedArtifactCore.lean
+++ b/aver-cert/assets/wall/current/AcceptedArtifactCore.lean
@@ -103,7 +103,16 @@ def obligationsOf (s : Subject) (tt : TypeTable) (fns : List FnEntry) : List Obl
 /-! ### Calls -/
 
 mutual
-  /-- The function indices a plan calls (`call` and `tailCall`). -/
+  /-- Every declared cons helper is a planned function whose plan is the
+    wall's cons plan (`Grammar.isConsPlan`: its body is `consBody`), so a
+    non-empty list literal calls a function whose meaning is `List.prepend`. -/
+def consPinned (tt : TypeTable) (fns : List FnEntry) : Bool :=
+  tt.listCons.all fun x =>
+    match planOf fns x.2 with
+    | some p => isConsPlan p
+    | none => false
+
+/-- The function indices a plan calls (`call` and `tailCall`). -/
   def callTargets : Expr → List Nat
     | .literal _ => []
     | .local _ => []
@@ -567,7 +576,8 @@ def plansAccepted (artifact : ArtifactData) : Bool :=
   typeTableConfirmed artifact.modBytes artifact.modLen m.subject m.types m.fnPlans &&
   dataConfirmed artifact.modBytes artifact.modLen m.subject m.types m.fnPlans &&
   roleTypesPinned artifact.modBytes artifact.modLen M &&
-  declsWellFormed m.subject m.types m.fnPlans
+  declsWellFormed m.subject m.types m.fnPlans &&
+  consPinned m.types m.fnPlans
 
 /-- The conjuncts of `plansAccepted` other than the per-entry checks. A
     package proves the per-entry checks in chunks, one declaration each, so
@@ -579,7 +589,8 @@ def plansAcceptedRest (artifact : ArtifactData) : Bool :=
   typeTableConfirmed artifact.modBytes artifact.modLen m.subject m.types m.fnPlans &&
   dataConfirmed artifact.modBytes artifact.modLen m.subject m.types m.fnPlans &&
   roleTypesPinned artifact.modBytes artifact.modLen M &&
-  declsWellFormed m.subject m.types m.fnPlans
+  declsWellFormed m.subject m.types m.fnPlans &&
+  consPinned m.types m.fnPlans
 
 theorem plansAccepted_of_parts (artifact : ArtifactData)
     (hall : artifact.manifest.fnPlans.all
@@ -588,9 +599,9 @@ theorem plansAccepted_of_parts (artifact : ArtifactData)
         artifact.manifest.fnPlans) = true)
     (hrest : plansAcceptedRest artifact = true) : plansAccepted artifact = true := by
   simp only [plansAcceptedRest, Bool.and_eq_true] at hrest
-  obtain ⟨⟨⟨⟨ha, hc⟩, hd⟩, he⟩, hf⟩ := hrest
+  obtain ⟨⟨⟨⟨⟨ha, hc⟩, hd⟩, he⟩, hf⟩, hg⟩ := hrest
   simp only [plansAccepted, Bool.and_eq_true]
-  exact ⟨⟨⟨⟨⟨ha, hall⟩, hc⟩, hd⟩, he⟩, hf⟩
+  exact ⟨⟨⟨⟨⟨⟨ha, hall⟩, hc⟩, hd⟩, he⟩, hf⟩, hg⟩
 
 /-- The manifest's obligations are exactly the ones the wall derives from its
     plans: no obligation field is producer data. -/
diff --git a/aver-cert/assets/wall/current/DeclaredLayout.lean b/aver-cert/assets/wall/current/DeclaredLayout.lean
index 8b3a6b811..27fef935c 100644
--- a/aver-cert/assets/wall/current/DeclaredLayout.lean
+++ b/aver-cert/assets/wall/current/DeclaredLayout.lean
@@ -205,7 +205,8 @@ def plansAcceptedRestL (artifact : ArtifactData) (L : Layout) : Bool :=
   typeTableConfirmed artifact.modBytes artifact.modLen m.subject m.types m.fnPlans &&
   dataConfirmed artifact.modBytes artifact.modLen m.subject m.types m.fnPlans &&
   roleTypesPinnedL L artifact.modBytes artifact.modLen M &&
-  declsWellFormed m.subject m.types m.fnPlans
+  declsWellFormed m.subject m.types m.fnPlans &&
+  consPinned m.types m.fnPlans
 
 theorem plansAcceptedRest_of_layout {artifact : ArtifactData} {L : Layout}
     (hL : layoutConfirmed artifact.modBytes artifact.modLen L = true)
diff --git a/aver-cert/assets/wall/current/Grammar.lean b/aver-cert/assets/wall/current/Grammar.lean
index edc8d6971..e583845a3 100644
--- a/aver-cert/assets/wall/current/Grammar.lean
+++ b/aver-cert/assets/wall/current/Grammar.lean
@@ -49,7 +49,11 @@
      Euclidean `__aint_divmod` call.
    * `interp parts` — `InterpolatedStr` whose parts are all `String` (a
      literal part printed as a string literal).
-   * `list t []` — the empty `List(..)` literal, with its element type.
+   * `list t items` — a `List(..)` literal with its element type: `[]` is
+     `ref.null` of the cons struct, and a non-empty literal pushes its items,
+     `ref.null`, and calls the `List<t>` cons helper once per item. The
+     helper's index comes from the type table (`MCtx.listCons`), and the
+     acceptance pins its plan to exactly `consPlan t`.
    * `construct c ty args` — `Construct`; `c` is the constructor
      (`MirCtor::User(CtorId)` as type id + constructor index, or a built-in
      `Some`/`None`/`Ok`/`Err`) and `ty` is the node's stamped type
@@ -206,8 +210,7 @@ mutual
     /-- `InterpolatedStr` whose parts are all `String`: a literal part is
         printed as a string literal, an embed as its expression. -/
     | interp (parts : List Expr)
-    /-- `List(items)` with its element type (the stamped instantiation);
-        only the empty literal `[]` is admitted. -/
+    /-- `List(items)` with its element type (the stamped instantiation). -/
     | list (elem : Ty) (items : List Expr)
   /-- The arms of a `Match`, in source order. -/
   inductive Arms where
@@ -276,6 +279,9 @@ structure MCtx where
   vecStruct : Ty → Nat := fun _ => 0
   listStruct : Ty → Nat := fun _ => 0
   opaqueStruct : Nat → Nat := fun _ => 0
+  /-- The cons helper of `List<T>` (`(T, List<T>) -> List<T>`) a non-empty
+      literal calls, when the type table declares one. -/
+  listCons : Ty → Option Nat := fun _ => none
 
 /-- One function's plan: signature, the resolver slot count (parameters and
     every binder; the const-compare scratch local sits at this index), the
@@ -437,6 +443,28 @@ def varArmΓ (M : MCtx) (n : Nat) (Γ : Nat → Option Ty) (tid : Nat) : Pat →
   | .wild => some Γ
   | _ => none
 
+/-! ## The cons helper
+
+A non-empty list literal calls the per-instantiation cons helper, whose body
+is one `struct.new` of the cons struct: exactly the lowering of the one-node
+plan `List.prepend(local 0, local 1)`. -/
+
+/-- The cons helper's signature. -/
+def consSig (t : Ty) : Sig := ⟨[t, .list t], .list t⟩
+
+/-- The cons helper's body: `List.prepend(head, tail)` over its parameters. -/
+def consBody : Expr := .call (.builtin .listPrepend) [.local 0, .local 1]
+
+/-- A plan is the wall's own cons plan: its body is `consBody`, so its
+    meaning is `List.prepend` of its two arguments. (Its signature is the
+    typing's business: a literal of `List<t>` requires the helper's planned
+    signature to be `consSig t`; its slots and locals are pinned with its
+    code entry like every plan's.) -/
+def isConsPlan (p : FnPlan) : Bool :=
+  match p.body with
+  | .call (.builtin .listPrepend) [.local 0, .local 1] => true
+  | _ => false
+
 /-! ## Typing
 
 One checker for every node. `n` is the resolver slot count: a `let` binder
@@ -557,9 +585,14 @@ mutual
         | some ts => if allStr ts then some .string else none
         | none => none
     | .list t items =>
-        match items with
-        | [] => some (.list t)
-        | _ => none
+        if items.isEmpty then some (.list t)
+        else
+          match M.listCons t, tysOf M n Γ items with
+          | some f, some ts =>
+              if M.sigs f = some (consSig t) ∧ ts.all (fun x => decide (x = t)) = true then
+                some (.list t)
+              else none
+          | _, _ => none
     | .match_ s arms =>
         match tyOf M n Γ false s with
         | some .int => if arms.firstLit then tyIntArms M n Γ tail arms else none
@@ -833,6 +866,11 @@ def strCat : List SVal → Option (List Nat)
 def divByZeroBytes : List Nat :=
   [100, 105, 118, 105, 115, 105, 111, 110, 32, 98, 121, 32, 122, 101, 114, 111]
 
+/-- The list of `vs`, in order, as cons cells of `List<t>`. -/
+def consAll (t : Ty) : List SVal → SVal
+  | [] => .nil t
+  | v :: vs => .cons t v (consAll t vs)
+
 def builtinEval : Builtin → List SVal → Option SVal
   | .boolAnd, [.b x, .b y] => some (.b (x && y))
   | .boolOr, [.b x, .b y] => some (.b (x || y))
@@ -965,9 +1003,11 @@ mutual
         | some vs => (strCat vs).map .s
         | none => none
     | .list t items =>
-        match items with
-        | [] => some (.nil t)
-        | _ => none
+        if items.isEmpty then some (.nil t)
+        else
+          match evalArgs F env items with
+          | some vs => some (consAll t vs)
+          | none => none
   def evalArgs (F : Nat → List SVal → Option SVal) (env : Nat → Option SVal) :
       List Expr → Option (List SVal)
     | [] => some []
diff --git a/aver-cert/assets/wall/current/GrammarBridge.lean b/aver-cert/assets/wall/current/GrammarBridge.lean
index 95571940c..1aa2df632 100644
--- a/aver-cert/assets/wall/current/GrammarBridge.lean
+++ b/aver-cert/assets/wall/current/GrammarBridge.lean
@@ -337,7 +337,15 @@ theorem eval_mono {F G : Nat → List SVal → Option SVal} (hle : Le F G) :
       split at h
       · rename_i vs hvs; rw [evalArgs_mono hle env parts vs hvs]; exact h
       · cases h
-  | env, .list t items, v, h => by simpa [eval] using h
+  | env, .list t items, v, h => by
+      simp only [eval] at h ⊢
+      by_cases he : items.isEmpty = true
+      · simp only [he, ↓reduceIte] at h ⊢
+        exact h
+      · simp only [he, Bool.false_eq_true, ↓reduceIte] at h ⊢
+        split at h
+        · rename_i vs hvs; rw [evalArgs_mono hle env items vs hvs]; exact h
+        · cases h
 theorem evalArgs_mono {F G : Nat → List SVal → Option SVal} (hle : Le F G) :
     ∀ (env : Nat → Option SVal) (es : List Expr) (vs : List SVal),
       evalArgs F env es = some vs → evalArgs G env es = some vs
diff --git a/aver-cert/assets/wall/current/GrammarLower.lean b/aver-cert/assets/wall/current/GrammarLower.lean
index 582d9e8dd..2ad2dccb9 100644
--- a/aver-cert/assets/wall/current/GrammarLower.lean
+++ b/aver-cert/assets/wall/current/GrammarLower.lean
@@ -46,7 +46,9 @@
    * a tuple destructure stashes the subject and reads each bound component
      with `ref.cast` + `struct.get` (`emit_mir_tuple_match`);
    * `[]` is `ref.null` of the list's cons struct, `List.prepend` is
-     `struct.new` of it;
+     `struct.new` of it; a non-empty literal pushes its items in order, then
+     `ref.null`, then calls the cons helper once per item, so the last item
+     is consed first (`emit_mir_list_literal`);
    * a List `Match` stashes the subject and tests it with `ref.is_null`: the
      `[]` arm in `then`, and in `else` the head (field 0) and tail (field 1)
      binders, each by `ref.cast` + `struct.get`, then the cons arm
@@ -442,7 +444,14 @@ mutual
               lowerListArms M X Γ tail (tyOf M X.n Γ tail (.match_ s arms)) t arms
         | _ => []
     | .interp parts => lowerArgsB M X Γ parts ++ concatB M parts.length
-    | .list t _ => [.nullOf (M.listStruct t)]
+    | .list t items =>
+        if items.isEmpty then [.nullOf (M.listStruct t)]
+        else
+          match M.listCons t with
+          | some f =>
+              lowerArgsB M X Γ items ++ [.nullOf (M.listStruct t)] ++
+                List.replicate items.length (.op (.call f))
+          | none => []
   def lowerArgsB (M : MCtx) (X : LCtx) (Γ : Nat → Option Ty) : List Expr → List BI
     | [] => []
     | e :: es => lowerB M X Γ false e ++ lowerArgsB M X Γ es
diff --git a/aver-cert/assets/wall/current/GrammarSound.lean b/aver-cert/assets/wall/current/GrammarSound.lean
index d602f93fd..c18dd032e 100644
--- a/aver-cert/assets/wall/current/GrammarSound.lean
+++ b/aver-cert/assets/wall/current/GrammarSound.lean
@@ -1372,12 +1372,26 @@ theorem tyOf_interp_inv {parts : List Expr} {T : Ty}
   · simp at h
 
 theorem tyOf_list_inv {t : Ty} {items : List Expr} {T : Ty}
-    (h : tyOf M n Γ tail (.list t items) = some T) : items = [] ∧ T = .list t := by
+    (h : tyOf M n Γ tail (.list t items) = some T) :
+    T = .list t ∧ (items = [] ∨ ∃ f ts, items.isEmpty = false ∧ M.listCons t = some f ∧
+      M.sigs f = some (consSig t) ∧ tysOf M n Γ items = some ts ∧ ∀ x ∈ ts, x = t) := by
   simp only [tyOf] at h
   split at h
-  · simp only [Option.some.injEq] at h
-    exact ⟨rfl, h.symm⟩
-  · simp at h
+  · rename_i he
+    simp only [Option.some.injEq] at h
+    exact ⟨h.symm, Or.inl (List.isEmpty_iff.mp he)⟩
+  · rename_i he
+    split at h
+    · rename_i f ts hf hts
+      split at h
+      · rename_i hc
+        simp only [Option.some.injEq] at h
+        refine ⟨h.symm, Or.inr ⟨f, ts, by simpa using he, hf, hc.1, hts, ?_⟩⟩
+        have h2 := hc.2
+        simp only [List.all_eq_true, decide_eq_true_eq] at h2
+        exact h2
+      · simp at h
+    · simp at h
 
 theorem tyOf_construct_inv {c : CtorTag} {ty : Ty} {args : List Expr} {T : Ty}
     (h : tyOf M n Γ tail (.construct c ty args) = some T) :
@@ -1879,6 +1893,98 @@ the nested argument lists and the arm shapes). The context fixes: the carrier sp
 host contracts at their indices, an arbitrary opaque `callee`, and a
 `Contract` for every callee the typing admits. -/
 
+/-! ## List literals
+
+A non-empty literal pushes its items, `ref.null`, and calls the cons helper
+once per item; the stack then holds the items in reverse, so the calls fold
+them into cons cells from the last one in. The helper is known only through
+its `Contract` and the model fact that its meaning is `List.prepend`. -/
+
+section ListLit
+variable {C : Nat} {S : CarrierSpec C} {M : MCtx}
+
+theorem eraseL_replicate (k : Nat) (i : WInstr) :
+    eraseL (List.replicate k (BI.op i)) = List.replicate k i := by
+  induction k with
+  | zero => simp [eraseL]
+  | succ k ih => simp [List.replicate_succ, eraseL, eraseI, ih]
+
+theorem consAll_foldl (t : Ty) (vs : List SVal) :
+    consAll t vs = vs.reverse.foldl (fun a v => SVal.cons t v a) (.nil t) := by
+  rw [List.foldl_reverse]
+  induction vs with
+  | nil => simp [consAll]
+  | cons v vs ih => simp [consAll, ih]
+
+theorem sreprL_append : ∀ {vs1 : List SVal} {ws1 : List WVal} {vs2 : List SVal}
+    {ws2 : List WVal}, SReprL S M vs1 ws1 → SReprL S M vs2 ws2 →
+      SReprL S M (vs1 ++ vs2) (ws1 ++ ws2)
+  | [], [], _, _, _, h2 => by simpa using h2
+  | _ :: _, _ :: _, _, _, h1, h2 => ⟨h1.1, sreprL_append h1.2 h2⟩
+  | [], _ :: _, _, _, h1, _ => by simp [SReprL] at h1
+  | _ :: _, [], _, _, h1, _ => by simp [SReprL] at h1
+
+theorem sreprL_reverse : ∀ {vs : List SVal} {ws : List WVal},
+    SReprL S M vs ws → SReprL S M vs.reverse ws.reverse
+  | [], [], _ => by simp [SReprL]
+  | _ :: _, _ :: _, h => by
+      simp only [List.reverse_cons]
+      exact sreprL_append (sreprL_reverse h.2) ⟨h.1, trivial⟩
+  | [], _ :: _, h => by simp [SReprL] at h
+  | _ :: _, [], h => by simp [SReprL] at h
+
+theorem hasTyL_mem {t : Ty} : ∀ {svs : List SVal} {ts : List Ty},
+    HasTyL M svs ts → (∀ x ∈ ts, x = t) → ∀ v ∈ svs, HasTy M v t
+  | [], _, _, _, v, hv => by simp at hv
+  | _ :: _, [], h, _, _, _ => by simp [HasTyL] at h
+  | a :: svs, x :: ts, h, hall, v, hv => by
+      rcases List.mem_cons.mp hv with rfl | hv
+      · have hx := hall x (by simp)
+        subst hx
+        exact h.1
+      · exact hasTyL_mem h.2 (fun y hy => hall y (by simp [hy])) v hv
+
+/-- `rs.length` calls of the cons helper over `acc :: wrs ++ st`, where `acc`
+    represents `tl` and `wrs` the items `rs` (last item first), fold them
+    into `tl` and leave one represented list on `st`. -/
+theorem consCalls_run {host : HostTbl} {ar : Nat → Option Nat} {callee : Callee}
+    {f : Nat} {t : Ty} {model : List SVal → Option SVal}
+    (hC : Contract S M host ar callee f (consSig t) model)
+    (hm : ∀ h tl sv, HasTy M tl (.list t) → model [h, tl] = some sv → sv = .cons t h tl) :
+    ∀ (rs : List SVal) (wrs : List WVal) (tl : SVal) (acc : WVal) (wl st : List WVal)
+      (out : Out),
+      SReprL S M rs wrs → (∀ v ∈ rs, HasTy M v t) → SRepr S M tl acc →
+      HasTy M tl (.list t) →
+      wRunF host ar callee (List.replicate rs.length (.call f)) wl (acc :: (wrs ++ st)) =
+        some out →
+      ∃ w, out = .ok wl (w :: st) ∧
+        SRepr S M (rs.foldl (fun a v => SVal.cons t v a) tl) w ∧
+        HasTy M (rs.foldl (fun a v => SVal.cons t v a) tl) (.list t)
+  | [], [], tl, acc, wl, st, out, _, _, hacc, htl, hrun => by
+      simp only [List.length_nil, List.replicate_zero, List.nil_append, wRunF,
+        Option.some.injEq] at hrun
+      subst hrun
+      exact ⟨acc, rfl, hacc, htl⟩
+  | [], _ :: _, _, _, _, _, _, hr, _, _, _, _ => by simp [SReprL] at hr
+  | _ :: _, [], _, _, _, _, _, hr, _, _, _, _ => by simp [SReprL] at hr
+  | r :: rs, w :: wrs, tl, acc, wl, st, out, hr, hall, hacc, htl, hrun => by
+      have har2 : ar f = some 2 := by simpa [consSig] using hC.2.1
+      have hpop : popArgs 2 (acc :: w :: (wrs ++ st)) = some ([w, acc], wrs ++ st) :=
+        popArgs_two w acc _
+      simp only [List.length_cons, List.replicate_succ, List.cons_append] at hrun
+      cases hc : callee f [w, acc] with
+      | none => simp [wRunF, hC.1, har2, hpop, hc] at hrun
+      | some r1 =>
+          simp only [wRunF, hC.1, har2, hpop, hc] at hrun
+          obtain ⟨sv, hmv, hsv, hT⟩ := hC.2.2 [r, tl] [w, acc] r1
+            ⟨hall r (by simp), htl, trivial⟩ ⟨hr.1, hacc, trivial⟩ hc
+          have hsv' := hm r tl sv htl hmv
+          subst hsv'
+          exact consCalls_run hC hm rs wrs (.cons t r tl) r1 wl st out hr.2
+            (fun v hv => hall v (by simp [hv])) hsv hT hrun
+
+end ListLit
+
 section Agreement
 variable {C : Nat} (S : CarrierSpec C)
   (box add sub mul cmp eq neg : List WVal → Option WVal)
@@ -1895,8 +2001,10 @@ variable {C : Nat} (S : CarrierSpec C)
   (F : Nat → List SVal → Option SVal)
   (hCallees : ∀ f sig, M.sigs f = some sig →
     Contract S M host ar callee f sig (F f))
+  (hConsF : ∀ t f, M.listCons t = some f → ∀ h tl sv, HasTy M tl (.list t) →
+    F f [h, tl] = some sv → sv = .cons t h tl)
   (X : LCtx)
-include Ctr hNegC hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R hCallees
+include Ctr hNegC hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R hCallees hConsF
 
 set_option hygiene false in
 /-- The size side condition of a recursive call in the agreement proofs: the
@@ -2962,10 +3070,28 @@ theorem agreement_step :
       subst hout
       exact ⟨.s bs, by simp [eval, hevs, hbs], by simp [HasTy], res_ok (by simp [SRepr]) hl1⟩
   | .list t items, hsz, Γ, env, tail, T, wl, st, out, hty, henv, hl, hrun => by
-      obtain ⟨rfl, rfl⟩ := tyOf_list_inv hty
-      simp [lowerW, lowerB, eraseL, eraseI, wRunF] at hrun
-      subst hrun
-      exact ⟨.nil t, by simp [eval], by simp [HasTy], res_ok (by simp [SRepr]) hl⟩
+      obtain ⟨rfl, hcase⟩ := tyOf_list_inv hty
+      rcases hcase with rfl | ⟨f, ts, hne, hf, hsig, hts, hall⟩
+      · simp [lowerW, lowerB, eraseL, eraseI, wRunF] at hrun
+        subst hrun
+        exact ⟨.nil t, by simp [eval], by simp [HasTy], res_ok (by simp [SRepr]) hl⟩
+      · simp only [lowerW, lowerB, hne, hf, Bool.false_eq_true, ↓reduceIte, eraseL_append,
+          List.append_assoc] at hrun
+        obtain ⟨o1, h1, hseq⟩ := run_split hrun
+        obtain ⟨svs, ws, wl1, rfl, hevs, hTs, hrep, hl1⟩ :=
+          agreementArgs items Γ env ts wl st o1 hts henv hl h1
+        have hlen : items.length = svs.reverse.length := by
+          rw [List.length_reverse, hasTyL_length hTs, tysOf_length hts]
+        simp only [seqOut, eraseL, eraseI, eraseL_replicate, List.cons_append,
+          List.nil_append, wRunF, hlen] at hseq
+        obtain ⟨w, rfl, hw, hT⟩ := consCalls_run (hCallees f (consSig t) hsig)
+          (hConsF t f hf) svs.reverse ws.reverse (.nil t) .null wl1 st out
+          (sreprL_reverse hrep) (fun v hv => hasTyL_mem hTs hall v (List.mem_reverse.mp hv))
+          (by simp [SRepr]) (by simp [HasTy]) hseq
+        refine ⟨consAll t svs, ?_, ?_, res_ok ?_ hl1⟩
+        · simp [eval, hne, hevs]
+        · rw [consAll_foldl]; exact hT
+        · rw [consAll_foldl]; exact hw
 
 theorem agreementArgs_step :
     ∀ (es : List Expr) (hsz : sizeOf es < n + 1) (Γ : Nat → Option Ty) (env : Nat → Option SVal) (Ts : List Ty)
@@ -3756,23 +3882,23 @@ theorem agreement_upto : ∀ n : Nat,
     obtain ⟨ih0, ih1, ih2, ih3, ih4, ih5, ih6, ih7, ih8⟩ := ih
     refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
     · intros
-      apply agreement_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
+      apply agreement_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
     · intros
-      apply agreementArgs_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
+      apply agreementArgs_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
     · intros
-      apply agreementIntArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
+      apply agreementIntArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
     · intros
-      apply agreementBoolArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
+      apply agreementBoolArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
     · intros
-      apply agreementOptArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
+      apply agreementOptArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
     · intros
-      apply agreementResArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
+      apply agreementResArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
     · intros
-      apply agreementVarArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
+      apply agreementVarArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
     · intros
-      apply agreementStrArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
+      apply agreementStrArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
     · intros
-      apply agreementTupArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
+      apply agreementTupArms_step S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X n ih0 ih1 ih2 ih3 ih4 ih5 ih6 ih7 ih8 _ ‹_› <;> assumption
 
 theorem agreement :
     ∀ (e : Expr) (Γ : Nat → Option Ty) (env : Nat → Option SVal) (tail : Bool) (T : Ty)
@@ -3786,7 +3912,7 @@ theorem agreement :
   := by
   intro e
   intros
-  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf e + 1)).1 e <;> first | assumption | exact Nat.lt_succ_self _
+  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf e + 1)).1 e <;> first | assumption | exact Nat.lt_succ_self _
 
 theorem agreementArgs :
     ∀ (es : List Expr) (Γ : Nat → Option Ty) (env : Nat → Option SVal) (Ts : List Ty)
@@ -3801,7 +3927,7 @@ theorem agreementArgs :
   := by
   intro es
   intros
-  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf es + 1)).2.1 es <;> first | assumption | exact Nat.lt_succ_self _
+  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf es + 1)).2.1 es <;> first | assumption | exact Nat.lt_succ_self _
 
 /-- The Int literal cascade: `sc` is the subject's code, re-run per literal
     arm; every run yields the same Int `x` (evaluation is pure). -/
@@ -3820,7 +3946,7 @@ theorem agreementIntArms :
   := by
   intro arms
   intros
-  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf arms + 1)).2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _
+  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf arms + 1)).2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _
 
 /-- The two-arm Bool match: one `if` on the subject's `i32`. -/
 theorem agreementBoolArms :
@@ -3835,7 +3961,7 @@ theorem agreementBoolArms :
   := by
   intro arms
   intros
-  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf arms + 1)).2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _
+  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf arms + 1)).2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _
 
 /-- The two-arm Option match over the subject held in the scratch. -/
 theorem agreementOptArms :
@@ -3850,7 +3976,7 @@ theorem agreementOptArms :
   := by
   intro arms
   intros
-  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf arms + 1)).2.2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _
+  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf arms + 1)).2.2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _
 
 /-- The two-arm Result match: `Ok` in the `then` (payload field 1), `Err` in
     the `else` (payload field 2). -/
@@ -3866,7 +3992,7 @@ theorem agreementResArms :
   := by
   intro arms
   intros
-  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf arms + 1)).2.2.2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _
+  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf arms + 1)).2.2.2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _
 
 /-- The user-variant `ref.test` cascade over the subject held in the
     scratch. `coversB` says some remaining arm reaches the subject's
@@ -3888,7 +4014,7 @@ theorem agreementVarArms :
   := by
   intro arms
   intros
-  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf arms + 1)).2.2.2.2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _
+  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf arms + 1)).2.2.2.2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _
 
 /-- The String literal cascade over the subject held in the scratch: each
     literal arm compares through `__wasmgc_string_eq`; `_` ends it. -/
@@ -3904,7 +4030,7 @@ theorem agreementStrArms :
   := by
   intro arms
   intros
-  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf arms + 1)).2.2.2.2.2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _
+  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf arms + 1)).2.2.2.2.2.2.2.1 arms <;> first | assumption | exact Nat.lt_succ_self _
 
 /-- The flat tuple destructure over the subject held in the scratch. -/
 theorem agreementTupArms :
@@ -3921,7 +4047,7 @@ theorem agreementTupArms :
   := by
   intro arms
   intros
-  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X (sizeOf arms + 1)).2.2.2.2.2.2.2.2 arms <;> first | assumption | exact Nat.lt_succ_self _
+  apply (agreement_upto S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X (sizeOf arms + 1)).2.2.2.2.2.2.2.2 arms <;> first | assumption | exact Nat.lt_succ_self _
 
 
 end Agreement
@@ -3940,6 +4066,37 @@ theorem groupModel_member (outer : Nat → Nat → List SVal → Option SVal)
       eval (groupModel outer G fuel) (argsEnv args) p.body := by
   simp [groupModel, hG]
 
+/-- The wall's own cons plan means `List.prepend` at every fuel. -/
+theorem groupModel_consPlan (outer : Nat → Nat → List SVal → Option SVal)
+    (G : Nat → Option FnPlan) {M : MCtx} {f : Nat} {p : FnPlan} {t : Ty}
+    (hG : G f = some p) (hb : p.body = consBody) :
+    ∀ k h tl sv, HasTy M tl (.list t) → groupModel outer G k f [h, tl] = some sv →
+      sv = .cons t h tl := by
+  intro k h tl sv htl hm
+  cases k with
+  | zero => simp [groupModel, hG] at hm
+  | succ k =>
+      rw [groupModel_member outer G hG, hb] at hm
+      cases tl <;> simp only [HasTy] at htl
+      · subst htl
+        simp [consBody, eval, evalArgs, argsEnv, builtinEval] at hm
+        subst hm; rfl
+      · obtain ⟨rfl, -, -⟩ := htl
+        simp [consBody, eval, evalArgs, argsEnv, builtinEval] at hm
+        subst hm; rfl
+
+theorem isConsPlan_body {p : FnPlan} (h : isConsPlan p = true) :
+    p.body = consBody := by
+  unfold isConsPlan at h
+  revert h
+  split
+  · rename_i heq
+    intro _
+    rw [heq]
+    rfl
+  · intro hb
+    cases hb
+
 theorem envTy_args {M : MCtx} {svs : List SVal} {ts : List Ty}
     (h : HasTyL M svs ts) : EnvTy M (argsEnv svs) (paramsΓ ts) := by
   intro i
@@ -3985,7 +4142,9 @@ theorem fn_certified_group {C : Nat} (S : CarrierSpec C)
       FnCertified S M code host f sig (fun fuel => outer fuel f))
     (hMem : ∀ f p, G f = some p →
       M.sigs f = some p.sig ∧ planTyped M p = true ∧ host f = none ∧
-        code f = some (fnCode M p)) :
+        code f = some (fnCode M p))
+    (hCons : ∀ t f, M.listCons t = some f → ∀ k h tl sv, HasTy M tl (.list t) →
+      groupModel outer G k f [h, tl] = some sv → sv = .cons t h tl) :
     ∀ f p, G f = some p →
       FnCertified S M code host f p.sig
         (fun fuel => groupModel outer G fuel f) := by
@@ -4047,6 +4206,7 @@ theorem fn_certified_group {C : Nat} (S : CarrierSpec C)
             obtain ⟨sv, hev, hT, hres⟩ := agreement S box add sub mul cmp eq neg Ctr hNegC host
               (fun g => (code g).map (·.arity)) (fun g as => wFuncN code host k g as) M
               hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R (groupModel outer G k) hCallees
+              (fun t g hg h tl sv htl hm => hCons t g hg k h tl sv htl hm)
               p.lctx p.body (paramsΓ p.sig.params) (argsEnv svs) true p.sig.ret
               (initLocals (fnCode M p) ws) [] o hty (envTy_args hTs) hLR hw
             have hm : groupModel outer G (k + 1) f svs = some sv := by
diff --git a/aver-cert/assets/wall/current/GrammarTotal.lean b/aver-cert/assets/wall/current/GrammarTotal.lean
index 593f3e967..988fc8285 100644
--- a/aver-cert/assets/wall/current/GrammarTotal.lean
+++ b/aver-cert/assets/wall/current/GrammarTotal.lean
@@ -334,6 +334,8 @@ variable {C : Nat} (S : CarrierSpec C)
   (F : Nat → List SVal → Option SVal)
   (hCallees : ∀ f sig, M.sigs f = some sig →
     Contract S M host ar callee f sig (F f))
+  (hConsF : ∀ t f, M.listCons t = some f → ∀ h tl sv, HasTy M tl (.list t) →
+    F f [h, tl] = some sv → sv = .cons t h tl)
   (X : LCtx)
   (hBoxT : ∀ k : Int, -(2 ^ 63 : Int) ≤ k → k < 2 ^ 63 → ∃ w, box [.i64v k] = some w)
   (hAddT : ∀ a b va vb, S.Repr a va → S.Repr b vb → ∃ w, add [va, vb] = some w)
@@ -345,7 +347,7 @@ variable {C : Nat} (S : CarrierSpec C)
   (hCallP : calls = true → ∀ g sig, mem g = true → M.sigs g = some sig →
     ∀ svs ws, HasTyL M (.i (n - 1) :: svs) sig.params →
       SReprL S M (.i (n - 1) :: svs) ws → ∃ r, callee g ws = some r)
-include Ctr hNegC hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R hCallees hBoxT hAddT hSubT hMulT
+include Ctr hNegC hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R hCallees hConsF hBoxT hAddT hSubT hMulT
   hSig hCallP
 
 mutual
@@ -381,13 +383,13 @@ theorem progress :
       · simp only [lowerW, lowerB, htl, hA, ↓reduceIte, eraseL_append, eraseL, eraseI]
         obtain ⟨o1, h1⟩ := progress l Γ env false .int wl st htl0 hΓ htl henv hl h0
         obtain ⟨sv1, _, hT1, hres1⟩ := agreement S box add sub mul cmp eq neg Ctr hNegC host ar
-          callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X l Γ env false .int
+          callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X l Γ env false .int
           wl st o1 htl henv hl h1
         obtain ⟨wl1, w1, rfl, hw1, hl1⟩ := res_false hres1
         obtain ⟨a, rfl⟩ := hasTy_int hT1
         obtain ⟨o2, h2⟩ := progress r Γ env false .int wl1 (w1 :: st) htr0 hΓ htr henv hl1 h0
         obtain ⟨sv2, _, hT2, hres2⟩ := agreement S box add sub mul cmp eq neg Ctr hNegC host ar
-          callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X r Γ env false .int
+          callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X r Γ env false .int
           wl1 (w1 :: st) o2 htr henv hl1 h2
         obtain ⟨wl2, w2, rfl, hw2, _⟩ := res_false hres2
         obtain ⟨b, rfl⟩ := hasTy_int hT2
@@ -417,7 +419,7 @@ theorem progress :
       obtain ⟨o1, h1⟩ := progressArgs args Γ env sig.params wl st hargs hΓ hts henv hl h0
       obtain ⟨svs, ws, wl1, rfl, hevs, hTs, hrep, _⟩ :=
         agreementArgs S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd
-          hSub hMul hNeg hCmp hEq R F hCallees X args Γ env sig.params wl st o1 hts henv hl h1
+          hSub hMul hNeg hCmp hEq R F hCallees hConsF X args Γ env sig.params wl st o1 hts henv hl h1
       obtain ⟨rest, rfl⟩ := descentHead_eq hdh
       have hd : eval F env (.binOp .sub (.local 0) (.literal (.int 1))) = some (.i (n - 1)) := by
         simp [eval, h0, intBin]
@@ -444,7 +446,7 @@ theorem progress :
       obtain ⟨o1, h1⟩ := progressArgs args Γ env sig.params wl st hargs hΓ hts henv hl h0
       obtain ⟨svs, ws, wl1, rfl, hevs, hTs, hrep, _⟩ :=
         agreementArgs S box add sub mul cmp eq neg Ctr hNegC host ar callee M hCarrier hBox hAdd
-          hSub hMul hNeg hCmp hEq R F hCallees X args Γ env sig.params wl st o1 hts henv hl h1
+          hSub hMul hNeg hCmp hEq R F hCallees hConsF X args Γ env sig.params wl st o1 hts henv hl h1
       obtain ⟨rest, rfl⟩ := descentHead_eq hdh
       have hd : eval F env (.binOp .sub (.local 0) (.literal (.int 1))) = some (.i (n - 1)) := by
         simp [eval, h0, intBin]
@@ -494,7 +496,7 @@ theorem progressArgs :
       simp only [lowerArgsW, lowerArgsB, eraseL_append]
       obtain ⟨o1, h1⟩ := progress e Γ env false t wl st htot.1 hΓ hte henv hl h0
       obtain ⟨sv, _, _, hres⟩ := agreement S box add sub mul cmp eq neg Ctr hNegC host ar
-        callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees X e Γ env false t
+        callee M hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R F hCallees hConsF X e Γ env false t
         wl st o1 hte henv hl h1
       obtain ⟨wl1, w, rfl, _, hl1⟩ := res_false hres
       obtain ⟨o2, h2⟩ := progressArgs es Γ env ts wl1 (w :: st) htot.2 hΓ htes henv hl1 h0
@@ -574,6 +576,8 @@ theorem fn_certified_total {C : Nat} (S : CarrierSpec C)
     (hMem : ∀ f p, G f = some p →
       M.sigs f = some p.sig ∧ planTyped M p = true ∧ host f = none ∧
         code f = some (fnCode M p))
+    (hCons : ∀ t f, M.listCons t = some f → ∀ k h tl sv, HasTy M tl (.list t) →
+      groupModel outer G k f [h, tl] = some sv → sv = .cons t h tl)
     (hBoxT : ∀ k : Int, -(2 ^ 63 : Int) ≤ k → k < 2 ^ 63 → ∃ w, box [.i64v k] = some w)
     (hAddT : ∀ a b va vb, S.Repr a va → S.Repr b vb → ∃ w, add [va, vb] = some w)
     (hSubT : ∀ a b va vb, S.Repr a va → S.Repr b vb → ∃ w, sub [va, vb] = some w)
@@ -585,7 +589,7 @@ theorem fn_certified_total {C : Nat} (S : CarrierSpec C)
       FnCertified S M code host f p.sig (fun fuel => groupModel outer G fuel f) ∧
         FnTotal S M code host f p.sig (fun fuel => groupModel outer G fuel f) := by
   have hCert := fn_certified_group S box add sub mul cmp eq neg Ctr hNegC code host M hCarrier
-    hBox hAdd hSub hMul hNeg hCmp hEq R G outer hOuter hMem
+    hBox hAdd hSub hMul hNeg hCmp hEq R G outer hOuter hMem hCons
   have hSigOf : ∀ f p, G f = some p → M.sigs f = some p.sig := fun f p h => (hMem f p h).1
   have hSig : ∀ g sig, mem g = true → M.sigs g = some sig → sig.ret = .int ∨ sig.ret = .bool := by
     intro g sig hg hs
@@ -650,7 +654,8 @@ theorem fn_certified_total {C : Nat} (S : CarrierSpec C)
           (ar := fun g => (code g).map (·.arity)) (callee := fun g as => wFuncN code host m g as)
           (M := M) (hCarrier := hCarrier) (hBox := hBox) (hAdd := hAdd) (hSub := hSub)
           (hMul := hMul) (hNeg := hNeg) (hCmp := hCmp) (hEq := hEq) (R := R)
-          (F := groupModel outer G m) (hCallees := hCallees) (X := p.lctx) (hBoxT := hBoxT)
+          (F := groupModel outer G m) (hCallees := hCallees)
+          (hConsF := fun t g hg h tl sv htl hm => hCons t g hg m h tl sv htl hm) (X := p.lctx) (hBoxT := hBoxT)
           (hAddT := hAddT) (hSubT := hSubT) (mulOk := mulOk) (hMulT := hMulT) (mem := mem)
           (calls := false) (n := n) (hSig := hSig) (hCallP := fun h => by cases h)
           base _ _ true p.sig.ret _ [] hbase hΓ hbty henv hLR h0
@@ -671,7 +676,8 @@ theorem fn_certified_total {C : Nat} (S : CarrierSpec C)
           (ar := fun g => (code g).map (·.arity)) (callee := fun g as => wFuncN code host m g as)
           (M := M) (hCarrier := hCarrier) (hBox := hBox) (hAdd := hAdd) (hSub := hSub)
           (hMul := hMul) (hNeg := hNeg) (hCmp := hCmp) (hEq := hEq) (R := R)
-          (F := groupModel outer G m) (hCallees := hCallees) (X := p.lctx) (hBoxT := hBoxT)
+          (F := groupModel outer G m) (hCallees := hCallees)
+          (hConsF := fun t g hg h tl sv htl hm => hCons t g hg m h tl sv htl hm) (X := p.lctx) (hBoxT := hBoxT)
           (hAddT := hAddT) (hSubT := hSubT) (mulOk := mulOk) (hMulT := hMulT) (mem := mem)
           (calls := true) (n := n) (hSig := hSig) (hCallP := hCallP)
           step _ _ true p.sig.ret _ [] hstep hΓ hsty henv hLR h0
@@ -679,6 +685,7 @@ theorem fn_certified_total {C : Nat} (S : CarrierSpec C)
     obtain ⟨sv, _, _, hres⟩ := agreement S box add sub mul cmp eq neg Ctr hNegC host
       (fun g => (code g).map (·.arity)) (fun g as => wFuncN code host m g as) M
       hCarrier hBox hAdd hSub hMul hNeg hCmp hEq R (groupModel outer G m) hCallees
+      (fun t g hg h tl sv htl hm => hCons t g hg m h tl sv htl hm)
       p.lctx p.body (paramsΓ p.sig.params) (argsEnv (.i n :: tl)) true p.sig.ret
       (initLocals (fnCode M p) (w0 :: ws')) [] out hty henv hLR hout
     unfold wFuncN
@@ -734,6 +741,8 @@ theorem fn_certified_total_of_check {C : Nat} (S : CarrierSpec C)
     (hMem : ∀ f p, G f = some p →
       M.sigs f = some p.sig ∧ planTyped M p = true ∧ host f = none ∧
         code f = some (fnCode M p))
+    (hCons : ∀ t f, M.listCons t = some f → ∀ k h tl sv, HasTy M tl (.list t) →
+      groupModel outer G k f [h, tl] = some sv → sv = .cons t h tl)
     (hBoxT : ∀ k : Int, -(2 ^ 63 : Int) ≤ k → k < 2 ^ 63 → ∃ w, box [.i64v k] = some w)
     (hAddT : ∀ a b va vb, S.Repr a va → S.Repr b vb → ∃ w, add [va, vb] = some w)
     (hSubT : ∀ a b va vb, S.Repr a va → S.Repr b vb → ∃ w, sub [va, vb] = some w)
@@ -743,7 +752,7 @@ theorem fn_certified_total_of_check {C : Nat} (S : CarrierSpec C)
         FnTotal S M code host f p.sig (fun fuel => groupModel outer G fuel f) := by
   obtain ⟨_, hall⟩ := checkTermGroup_spec hck
   refine fn_certified_total S box add sub mul cmp eq neg Ctr hNegC code host M hCarrier hBox hAdd
-    hSub hMul hNeg hCmp hEq R G outer hOuter hMem hBoxT hAddT hSubT (role == .mul)
+    hSub hMul hNeg hCmp hEq R G outer hOuter hMem hCons hBoxT hAddT hSubT (role == .mul)
     (fun h => hMulT (by simpa using h)) (memOf ms) ?_ ?_
   · intro g hg
     obtain ⟨m, hm, hmg⟩ := List.any_eq_true.mp hg
diff --git a/aver-cert/assets/wall/current/SchemaCore.lean b/aver-cert/assets/wall/current/SchemaCore.lean
index cef070fa4..fcfac131d 100644
--- a/aver-cert/assets/wall/current/SchemaCore.lean
+++ b/aver-cert/assets/wall/current/SchemaCore.lean
@@ -67,6 +67,10 @@ structure TypeTable where
   opaques : List (Nat × Nat)
   /-- The passive data segment holding each string literal's bytes. -/
   strSegs : List (List Nat × Nat)
+  /-- The cons helper of each `List<T>` a non-empty literal builds: the
+      function the literal calls once per item. The acceptance pins its plan
+      to the wall's cons plan (`Grammar.isConsPlan`). -/
+  listCons : List (Ty × Nat) := []
 deriving Repr
 
 /-- One planned function: the plan is the function's MIR body printed 1:1
diff --git a/aver-cert/assets/wall/current/TypeTable.lean b/aver-cert/assets/wall/current/TypeTable.lean
index 56cbf0bbb..9c785a5ac 100644
--- a/aver-cert/assets/wall/current/TypeTable.lean
+++ b/aver-cert/assets/wall/current/TypeTable.lean
@@ -103,7 +103,8 @@ def mctxOf (s : Subject) (tt : TypeTable) (fns : List FnEntry) : MCtx :=
     divmod := idxOr 23 (roleOf s.hostRoleTable (·.divmod))
     vecStruct := lookupTy 20 tt.vecs
     listStruct := lookupTy 21 tt.lists
-    opaqueStruct := lookupNat 22 tt.opaques }
+    opaqueStruct := lookupNat 22 tt.opaques
+    listCons := fun t => (tt.listCons.find? fun x => decide (x.1 = t)).map (·.2) }
 
 /-! ## The opening rec group, raw and decoded
 
diff --git a/aver-cert/src/engine/plan.rs b/aver-cert/src/engine/plan.rs
index b376f75a0..b4a0309c2 100644
--- a/aver-cert/src/engine/plan.rs
+++ b/aver-cert/src/engine/plan.rs
@@ -175,6 +175,10 @@ pub struct PlanTypeTable {
     pub lists: Vec<(PlanTy, u32)>,
     pub opaques: Vec<(u32, u32)>,
     pub str_segs: Vec<(Vec<u8>, u32)>,
+    /// The cons helper of each `List<T>` a non-empty literal builds
+    /// (`Schema.TypeTable.listCons`): the function the literal calls once per
+    /// item, whose plan must be exactly [`FnPlan::cons`].
+    pub list_cons: Vec<(PlanTy, u32)>,
 }
 
 /// One user function as the compiler printed it: its wasm function index, its
@@ -445,6 +449,21 @@ impl PlanExpr {
 }
 
 impl FnPlan {
+    /// `Grammar.isConsPlan`'s plan: the cons helper of `List<t>`, one
+    /// `List.prepend` over its two parameters and no declared local.
+    pub fn cons(t: &PlanTy) -> FnPlan {
+        FnPlan {
+            params: vec![t.clone(), PlanTy::List(Box::new(t.clone()))],
+            ret: PlanTy::List(Box::new(t.clone())),
+            nslots: 2,
+            locals: Vec::new(),
+            body: PlanExpr::Call(
+                PlanCallee::Builtin(PlanBuiltin::ListPrepend),
+                vec![PlanExpr::Local(0), PlanExpr::Local(1)],
+            ),
+        }
+    }
+
     /// The Lean `Grammar.FnPlan` term.
     pub fn lean(&self) -> String {
         format!(
@@ -618,13 +637,23 @@ impl PlanTypeTable {
         let lists = field("lists", "Ty × Nat", &pairs(&self.lists));
         let opaques = field("opaques", "Nat × Nat", &opaques);
         let segs = field("strSegs", "List Nat × Nat", &segs);
+        // Written only when present: the wall's default is the empty list,
+        // so a module without list literals renders as before.
+        let cons = if self.list_cons.is_empty() {
+            String::new()
+        } else {
+            format!(
+                ",\n    listCons := {}",
+                field("listCons", "Ty × Nat", &pairs(&self.list_cons))
+            )
+        };
         let pieces = decls
             .lines()
             .filter_map(|line| line.strip_prefix("def "))
             .filter_map(|rest| rest.split_once(" :").map(|(n, _)| n.to_string()))
             .collect();
         let text = format!(
-            "{decls}def {name} : TypeTable :=\n  {{ carrier := {}, mag := {}, str := {}, strVec := {},\n    records := {records},\n    sums := {sums},\n    options := {options}, results := {results},\n    vecs := {vecs}, lists := {lists}, opaques := {opaques},\n    strSegs := {segs} }}\n\n",
+            "{decls}def {name} : TypeTable :=\n  {{ carrier := {}, mag := {}, str := {}, strVec := {},\n    records := {records},\n    sums := {sums},\n    options := {options}, results := {results},\n    vecs := {vecs}, lists := {lists}, opaques := {opaques},\n    strSegs := {segs}{cons} }}\n\n",
             lean_opt_nat(self.carrier),
             lean_opt_nat(self.mag),
             lean_opt_nat(self.str_),
diff --git a/aver-cert/src/engine/plan_check.rs b/aver-cert/src/engine/plan_check.rs
index 782d114e7..57b97623d 100644
--- a/aver-cert/src/engine/plan_check.rs
+++ b/aver-cert/src/engine/plan_check.rs
@@ -137,6 +137,11 @@ impl<'a> MCtx<'a> {
         idx_or(21, self.tt.lists.iter().find(|l| &l.0 == t).map(|l| l.1))
     }
 
+    /// `MCtx.listCons`: the declared cons helper of `List<t>`.
+    fn list_cons(&self, t: &PlanTy) -> Option<u32> {
+        self.tt.list_cons.iter().find(|l| &l.0 == t).map(|l| l.1)
+    }
+
     fn opaque_struct(&self, tid: u32) -> u64 {
         idx_or(22, self.tt.opaques.iter().find(|o| o.0 == tid).map(|o| o.1))
     }
@@ -469,7 +474,16 @@ impl MCtx<'_> {
             }
             PlanExpr::Construct(c, ty, args) => self.ctor_ty(*c, ty, &self.tys_of(n, g, args)?),
             PlanExpr::Interp(parts) => all_str(&self.tys_of(n, g, parts)?).then_some(PlanTy::Str),
-            PlanExpr::List(t, items) => items.is_empty().then(|| PlanTy::List(Box::new(t.clone()))),
+            PlanExpr::List(t, items) => {
+                let lt = PlanTy::List(Box::new(t.clone()));
+                if items.is_empty() {
+                    return Some(lt);
+                }
+                let f = self.list_cons(t)?;
+                let ts = self.tys_of(n, g, items)?;
+                let sig_ok = self.sigs.get(&f) == Some(&(vec![t.clone(), lt.clone()], lt.clone()));
+                (sig_ok && ts.iter().all(|x| x == t)).then_some(lt)
+            }
             PlanExpr::Match(s, arms) => match self.ty_of(n, g, false, s)? {
                 PlanTy::Int => {
                     matches!(arms.first(), Some((PlanPat::LitInt(_), _))).then_some(())?;
@@ -1358,7 +1372,18 @@ impl MCtx<'_> {
                 out.extend(self.concat(parts.len()));
                 out
             }
-            PlanExpr::List(t, _) => vec![BI::NullOf(self.list_struct(t))],
+            PlanExpr::List(t, items) => {
+                if items.is_empty() {
+                    return vec![BI::NullOf(self.list_struct(t))];
+                }
+                let Some(f) = self.list_cons(t) else {
+                    return vec![];
+                };
+                let mut out = self.lower_args(x, g, items);
+                out.push(BI::NullOf(self.list_struct(t)));
+                out.extend(items.iter().map(|_| BI::Op(WI::Call(u64::from(f)))));
+                out
+            }
         }
     }
 
@@ -1750,7 +1775,7 @@ fn lowered_calls(bs: &[BI], out: &mut Vec<u64>) {
 /// `AcceptedArtifact.callTargets`.
 fn call_targets(e: &PlanExpr, out: &mut Vec<u32>) {
     match e {
-        PlanExpr::Literal(_) | PlanExpr::Local(_) | PlanExpr::List(_, _) => {}
+        PlanExpr::Literal(_) | PlanExpr::Local(_) => {}
         PlanExpr::Let(_, v, b) => {
             call_targets(v, out);
             call_targets(b, out);
@@ -1762,7 +1787,8 @@ fn call_targets(e: &PlanExpr, out: &mut Vec<u32>) {
         PlanExpr::Call(_, args)
         | PlanExpr::RecordCreate(_, args)
         | PlanExpr::Construct(_, _, args)
-        | PlanExpr::Interp(args) => args.iter().for_each(|a| call_targets(a, out)),
+        | PlanExpr::Interp(args)
+        | PlanExpr::List(_, args) => args.iter().for_each(|a| call_targets(a, out)),
         PlanExpr::BinOp(_, l, r) => {
             call_targets(l, out);
             call_targets(r, out);
@@ -1780,6 +1806,55 @@ fn call_targets(e: &PlanExpr, out: &mut Vec<u32>) {
     }
 }
 
+/// The element types of the non-empty list literals of a plan: each one
+/// calls its type's cons helper (`MCtx.listCons`), which must therefore be
+/// offered with the plan.
+fn literal_list_types(e: &PlanExpr, out: &mut Vec<PlanTy>) {
+    match e {
+        PlanExpr::Literal(_) | PlanExpr::Local(_) => {}
+        PlanExpr::Let(_, v, b) | PlanExpr::BinOp(_, v, b) => {
+            literal_list_types(v, out);
+            literal_list_types(b, out);
+        }
+        PlanExpr::List(t, items) => {
+            if !items.is_empty() {
+                out.push(t.clone());
+            }
+            items.iter().for_each(|a| literal_list_types(a, out));
+        }
+        PlanExpr::Call(_, args)
+        | PlanExpr::TailCall(_, args)
+        | PlanExpr::RecordCreate(_, args)
+        | PlanExpr::Construct(_, _, args)
+        | PlanExpr::Interp(args) => args.iter().for_each(|a| literal_list_types(a, out)),
+        PlanExpr::Neg(x) | PlanExpr::Project(_, _, x) => literal_list_types(x, out),
+        PlanExpr::If(c, t, el) => {
+            literal_list_types(c, out);
+            literal_list_types(t, out);
+            literal_list_types(el, out);
+        }
+        PlanExpr::Match(s, arms) => {
+            literal_list_types(s, out);
+            arms.iter().for_each(|(_, b)| literal_list_types(b, out));
+        }
+    }
+}
+
+/// The functions a plan runs: its calls (`call_targets`) and the cons
+/// helpers of its non-empty list literals.
+fn plan_targets(tt: &PlanTypeTable, p: &FnPlan) -> Vec<u32> {
+    let mut out = Vec::new();
+    call_targets(&p.body, &mut out);
+    let mut tys = Vec::new();
+    literal_list_types(&p.body, &mut tys);
+    for t in tys {
+        if let Some((_, f)) = tt.list_cons.iter().find(|l| l.0 == t) {
+            out.push(*f);
+        }
+    }
+    out
+}
+
 /// `GrammarLower.exprLits`: every string literal a plan lowers to
 /// `array.new_data`.
 fn string_lits<'e>(e: &'e PlanExpr, out: &mut Vec<&'e [u8]>) {
diff --git a/aver-cert/src/engine/produce.rs b/aver-cert/src/engine/produce.rs
index 5c569c3c4..fbeaa94e2 100644
--- a/aver-cert/src/engine/produce.rs
+++ b/aver-cert/src/engine/produce.rs
@@ -430,6 +430,12 @@ impl Cited {
                 .filter(|s| self.segs.contains(&s.0))
                 .cloned()
                 .collect(),
+            list_cons: tt
+                .list_cons
+                .iter()
+                .filter(|l| has(PlanTy::List(Box::new(l.0.clone()))))
+                .cloned()
+                .collect(),
         }
     }
 }
@@ -505,8 +511,7 @@ fn check_candidate(
     plan: &FnPlan,
     candidates: &BTreeSet<u32>,
 ) -> Option<String> {
-    let mut targets = Vec::new();
-    call_targets(&plan.body, &mut targets);
+    let targets = plan_targets(m.tt, plan);
     if let Some(t) = targets.iter().find(|t| !candidates.contains(t)) {
         return Some(format!("calls function {t}, which has no certified plan"));
     }
@@ -602,6 +607,18 @@ pub fn analyze(
 
     let mut types = plans.types.clone();
     confirm_type_table(&facts, &mut types);
+    // A cons helper is never a user function: an index the compiler also
+    // printed a user plan for is dropped (its literals then decline).
+    types
+        .list_cons
+        .retain(|(_, f)| !plans.fns.iter().any(|p| p.func_idx == *f));
+    // The cons helper of each literal's list type is offered with the wall's
+    // own cons plan; the byte check below confirms the helper is exactly it.
+    let cons_plans: Vec<(u32, FnPlan)> = types
+        .list_cons
+        .iter()
+        .map(|(t, f)| (*f, FnPlan::cons(t)))
+        .collect();
 
     let mut reasons: BTreeMap<u32, String> = BTreeMap::new();
     let mut plan_of: BTreeMap<u32, &FnPlan> = BTreeMap::new();
@@ -615,6 +632,9 @@ pub fn analyze(
             }
         }
     }
+    for (f, p) in &cons_plans {
+        plan_of.entry(*f).or_insert(p);
+    }
     let mut candidates: BTreeSet<u32> = plan_of.keys().copied().collect();
     loop {
         let fns: Vec<(u32, &FnPlan)> = candidates.iter().map(|f| (*f, plan_of[f])).collect();
@@ -638,8 +658,7 @@ pub fn analyze(
     // reaches.
     let mut edges: BTreeMap<u32, Vec<u32>> = BTreeMap::new();
     for f in &candidates {
-        let mut t = Vec::new();
-        call_targets(&plan_of[f].body, &mut t);
+        let mut t = plan_targets(&types, plan_of[f]);
         t.sort_unstable();
         t.dedup();
         edges.insert(*f, t);
@@ -758,7 +777,11 @@ pub fn analyze(
     let mut cited = Cited::default();
     entries.iter().for_each(|e| cited.plan(&e.plan));
     cited.close(&types);
-    let types = cited.restrict(&types);
+    let mut types = cited.restrict(&types);
+    // `AcceptedArtifact.consPinned`: every declared cons helper is planned.
+    types
+        .list_cons
+        .retain(|(_, f)| entries.iter().any(|e| e.func_idx == *f));
 
     let declined: Vec<(String, String)> = export_name
         .iter()
diff --git a/aver-cert/src/engine/source_bridges.rs b/aver-cert/src/engine/source_bridges.rs
index 8e45a3c95..a1c1f8fd6 100644
--- a/aver-cert/src/engine/source_bridges.rs
+++ b/aver-cert/src/engine/source_bridges.rs
@@ -1493,7 +1493,8 @@ const STEP_EVAL: &str = "AverCert.Grammar.eval, AverCert.Grammar.evalArgs, arms_
      _root_.false_and, _root_.and_false, AverCert.GrammarBridge.decodeStr_strBytes, \
      _root_.Option.bind_some, _root_.Function.comp_apply, strBytes_eq_iff, strBytes_beq, \
      Nat.reduceEqDiff, Int.reduceEq, ← AverCert.GrammarBridge.strBytes_append, \
-     _root_.List.append_nil, str_toString, str_hadd";
+     _root_.List.append_nil, str_toString, str_hadd, _root_.List.isEmpty_nil, \
+     _root_.List.isEmpty_cons, _root_.Bool.false_eq_true, AverCert.Grammar.consAll";
 
 /// Normal forms a leaf closes with, on top of the source definition.
 const STEP_NORM: &str = "_root_.bne, dec_eq_beq, dec_ne_bne, strBytes_eq_iff, str_toString, \
diff --git a/aver-cert/src/format.rs b/aver-cert/src/format.rs
index 6540755c8..9071d838a 100644
--- a/aver-cert/src/format.rs
+++ b/aver-cert/src/format.rs
@@ -180,7 +180,7 @@ pub const FN_CLAIM_DISCHARGE_THEOREM: &str = "AcceptanceSoundness.fn_claim_disch
 
 /// Identity of the exact checker-owned Lean wall shipped by this release.
 pub const CURRENT_WALL_ID: &str =
-    "sha256:5168df0c3f4da023c53a9c929e081803c559ed2e22fc6a103f8fb827745ae4d9";
+    "sha256:318de1883be91114ed8a396835aea6d183ac9acc4903c7c99e72b023a20ce2c6";
 
 /// Complete host-import surface admitted by the wasm-gc certificate format.
 ///
diff --git a/docs/certificate-format.md b/docs/certificate-format.md
index f846521ee..1dd56a2a1 100644
--- a/docs/certificate-format.md
+++ b/docs/certificate-format.md
@@ -29,7 +29,7 @@ Schema history, one line per bump. Each bump is exact-match, so a verifier of ve
 - 8: the `sourceBridges` array and the `bridges` key of every law entry.
 - 9: every obligation is stated over one plan grammar. The Lean manifest carries one plan list (`fnPlans`), each entry a function's optimized MIR body printed 1:1, and a declared type layout (`types`) that the wall confirms against the type and data sections. The obligations are exactly the ones the wall derives from the plans, and their model is the plan's fuel-indexed meaning. Every certified export reports the class `source-plan-v1` with wall-derived facets. `hostRoleTable` gained the `divmod` key. Source-bridges are restated over the plan grammar, in two statement kinds (section 9).
 
-The wall identity is computed, not assigned. It is the SHA-256 of a domain-separated, sorted, length-framed encoding of every wall source file plus the toolchain pin, written as `sha256:` and 64 lowercase hex digits. The encoding is: the ASCII bytes `aver-certificate-wall\0v1\0`; the file count as a big-endian `u64`; then, for each file in ascending filename order, the filename length as a big-endian `u64`, the filename bytes, the contents length as a big-endian `u64`, and the contents. The file set is the 24 embedded `.lean` wall sources plus one synthetic file named `lean-toolchain`, whose contents are the embedded toolchain file verbatim: the ASCII bytes `leanprover/lean4:v4.34.0` and one trailing newline. The newline is hashed; a reimplementation that hashes the trimmed pin computes a different identity. The current embedded wall identity is `sha256:5168df0c3f4da023c53a9c929e081803c559ed2e22fc6a103f8fb827745ae4d9` (`CURRENT_WALL_ID` in `format.rs`). The reference verifier recomputes the digest over its embedded sources on first use and aborts if it differs from the compiled-in constant. A reimplementation MUST resolve `format.wall_id` only against source sets whose recomputed identity matches byte for byte, never by name, path or prefix.
+The wall identity is computed, not assigned. It is the SHA-256 of a domain-separated, sorted, length-framed encoding of every wall source file plus the toolchain pin, written as `sha256:` and 64 lowercase hex digits. The encoding is: the ASCII bytes `aver-certificate-wall\0v1\0`; the file count as a big-endian `u64`; then, for each file in ascending filename order, the filename length as a big-endian `u64`, the filename bytes, the contents length as a big-endian `u64`, and the contents. The file set is the 24 embedded `.lean` wall sources plus one synthetic file named `lean-toolchain`, whose contents are the embedded toolchain file verbatim: the ASCII bytes `leanprover/lean4:v4.34.0` and one trailing newline. The newline is hashed; a reimplementation that hashes the trimmed pin computes a different identity. The current embedded wall identity is `sha256:318de1883be91114ed8a396835aea6d183ac9acc4903c7c99e72b023a20ce2c6` (`CURRENT_WALL_ID` in `format.rs`). The reference verifier recomputes the digest over its embedded sources on first use and aborts if it differs from the compiled-in constant. A reimplementation MUST resolve `format.wall_id` only against source sets whose recomputed identity matches byte for byte, never by name, path or prefix.
 
 > **TODO-decision: freeze criteria.** Neither `format.version = 1` nor `schema_version = 9` is frozen. What counts as a compatible extension, and whether a frozen schema admits additive optional fields, is open. Until a freeze, every schema change bumps `schema_version`, and verifiers reject non-matching versions exactly.
 
@@ -231,7 +231,7 @@ A plan (`Grammar.FnPlan`) is `{sig, nslots, locals, body}`: the signature, the r
 - `match_` with the arm shapes the emitter lowers: an Int literal cascade with a catch-all last, a two-arm Bool match, a two-arm Option or Result match, a user-variant `ref.test` cascade of two or more arms covering every constructor, a String literal cascade with `_` last, a single-arm flat tuple destructure, and a two-arm List match (`[]` and `[head, ..tail]` in either order, or either one first and `_` second);
 - `construct` for user constructors and `Some`, `None`, `Ok`, `Err`, carrying the node's type;
 - `interp` whose parts are all Strings;
-- `list t []`, the empty list.
+- `list t items`, a list literal: `[]`, or a non-empty literal whose items all have the element type `t`, when the type table declares the `List<t>` cons helper (`listCons`) and the helper's planned signature is `(t, List<t>) -> List<t>`.
 
 The printer also declines a function that declares effects, uses raw i64 slots, has no MIR body, or whose parameters are not slots `0..n`.
 
@@ -245,7 +245,7 @@ The printer also declines a function that declares effects, uses raw i64 slots,
 
 `GrammarLower` is a port of the wasm-gc MIR emitter (`src/codegen/wasm_gc/body/from_mir/`) for the admitted nodes. One lowering produces both the instruction tree the interpreter runs (`fnCode`) and the code-entry bytes the acceptance compares (`codeEntryBytes`, locals vector and size prefix included), so the proved code and the pinned bytes come from one tree.
 
-Every lowering choice is a function of the plan and the declarations, never a plan flag: an Int comparison against a literal looks for the literal on the left first and flips the operator, re-emits a bare local operand and stashes any other operand in the const-compare scratch local; the scratch locals sit after the resolver slots in the order the emitter reserves them; an `if` takes its block type from the then-branch type; a List match tests the stashed subject with `ref.is_null`, runs the `[]` arm in `then`, and reads the head (field 0) and tail (field 1) of the cons struct into the cons arm's binders in `else`; a `tailCall` is `return_call` and a `call` is `call`, as MIR marked them. A reimplementation MUST compute both images inside the kernel and MUST NOT replace them with an out-of-kernel lowering.
+Every lowering choice is a function of the plan and the declarations, never a plan flag: an Int comparison against a literal looks for the literal on the left first and flips the operator, re-emits a bare local operand and stashes any other operand in the const-compare scratch local; the scratch locals sit after the resolver slots in the order the emitter reserves them; an `if` takes its block type from the then-branch type; a List match tests the stashed subject with `ref.is_null`, runs the `[]` arm in `then`, and reads the head (field 0) and tail (field 1) of the cons struct into the cons arm's binders in `else`; a non-empty list literal pushes its items in order, then `ref.null` of the cons struct, then calls the declared cons helper once per item, so the last item is consed first; a `tailCall` is `return_call` and a `call` is `call`, as MIR marked them. A reimplementation MUST compute both images inside the kernel and MUST NOT replace them with an out-of-kernel lowering.
 
 An index the declarations do not provide lowers to `TypeTable.absent k`, a value outside the u32 range that no encoder accepts, so a plan citing an undeclared type or helper cannot match any code entry.
 
@@ -275,7 +275,7 @@ For each `FnEntry` (`entryAccepted`):
 
 ### 7.3 Type table and data segments
 
-The type table (`Schema.TypeTable`) declares the carrier and its magnitude array, `$string`, `Vector<String>`, records and tuples (`RecordDecl {tid, struct, fields}`), sums (`SumDecl {tid, root, ctors}`), `Option`, `Result`, `Vector` and `List` instantiations, opaque pass-through types, and the data segment of each string literal. `TypeTable.typeTableConfirmed` requires:
+The type table (`Schema.TypeTable`) declares the carrier and its magnitude array, `$string`, `Vector<String>`, records and tuples (`RecordDecl {tid, struct, fields}`), sums (`SumDecl {tid, root, ctors}`), `Option`, `Result`, `Vector` and `List` instantiations, opaque pass-through types, the data segment of each string literal, and the cons helper of each `List` instantiation a literal builds (`listCons`, absent when empty). `TypeTable.typeTableConfirmed` requires:
 
 - the type section decodes, and its first rectype is an explicit rec group (`0x4e`); every struct and array the table names is an entry of that group;
 - `keysUnique`: record and sum type ids are unique;
@@ -288,6 +288,8 @@ The type table (`Schema.TypeTable`) declares the carrier and its magnitude array
 
 `TypeTable.declsWellFormed` requires the declarations to be inhabited: `eqref` appears only as the subject-scratch local; no chain of one-field records loops; and every declared record and sum, and every parameter and result type of every plan, has a finite value (`inhabited`, proved sound by `inhabTy_sound`). Without it an obligation over an uninhabitable type would hold of any code.
 
+`AcceptedArtifact.consPinned` requires every declared cons helper to be a planned function whose plan is the wall's cons plan (`Grammar.isConsPlan`: its body is `List.prepend(local 0, local 1)`). The typing of a literal of `List<t>` requires that helper's planned signature to be `(t, List<t>) -> List<t>`, and its code entry is pinned like every other plan's, so a literal's calls reach a function whose meaning is `List.prepend`, proved rather than assumed.
+
 A record's `tid` is the plans' own name for a type and is declared, not bound: a wrong id renames a confirmed layout and cannot change it.
 
 ### 7.4 Runtime contracts
@@ -488,7 +490,7 @@ A certificate does not expire. It verifies against a verifier that embeds the wa
 | 4.4 Wasip2 envelope | `aver-cert/assets/wall/current/Wasip2Envelope.lean`, `aver-cert/assets/wall/current/AcceptedArtifactCore.lean` (`artifactEnvelopeAccepted`), `aver-cert/src/verifier.rs` (`prepare_wasip2_artifact_with_declared_envelope`) |
 | 5 Statement | `aver-cert/assets/wall/current/SchemaCore.lean` (`TypeTable`, `FnEntry`, `HostFns`, `HostContracts`, `HostTotal`, `Obligation`, `Manifest`, `HoldsCore`), `aver-cert/assets/wall/current/SchemaBase.lean` (`Subject`, `Policy`, `TotalityRole`, `CarrierSpec`, `CanonRepr`), `aver-cert/assets/wall/current/Schema.lean` (`Holds`), `aver-cert/assets/wall/current/AcceptedArtifact.lean` (`accepted`), `aver-cert/assets/wall/current/AcceptanceSoundness.lean` (`fn_claim_discharges`, `accept_sound`, `accepted_nonvacuous`) |
 | 6 Plan | `src/codegen/cert/plan_from_mir.rs`, `aver-cert/src/engine/plan.rs`, `aver-cert/assets/wall/current/Grammar.lean` (`Expr`, `FnPlan`, `tyOf`, `planTyped`, `eval`, `groupModel`, `SRepr`), `aver-cert/assets/wall/current/GrammarLower.lean` (`fnCode`, `codeEntryBytes`), `aver-cert/assets/wall/current/GrammarSound.lean` (`agreement`, `fn_certified_group`) |
-| 7 Pins | `aver-cert/assets/wall/current/AcceptedArtifactCore.lean` (`entryAccepted`, `callsOrdered`, `sigPinned`, `roleTypesPinned`, `indicesDistinct`, `plansAccepted`, `obligationsOf`, `exportsAccounted`, `importsWithinCapabilities`, `startAccounted`, `closureIsolation`), `aver-cert/assets/wall/current/TypeTable.lean` (`mctxOf`, `typeTableConfirmed`, `dataConfirmed`, `declsWellFormed`), `aver-cert/assets/wall/current/GrammarLower.lean` (`S3Pin`, `DataPin`), `aver-cert/assets/wall/current/ClaimAxes.lean` (`contractsMatch`, `reportEntries`, `reportFacets`), `aver-cert/assets/wall/current/DeclaredLayout.lean` (`layoutConfirmed`, `fnTypesConfirmed`, `exportNamesDistinct`, `StringFast`, `Chars`), `aver-cert/assets/wall/current/ByteWindow.lean` (`typesLazy`, `exportsLazy`, `codeLazy`), `aver-cert/assets/wall/current/SortedKeys.lean` (`exportsAccountedOf_of_fast`, `closureIsolationL_of_S`), `aver-cert/src/wall.rs` (`render_artifact_bytes`) |
+| 7 Pins | `aver-cert/assets/wall/current/AcceptedArtifactCore.lean` (`entryAccepted`, `callsOrdered`, `sigPinned`, `roleTypesPinned`, `indicesDistinct`, `consPinned`, `plansAccepted`, `obligationsOf`, `exportsAccounted`, `importsWithinCapabilities`, `startAccounted`, `closureIsolation`), `aver-cert/assets/wall/current/TypeTable.lean` (`mctxOf`, `typeTableConfirmed`, `dataConfirmed`, `declsWellFormed`), `aver-cert/assets/wall/current/GrammarLower.lean` (`S3Pin`, `DataPin`), `aver-cert/assets/wall/current/ClaimAxes.lean` (`contractsMatch`, `reportEntries`, `reportFacets`), `aver-cert/assets/wall/current/DeclaredLayout.lean` (`layoutConfirmed`, `fnTypesConfirmed`, `exportNamesDistinct`, `StringFast`, `Chars`), `aver-cert/assets/wall/current/ByteWindow.lean` (`typesLazy`, `exportsLazy`, `codeLazy`), `aver-cert/assets/wall/current/SortedKeys.lean` (`exportsAccountedOf_of_fast`, `closureIsolationL_of_S`), `aver-cert/src/wall.rs` (`render_artifact_bytes`) |
 | 8 Totality | `aver-cert/assets/wall/current/GrammarTotal.lean` (`checkTermGroup`, `groupPolicy`, `fn_certified_total_of_check`) |
 | 9 Bridges and laws | `aver-cert/assets/wall/current/GrammarBridge.lean` (`Exact`, `Adequate`, `ArgsTyped`, `adequate_transfer`, `exact_of_step`, `bridge_of_step`), `aver-cert/src/bridge_statement.rs` (`render_bridge_statement`, `pinned_from_expanded`, `law_mentioned_bridges`), `aver-cert/src/engine/source_bridges.rs`, `aver-cert/src/engine/law_claims.rs`, `aver-cert/src/verifier.rs` (`validate_law_candidate`, `validate_source_bridge_candidate`, `read_source_encoder`) |
 | 10 Witness and audit | `aver-cert/src/verifier.rs` (`checker_witness`, `REPORT_PIN_PREFIX`, `checker_audit`, `AXIOM_WHITELIST`, `CHECKED_ROOT`, `parse_law_audits`, `parse_bridged_law_audits`, `parse_bridge_audits`), `aver-cert/src/checker_audit.lean` |
diff --git a/docs/certification.md b/docs/certification.md
index 01402d97c..87ff15a8e 100644
--- a/docs/certification.md
+++ b/docs/certification.md
@@ -105,9 +105,9 @@ L3 is derived by the wall (`GrammarTotal.checkTermGroup`), never read from a man
 
 Every certified export reports one class, `source-plan-v1`, with facets the wall derives from the plan: `recursive`, `mutual`, `calls`, `records`, `variants`, `strings`, `floats`.
 
-The plan grammar is the admitted subset of optimized MIR. It covers Int, Bool, Float and String literals; locals and named `let`; calls to other planned functions, including self and mutual recursion and tail calls; Int `+ - *` and the six comparisons; Bool `and`, `or`, `not`, `==` and `!=`; Float comparisons other than `!=`; String `+`, `==`, `!=` and interpolation of String parts; `if`; records with two or more fields (create in declared order, and project); user variants, `Option` and `Result` (construct and match); matches on Int, Bool and String literals, flat tuple destructuring, and a List match on `[]` and `[head, ..tail]`; `Option.withDefault` and `Result.withDefault`; `Int.div` and `Int.mod` by a nonzero literal, or fused under `Result.withDefault` with an Int default; the empty list and `List.prepend`. A function that touches a `Vector` is declined: on wasm-gc a `Vector` value is a version struct over a shared array, and the wall models it as the plain array of its elements.
+The plan grammar is the admitted subset of optimized MIR. It covers Int, Bool, Float and String literals; locals and named `let`; calls to other planned functions, including self and mutual recursion and tail calls; Int `+ - *` and the six comparisons; Bool `and`, `or`, `not`, `==` and `!=`; Float comparisons other than `!=`; String `+`, `==`, `!=` and interpolation of String parts; `if`; records with two or more fields (create in declared order, and project); user variants, `Option` and `Result` (construct and match); matches on Int, Bool and String literals, flat tuple destructuring, and a List match on `[]` and `[head, ..tail]`; `Option.withDefault` and `Result.withDefault`; `Int.div` and `Int.mod` by a nonzero literal, or fused under `Result.withDefault` with an Int default; list literals, empty or not, and `List.prepend`. A non-empty literal calls the per-type cons helper once per item; the certificate carries that helper as a planned function and the wall checks that its plan is exactly one `List.prepend` of its two parameters. A function that touches a `Vector` is declined: on wasm-gc a `Vector` value is a version struct over a shared array, and the wall models it as the plain array of its elements.
 
-A function is declined, with the MIR node or type named in the reason, when it has effects, uses raw i64 slots, negates an Int (the negation helper has no wall template yet), uses an Int literal outside the i64 range, does Float arithmetic, calls through a function value, builds a non-empty list literal, calls a `List` helper other than `List.prepend`, or uses any other node outside the subset. A function is also declined when the producer's check finds that its plan does not lower to exactly its code entry.
+A function is declined, with the MIR node or type named in the reason, when it has effects, uses raw i64 slots, negates an Int (the negation helper has no wall template yet), uses an Int literal outside the i64 range, does Float arithmetic, calls through a function value, calls a `List` helper other than `List.prepend`, or uses any other node outside the subset. A function is also declined when the producer's check finds that its plan does not lower to exactly its code entry.
 
 ## Package format
 
diff --git a/src/codegen/cert/plan_from_mir.rs b/src/codegen/cert/plan_from_mir.rs
index 3b6e96d41..27c1b2b72 100644
--- a/src/codegen/cert/plan_from_mir.rs
+++ b/src/codegen/cert/plan_from_mir.rs
@@ -61,6 +61,9 @@ pub trait PlanLayout {
     fn result(&self, canonical: &str) -> Option<u32>;
     fn vector(&self, canonical: &str) -> Option<u32>;
     fn list(&self, canonical: &str) -> Option<u32>;
+    /// The function index of the `List<T>` cons helper a non-empty literal
+    /// calls once per item (`emit_mir_list_literal`).
+    fn list_cons(&self, canonical: &str) -> Option<u32>;
     fn tuple(&self, canonical: &str) -> Option<u32>;
     fn map(&self, canonical: &str) -> Option<u32>;
     /// A type name the emitter represents specially (packed sequence,
@@ -430,6 +433,23 @@ impl TypeTableBuilder {
         Err(format!("type `{name}`"))
     }
 
+    /// Declare the cons helper of `List<elem>` (the literal's canonical type
+    /// `canonical`), which a non-empty literal calls once per item.
+    fn list_cons(
+        &mut self,
+        layout: &dyn PlanLayout,
+        canonical: &str,
+        elem: &PlanTy,
+    ) -> Result<(), String> {
+        let f = layout
+            .list_cons(canonical)
+            .ok_or_else(|| format!("List (non-empty literal): `{canonical}` has no cons helper"))?;
+        if !self.table.list_cons.iter().any(|l| &l.0 == elem) {
+            self.table.list_cons.push((elem.clone(), f));
+        }
+        Ok(())
+    }
+
     /// Declare the passive data segment holding a string literal's bytes.
     fn str_seg(&mut self, layout: &dyn PlanLayout, bytes: &[u8]) -> Result<(), String> {
         if self.table.str_segs.iter().any(|(b, _)| b == bytes) {
@@ -784,14 +804,18 @@ impl Printer<'_> {
                     .collect::<Result<_, _>>()?,
             ),
             MirExpr::List(items) => {
-                if !items.is_empty() {
-                    return Err("List (non-empty literal)".into());
-                }
-                let ty = self.ty(&stamped(expr)?)?;
+                let text = stamped(expr)?;
+                let ty = self.ty(&text)?;
                 let PlanTy::List(elem) = ty else {
                     return Err("List (stamp is not a List)".into());
                 };
-                PlanExpr::List(*elem, Vec::new())
+                if !items.is_empty() {
+                    let canonical = parse_ty(&text)
+                        .map(|t| t.canonical())
+                        .ok_or("List (stamp does not parse)")?;
+                    self.types.list_cons(self.layout, &canonical, &elem)?;
+                }
+                PlanExpr::List(*elem, self.exprs(items)?)
             }
             other => return Err(node_name(other).to_string()),
         })
@@ -1258,4 +1282,24 @@ fn notLiteral(a: Int, d: Int) -> Int
         assert_eq!(arms[0].0, PlanPat::EmptyList);
         assert!(matches!(arms[1].0, PlanPat::Cons(h, t) if h != PLAN_NO_SLOT && h != t));
     }
+
+    #[test]
+    fn a_list_literal_prints_its_items_and_declares_its_cons_helper() {
+        let (map, types) = plans(
+            r#"
+module L
+    intent = "literal probes"
+    exposes [three]
+
+fn three(x: Int) -> List<Int>
+    [x, 2, x]
+"#,
+        );
+        let three = plan(&map, "three");
+        let PlanExpr::List(PlanTy::Int, items) = &three.body else {
+            panic!("three body: {:?}", three.body)
+        };
+        assert_eq!(items.len(), 3);
+        assert!(types.list_cons.iter().any(|(t, _)| *t == PlanTy::Int));
+    }
 }
diff --git a/src/codegen/wasm_gc/cert_layout.rs b/src/codegen/wasm_gc/cert_layout.rs
index e384c8f2b..225d70b63 100644
--- a/src/codegen/wasm_gc/cert_layout.rs
+++ b/src/codegen/wasm_gc/cert_layout.rs
@@ -12,6 +12,7 @@ use super::types::TypeRegistry;
 
 pub(super) struct CertLayout<'a> {
     pub(super) registry: &'a TypeRegistry,
+    pub(super) fn_map: &'a super::body::FnMap,
     pub(super) symbol_table: &'a SymbolTable,
     pub(super) fn_idx: HashMap<FnId, u32>,
     pub(super) builtins: &'a [String],
@@ -71,6 +72,10 @@ impl PlanLayout for CertLayout<'_> {
         self.registry.list_type_idx(canonical)
     }
 
+    fn list_cons(&self, canonical: &str) -> Option<u32> {
+        self.fn_map.list_ops_lookup(canonical).map(|ops| ops.cons)
+    }
+
     fn tuple(&self, canonical: &str) -> Option<u32> {
         self.registry.tuple_type_idx(canonical)
     }
diff --git a/src/codegen/wasm_gc/module.rs b/src/codegen/wasm_gc/module.rs
index b8eadd50c..127754afc 100644
--- a/src/codegen/wasm_gc/module.rs
+++ b/src/codegen/wasm_gc/module.rs
@@ -6150,6 +6150,7 @@ pub(super) fn emit_module_with(
     // never changes a byte.
     let cert_layout = super::cert_layout::CertLayout {
         registry: &registry,
+        fn_map: &fn_map,
         symbol_table: &symbol_table,
         fn_idx: resolved_fn_defs
             .iter()
diff --git a/tests/cert_certify_spec.rs b/tests/cert_certify_spec.rs
index f48129d4e..6231e5b40 100644
--- a/tests/cert_certify_spec.rs
+++ b/tests/cert_certify_spec.rs
@@ -2961,8 +2961,8 @@ fn cert_projects_payment_ops_package_checks() {
         "payment_ops check verdict does not say CHECKED:\n{report}"
     );
     assert!(
-        report.contains("101 checked exports"),
-        "payment_ops must keep the 101 exports it certifies:\n{report}"
+        report.contains("106 checked exports"),
+        "payment_ops must keep the 106 exports it certifies:\n{report}"
     );
     // The project's single `verify … law` is universal by design but its
     // emitted proof ladder has no `String.replace` theory and lands on its
diff --git a/tests/cert_hardening_spec.rs b/tests/cert_hardening_spec.rs
index 7039e14a0..0ff1b32e8 100644
--- a/tests/cert_hardening_spec.rs
+++ b/tests/cert_hardening_spec.rs
@@ -37,7 +37,10 @@
 //!   reaches a work import;
 //! * a List match whose arm results are exchanged, List cons structs declared
 //!   for each other's instantiation, and a cons pattern whose head and tail
-//!   slots are exchanged.
+//!   slots are exchanged;
+//! * a List literal's cons helper declared as a user function of the same
+//!   signature, a cons helper whose plan is not the cons plan, and the cons
+//!   helpers of two instantiations exchanged.
 //!
 //! Gated behind `wasm` and skipped when `lake` is unavailable, like the other
 //! certificate suites.
@@ -1536,3 +1539,146 @@ fn cert_hardening_declines_a_cons_pattern_with_head_and_tail_exchanged() {
     let (ok, report) = aver_cert("check", &wasm, &cert);
     assert_declined(ok, &report, "did not build");
 }
+
+/// A program building non-empty List literals: Int literals, String
+/// parameters, and a user function `keep` with the cons helper's signature
+/// whose plan is not the cons plan (it returns the tail).
+const LITS: &str = "module Lits
+    intent = \"List literals.\"
+    exposes [three, pair, keep]
+
+fn three() -> List<Int>
+    ? \"Three Ints.\"
+    [1, 2, 3]
+
+fn pair(a: String, b: String) -> List<String>
+    ? \"Two Strings.\"
+    [a, b]
+
+fn keep(h: Int, t: List<Int>) -> List<Int>
+    ? \"The tail, unchanged.\"
+    t
+";
+
+/// Emit the List-literal certificate into a fresh scratch directory.
+fn literal_baseline(prefix: &str) -> Option<(ScratchDir, PathBuf, PathBuf)> {
+    if !lake_available() {
+        return None;
+    }
+    let dir = temp_dir(prefix);
+    std::fs::write(dir.join("lits.av"), LITS).unwrap();
+    let out = dir.join("out");
+    let compile = aver_command()
+        .current_dir(&*dir)
+        .args([
+            "compile",
+            "lits.av",
+            "--target",
+            "wasm-gc",
+            "--certify",
+            "-o",
+        ])
+        .arg(&out)
+        .output()
+        .expect("aver compile --certify runs");
+    assert!(
+        compile.status.success(),
+        "compile --certify failed:\n{}",
+        String::from_utf8_lossy(&compile.stderr)
+    );
+    Some((dir, out.join("lits.wasm"), out.join("cert")))
+}
+
+/// The digits right after the first occurrence of `needle` in `text`.
+fn number_after(text: &str, needle: &str) -> String {
+    let at = text
+        .find(needle)
+        .unwrap_or_else(|| panic!("`{needle}` is in Plans.lean"))
+        + needle.len();
+    text[at..]
+        .chars()
+        .take_while(char::is_ascii_digit)
+        .collect()
+}
+
+/// The honest certificate checks, with every export certified; the cons
+/// helpers ride along as planned internal functions.
+#[test]
+fn cert_hardening_accepts_list_literals() {
+    let Some((_dir, wasm, cert)) = literal_baseline("certharden-lits-clean") else {
+        return;
+    };
+    let plans = std::fs::read_to_string(cert.join("Plans.lean")).unwrap();
+    assert!(plans.contains("listCons := [(.int, "), "{plans}");
+    assert!(plans.contains("(.string, "), "{plans}");
+    let (ok, report) = aver_cert("check", &wasm, &cert);
+    assert!(ok, "the List-literal certificate must check:\n{report}");
+    assert!(report.contains("3 checked exports"), "{report}");
+}
+
+/// The cons helper a literal calls is the one the type table declares, and
+/// the wall requires its plan to be exactly the cons plan: pointing
+/// `List<Int>`'s entry at `keep`, a user function of the same signature
+/// whose plan returns the tail, is refused.
+#[test]
+fn cert_hardening_declines_a_cons_helper_that_is_a_user_function() {
+    let Some((_dir, wasm, cert)) = literal_baseline("certharden-lits-user") else {
+        return;
+    };
+    let plans = cert.join("Plans.lean");
+    let text = std::fs::read_to_string(&plans).unwrap();
+    let cons = number_after(&text, "listCons := [(.int, ");
+    let keep = number_after(&text, "⟨\"keep\", true, ");
+    replace_once(
+        &plans,
+        &format!("listCons := [(.int, {cons})"),
+        &format!("listCons := [(.int, {keep})"),
+    );
+    let (ok, report) = aver_cert("check", &wasm, &cert);
+    assert_declined(ok, &report, "did not build");
+}
+
+/// The cons helper's own plan is pinned to the cons plan: a plan that
+/// returns the tail instead of consing lowers to other bytes and is not the
+/// wall's cons plan, so the package is refused.
+#[test]
+fn cert_hardening_declines_a_cons_helper_whose_plan_is_not_the_cons_plan() {
+    let Some((_dir, wasm, cert)) = literal_baseline("certharden-lits-plan") else {
+        return;
+    };
+    let plans = cert.join("Plans.lean");
+    let text = std::fs::read_to_string(&plans).unwrap();
+    let cons = number_after(&text, "listCons := [(.int, ");
+    let def = format!("def fn{cons} : FnPlan :=");
+    let at = text.find(&def).expect("the cons helper is planned");
+    let body = "body := (.call (.builtin .listPrepend) [(.local 0), (.local 1)])";
+    let rel = text[at..]
+        .find(body)
+        .expect("the cons helper's body is the cons plan");
+    let mut tampered = text.clone();
+    tampered.replace_range(at + rel..at + rel + body.len(), "body := (.local 1)");
+    std::fs::write(&plans, tampered).unwrap();
+    let (ok, report) = aver_cert("check", &wasm, &cert);
+    assert_declined(ok, &report, "did not build");
+}
+
+/// The cons helpers of two instantiations exchanged: each literal would call
+/// the other type's helper, whose planned signature is not its cons
+/// signature, so the typing refuses the literals.
+#[test]
+fn cert_hardening_declines_exchanged_cons_helpers() {
+    let Some((_dir, wasm, cert)) = literal_baseline("certharden-lits-swap") else {
+        return;
+    };
+    let plans = cert.join("Plans.lean");
+    let text = std::fs::read_to_string(&plans).unwrap();
+    let int_f = number_after(&text, "listCons := [(.int, ");
+    let str_f = number_after(&text, &format!("listCons := [(.int, {int_f}), (.string, "));
+    replace_once(
+        &plans,
+        &format!("listCons := [(.int, {int_f}), (.string, {str_f})]"),
+        &format!("listCons := [(.int, {str_f}), (.string, {int_f})]"),
+    );
+    let (ok, report) = aver_cert("check", &wasm, &cert);
+    assert_declined(ok, &report, "did not build");
+}
diff --git a/tests/snapshots/cert_certify_spec__add_one_certificate_package.snap b/tests/snapshots/cert_certify_spec__add_one_certificate_package.snap
index 5fdb67f84..902ec8d24 100644
--- a/tests/snapshots/cert_certify_spec__add_one_certificate_package.snap
+++ b/tests/snapshots/cert_certify_spec__add_one_certificate_package.snap
@@ -5,7 +5,7 @@ expression: golden
 == cert-manifest.json ==
 {
   "schema_version": 9,
-  "format": {"version": 1, "wall_id": "sha256:5168df0c3f4da023c53a9c929e081803c559ed2e22fc6a103f8fb827745ae4d9"},
+  "format": {"version": 1, "wall_id": "sha256:318de1883be91114ed8a396835aea6d183ac9acc4903c7c99e72b023a20ce2c6"},
   "wasm": "add_one.wasm",
   "wasm_sha256": "4b86ac5e745a7f0aeef0d24178a3f47ed09b4f98ffc36216aedf252c9cb20583",
   "target": "wasm-gc",
diff --git a/tests/snapshots/cert_certify_spec__wasip2_component_certificate_package.snap b/tests/snapshots/cert_certify_spec__wasip2_component_certificate_package.snap
index 8e7df5cb7..5dab863f1 100644
--- a/tests/snapshots/cert_certify_spec__wasip2_component_certificate_package.snap
+++ b/tests/snapshots/cert_certify_spec__wasip2_component_certificate_package.snap
@@ -5,7 +5,7 @@ expression: golden
 == cert-manifest.json ==
 {
   "schema_version": 9,
-  "format": {"version": 1, "wall_id": "sha256:5168df0c3f4da023c53a9c929e081803c559ed2e22fc6a103f8fb827745ae4d9"},
+  "format": {"version": 1, "wall_id": "sha256:318de1883be91114ed8a396835aea6d183ac9acc4903c7c99e72b023a20ce2c6"},
   "wasm": "wasip2_carrierless.component.wasm",
   "wasm_sha256": "0e7064150f82e180dff6f774a8f48711acd2ea21d183ee06576d4f7c9f135aed",
   "target": "wasip2",
diff --git a/tools/cert-baseline.json b/tools/cert-baseline.json
index ef871ac0d..59bbac950 100644
--- a/tools/cert-baseline.json
+++ b/tools/cert-baseline.json
@@ -96,6 +96,7 @@
  },
  "projects/payment_ops/main.av": {
   "bridges": [
+   "App_Cli_helpLines",
    "App_Commands_duplicateSettlementAudit",
    "App_Commands_duplicateWebhookAudit",
    "App_Commands_sampleAudit",
@@ -106,10 +107,13 @@
    "App_Queries_sampleCase",
    "App_Queries_sampleEvent",
    "App_Queries_sampleSettlement",
+   "App_Queries_sampleState",
    "App_Render_renderCaseItem",
    "App_Render_sampleAudit",
    "App_Render_sampleCase",
+   "App_Render_sampleDetail",
    "App_Render_sampleEvent",
+   "App_Render_sampleReport",
    "App_Render_sampleSettlement",
    "App_Render_sampleSummary",
    "App_Render_settlementKindText",
@@ -157,6 +161,7 @@
    "Infra_Store_settlementsPath"
   ],
   "certified": {
+   "App_Cli_helpLines": "L1",
    "App_Commands_duplicateSettlementAudit": "L1",
    "App_Commands_duplicateWebhookAudit": "L1",
    "App_Commands_hasSettlementRow": "L1",
@@ -173,12 +178,15 @@
    "App_Queries_sampleEvent": "L1",
    "App_Queries_sampleOrFirst": "L1",
    "App_Queries_sampleSettlement": "L1",
+   "App_Queries_sampleState": "L1",
    "App_Render_renderAuditItemsInto": "L1",
    "App_Render_renderCaseItem": "L1",
    "App_Render_renderCaseItemsInto": "L1",
    "App_Render_sampleAudit": "L1",
    "App_Render_sampleCase": "L1",
+   "App_Render_sampleDetail": "L1",
    "App_Render_sampleEvent": "L1",
+   "App_Render_sampleReport": "L1",
    "App_Render_sampleSettlement": "L1",
    "App_Render_sampleSummary": "L1",
    "App_Render_settlementKindText": "L1",
@@ -224,6 +232,7 @@
    "Domain_Normalize_normalizeWebhookEvent": "L1",
    "Domain_Reconcile_amountMissing": "L1",
    "Domain_Reconcile_compareAmounts": "L1",
+   "Domain_Reconcile_compareCurrency": "L1",
    "Domain_Reconcile_findState": "L1",
    "Domain_Reconcile_firstCurrency": "L1",
    "Domain_Reconcile_prependAll": "L1",