diff --git a/verification/aeneas/lean/DropJson.lean b/verification/aeneas/lean/DropJson.lean
new file mode 100644
index 0000000000..ee0d59f8c9
--- /dev/null
+++ b/verification/aeneas/lean/DropJson.lean
@@ -0,0 +1,437 @@
+/- Copyright 2026 The Fuchsia Authors
+
+Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+<LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+This file may not be copied, modified, or distributed except according to
+those terms. -/
+
+module
+public import Lean
+public import DropOwnership
+@[expose] public section
+
+/-!
+This decoder reads a complete Charon body, including its local declarations.
+It accepts a deliberately small executable schema. Every operand is decoded in
+evaluation order. It does not search JSON recursively for moves or accept an
+externally supplied list of effects.
+
+Source spans, comments, statement IDs, types, generic arguments, and the static
+trait reference in drop glue cannot carry executable operands in this schema.
+Their payloads are explicitly ignored here. The ordinary admission audit still
+checks operations, types, function identities, and all execution dependencies.
+This decoder supplies only the additional ownership condition for erasing a
+conditional drop, under the compiler correspondence premise of DropOwnership.
+-/
+
+namespace AeneasSpecs.DropJson
+
+open Lean DropOwnership
+
+abbrev Decode := Except String
+
+def require (condition : Bool) (message : String) : Decode Unit :=
+  if condition then pure () else throw message
+
+def fields (j : Json) (names : List String) : Decode Unit := do
+  let obj ← j.getObj?
+  let actual := obj.toList.map Prod.fst
+  require (actual.length == names.length && actual.all names.contains)
+    "unexpected or missing object fields"
+
+def field := Json.getObjVal?
+
+def variant (j : Json) : Decode (String × Json) := do
+  let obj ← j.getObj?
+  match obj.toList with
+  | [kv] => pure kv
+  | _ => throw "expected one constructor"
+
+def tuple (j : Json) (n : Nat) : Decode (Array Json) := do
+  let a ← j.getArr?
+  require (a.size == n) "wrong constructor arity"
+  pure a
+
+def item (a : Array Json) (i : Nat) : Decode Json :=
+  match a[i]? with
+  | some j => pure j
+  | none => throw "missing constructor argument"
+
+def localIndex (count : Nat) (j : Json) : Decode Nat := do
+  let i ← j.getNat?
+  require (i < count) "local index out of bounds"
+  pure i
+
+def globalRef (j : Json) : Decode Unit := do
+  fields j ["id", "generics"]
+  let _ ← (← field j "id").getNat?
+  -- Generic arguments describe types and constants, not runtime operands.
+  pure ()
+
+def functionRef (j : Json) : Decode Unit := do
+  fields j ["kind", "generics"]
+  let (tag, value) ← variant (← field j "kind")
+  match tag with
+  | "Fun" => let _ ← value.getNat?; pure ()
+  | "Trait" =>
+    let args ← tuple value 2
+    let _ ← (← item args 1).getNat?
+    -- The first argument is a static trait reference, not a place or operand.
+    pure ()
+  | _ => throw "unsupported function reference"
+
+def directFunction (j : Json) : Decode Unit := do
+  let (tag, value) ← variant j
+  require (tag == "Regular") "unsupported executable function operand"
+  functionRef value
+  let (kind, _) ← variant (← field value "kind")
+  require (kind == "Fun") "only direct function calls are supported"
+
+def constant (j : Json) : Decode Unit := do
+  let (tag, value) ← variant j
+  require (tag == "Untagged") "unsupported constant wrapper"
+  let args ← tuple value 2
+  let (kind, payload) ← variant (← item args 0)
+  -- The second argument is the static type of this constant.
+  match kind with
+  | "Global" => globalRef payload
+  | "Bool" => let _ ← payload.getBool?; pure ()
+  | "Adt" =>
+    let a ← tuple payload 2
+    require (← item a 0).isNull "only unit constants are supported"
+    require (← (← item a 1).getArr?).isEmpty "only unit constants are supported"
+  | "Opaque" =>
+    require ((← payload.getStr?) == "Missing metadata") "unsupported opaque constant"
+  | _ => throw "unsupported constant expression"
+
+structure Place where
+  root : Option Nat
+  whole : Bool
+  restricted : List Nat := []
+
+def place : Nat → Nat → Json → Decode Place
+  | 0, _, _ => throw "place nesting limit exceeded"
+  | fuel + 1, count, j => do
+    fields j ["kind", "ty"]
+    let (tag, value) ← variant (← field j "kind")
+    match tag with
+    | "Local" => pure ⟨some (← localIndex count value), true, []⟩
+    | "Global" => globalRef value; pure ⟨none, true, []⟩
+    | "Projection" =>
+      let args ← tuple value 2
+      let base ← place fuel count (← item args 0)
+      -- Dereference is the only supported projection. Its base cannot be a
+      -- candidate local anywhere in the body, including disconnected code.
+      require ((← (← item args 1).getStr?) == "Deref") "unsupported place projection"
+      pure ⟨base.root, false, base.root.toList ++ base.restricted⟩
+    | _ => throw "unsupported place constructor"
+
+structure Audit where
+  effects : List Effect := []
+  restricted : List Nat := []
+
+def Audit.append (a b : Audit) : Audit :=
+  ⟨a.effects ++ b.effects, a.restricted ++ b.restricted⟩
+
+def operand (fuel count : Nat) (j : Json) : Decode Audit := do
+  let (tag, value) ← variant j
+  match tag with
+  | "Move" | "Copy" =>
+    let p ← place fuel count value
+    let effects := if tag == "Move" && p.whole then
+        p.root.toList.map Effect.consume else []
+    pure ⟨effects, p.restricted⟩
+  | "Const" => constant value; pure {}
+  | _ => throw "unsupported operand constructor"
+
+def destination (fuel count : Nat) (j : Json) : Decode Audit := do
+  let p ← place fuel count j
+  let effects := if p.whole then p.root.toList.map Effect.define else []
+  pure ⟨effects, p.restricted⟩
+
+def rvalue (fuel count : Nat) (j : Json) : Decode Audit := do
+  let (tag, value) ← variant j
+  match tag with
+  | "Use" =>
+    let args ← tuple value 2
+    require ((← (← item args 1).getStr?) == "Yes") "unsupported Use mode"
+    operand fuel count (← item args 0)
+  | "Ref" =>
+    fields value ["place", "kind", "ptr_metadata"]
+    let kind ← (← field value "kind").getStr?
+    require (["Shared", "Mut"].contains kind) "unsupported reference kind"
+    let p ← place fuel count (← field value "place")
+    let metadata ← operand fuel count (← field value "ptr_metadata")
+    pure ⟨metadata.effects, p.root.toList ++ p.restricted ++ metadata.restricted⟩
+  | "BinaryOp" =>
+    let args ← tuple value 3
+    require ((← (← item args 0).getStr?) == "Eq") "unsupported binary operation"
+    let left ← operand fuel count (← item args 1)
+    let right ← operand fuel count (← item args 2)
+    pure (left.append right)
+  | _ => throw "unsupported rvalue constructor"
+
+def simple (fuel count : Nat) (j : Json) : Decode Audit := do
+  let (tag, value) ← variant j
+  match tag with
+  | "StorageLive" | "StorageDead" => pure ⟨[.define (← localIndex count value)], []⟩
+  | "Assign" =>
+    let args ← tuple value 2
+    let rhs ← rvalue fuel count (← item args 1)
+    let dest ← destination fuel count (← item args 0)
+    pure (rhs.append dest)
+  | "Borrowck" =>
+    let (kind, p) ← variant value
+    require (kind == "FakeRead") "unsupported borrow-checking statement"
+    let p ← place fuel count p
+    pure ⟨[], p.restricted⟩
+  | _ => throw "unsupported simple statement"
+
+def call (fuel count : Nat) (j : Json) : Decode Audit := do
+  fields j ["func", "args", "dest"]
+  directFunction (← field j "func")
+  let args ← (← field j "args").getArr?
+  let mut result : Audit := {}
+  for arg in args do
+    result := result.append (← operand fuel count arg)
+  -- Restoring the destination in this node precedes every normal and unwind
+  -- successor. Even an unwinding call cannot establish an empty destination.
+  pure (result.append (← destination fuel count (← field j "dest")))
+
+def dropLocal (fuel count : Nat) (j : Json) : Decode Nat := do
+  require ((← (← field j "kind").getStr?) == "Conditional") "only conditional drops are supported"
+  let p ← place fuel count (← field j "place")
+  require p.whole "projected drop is unsupported"
+  let some root := p.root | throw "drop of a global is unsupported"
+  functionRef (← field j "fn_ptr")
+  pure root
+
+def abort (j : Json) : Decode Unit := do
+  match j with
+  | .str "UnwindTerminate" => pure ()
+  | _ =>
+    let (tag, path) ← variant j
+    require (tag == "Panic") "unsupported abort constructor"
+    let path ← path.getArr?
+    for part in path do
+      let (tag, args) ← variant part
+      require (tag == "Ident") "unsupported panic name component"
+      let args ← tuple args 2
+      let _ ← (← item args 0).getStr?
+      let _ ← (← item args 1).getNat?
+    pure ()
+
+def assertion (fuel count : Nat) (j : Json) : Decode Audit := do
+  fields j ["cond", "expected", "check_kind"]
+  let _ ← (← field j "expected").getBool?
+  require (← field j "check_kind").isNull "unsupported assertion check kind"
+  operand fuel count (← field j "cond")
+
+def wrapper (structured : Bool) (j : Json) : Decode Json := do
+  fields j (if structured then ["span", "id", "kind", "comments_before"]
+    else ["span", "kind", "comments_before"])
+  if structured then
+    let _ ← (← field j "id").getNat?
+  field j "kind"
+
+structure Annotated where
+  node : Node
+  restricted : List Nat := []
+
+def target (count : Nat) (j : Json) : Decode Nat := do
+  let i ← j.getNat?
+  require (i < count) "control target out of bounds"
+  pure i
+
+def switch (fuel count blocks : Nat) (j : Json) : Decode (Audit × List Nat) := do
+  fields j ["data", "branches"]
+  let successors ← (← field j "branches").getArr?
+  require (!successors.isEmpty) "empty switch successor list"
+  let successors ← successors.toList.mapM (target blocks)
+  let data ← field j "data"
+  fields data ["scrutinee", "branches", "fallback"]
+  let (tag, scrutinee) ← variant (← field data "scrutinee")
+  require (tag == "Value") "unsupported switch scrutinee"
+  let effects ← operand fuel count scrutinee
+  let branches ← (← field data "branches").getArr?
+  for branch in branches do
+    let branch ← tuple branch 2
+    constant (← item branch 0)
+    let _ ← target successors.length (← item branch 1)
+  let _ ← target successors.length (← field data "fallback")
+  pure (effects, successors)
+
+def unstructured (fuel count : Nat) (j : Json) : Decode (List Annotated) := do
+  let blocks ← j.getArr?
+  require (!blocks.isEmpty) "empty unstructured body"
+  blocks.toList.mapM fun block => do
+    fields block ["statements", "terminator"]
+    let statements ← (← field block "statements").getArr?
+    let mut audit : Audit := {}
+    for statement in statements do
+      audit := audit.append (← simple fuel count (← wrapper false statement))
+    let kind ← wrapper false (← field block "terminator")
+    match kind with
+    | .str "Return" | .str "UnwindResume" =>
+      pure ⟨⟨audit.effects, none, []⟩, audit.restricted⟩
+    | _ =>
+      let (tag, value) ← variant kind
+      match tag with
+      | "Goto" =>
+        fields value ["target"]
+        pure ⟨⟨audit.effects, none, [← target blocks.size (← field value "target")]⟩, audit.restricted⟩
+      | "Abort" => abort value; pure ⟨⟨audit.effects, none, []⟩, audit.restricted⟩
+      | "Call" =>
+        fields value ["call", "target", "on_unwind"]
+        let total := audit.append (← call fuel count (← field value "call"))
+        let normal ← target blocks.size (← field value "target")
+        let unwind ← target blocks.size (← field value "on_unwind")
+        pure ⟨⟨total.effects, none, [normal, unwind]⟩, total.restricted⟩
+      | "Drop" =>
+        fields value ["kind", "place", "fn_ptr", "target", "on_unwind"]
+        let dropped ← dropLocal fuel count value
+        let normal ← target blocks.size (← field value "target")
+        let unwind ← target blocks.size (← field value "on_unwind")
+        pure ⟨⟨audit.effects, some dropped, [normal, unwind]⟩, audit.restricted⟩
+      | "Switch" =>
+        let (branchAudit, successors) ← switch fuel count blocks.size value
+        let total := audit.append branchAudit
+        pure ⟨⟨total.effects, none, successors⟩, total.restricted⟩
+      | "Assert" =>
+        fields value ["assert", "target", "on_unwind"]
+        let total := audit.append (← assertion fuel count (← field value "assert"))
+        let normal ← target blocks.size (← field value "target")
+        let unwind ← target blocks.size (← field value "on_unwind")
+        pure ⟨⟨total.effects, none, [normal, unwind]⟩, total.restricted⟩
+      | _ => throw "unsupported unstructured terminator"
+
+abbrev Build := StateT (Array Annotated) Decode
+
+def emit (a : Annotated) : Build Nat := do
+  let nodes ← get
+  set (nodes.push a)
+  pure nodes.size
+
+-- The continuation is explicit. Abrupt exits ignore it. Statements after an
+-- abrupt exit are still decoded and remain conservative disconnected nodes.
+def structured : Nat → Nat → Json → List Nat → Build Nat
+  | 0, _, _, _ => throw "structured nesting limit exceeded"
+  | fuel + 1, count, block, continuation => do
+    fields block ["span", "id", "statements"]
+    let _ ← (← field block "id").getNat?
+    let statements ← (← field block "statements").getArr?
+    let mut next := continuation
+    for statement in statements.toList.reverse do
+      let kind ← wrapper true statement
+      let node ← match kind with
+        | .str "Return" | .str "UnwindResume" => emit ⟨⟨[], none, []⟩, []⟩
+        | _ => do
+          let (tag, value) ← variant kind
+          match tag with
+          | "Abort" => abort value; emit ⟨⟨[], none, []⟩, []⟩
+          | "Call" =>
+            fields value ["call", "on_unwind"]
+            let audit ← call fuel count (← field value "call")
+            -- Falling through a cleanup is conservatively allowed to reach
+            -- the same continuation. Its actual abrupt exits never do so.
+            let unwind ← structured fuel count (← field value "on_unwind") next
+            emit ⟨⟨audit.effects, none, next ++ [unwind]⟩, audit.restricted⟩
+          | "Drop" =>
+            fields value ["kind", "place", "fn_ptr", "on_unwind"]
+            let dropped ← dropLocal fuel count value
+            let unwind ← structured fuel count (← field value "on_unwind") next
+            emit ⟨⟨[], some dropped, next ++ [unwind]⟩, []⟩
+          | "Assert" =>
+            fields value ["assert", "on_failure", "on_unwind"]
+            let audit ← assertion fuel count (← field value "assert")
+            abort (← field value "on_failure")
+            let unwind ← structured fuel count (← field value "on_unwind") next
+            emit ⟨⟨audit.effects, none, next ++ [unwind]⟩, audit.restricted⟩
+          | _ =>
+            -- Loop, Break, Continue, and every unknown constructor fail here.
+            let audit ← simple fuel count kind
+            emit ⟨⟨audit.effects, none, next⟩, audit.restricted⟩
+      next := [node]
+    emit ⟨⟨[], none, next⟩, []⟩
+
+def locals (j : Json) : Decode Nat := do
+  fields j ["arg_count", "locals"]
+  let args ← (← field j "arg_count").getNat?
+  let declarations ← (← field j "locals").getArr?
+  require (args < declarations.size) "invalid argument count"
+  for i in [:declarations.size] do
+    let declaration ← item declarations i
+    fields declaration ["index", "name", "span", "ty", "drop_flag_for"]
+    require ((← (← field declaration "index").getNat?) == i) "locals are not densely indexed"
+    require (← field declaration "drop_flag_for").isNull "drop flag locals are unsupported"
+    let name ← field declaration "name"
+    unless name.isNull do
+      let _ ← name.getStr?
+  pure declarations.size
+
+def topological (nodes : List Node) : Nat → List Nat → List Nat → Decode (List Nat)
+  | 0, remaining, order =>
+    if remaining.isEmpty then pure order else throw "cyclic control flow"
+  | fuel + 1, remaining, order => do
+    if remaining.isEmpty then return order
+    let some chosen := remaining.find? (fun i => remaining.all fun predecessor =>
+      match nodes[predecessor]? with
+      | some node => !node.successors.contains i
+      | none => false) | throw "cyclic control flow"
+    topological nodes fuel (remaining.erase chosen) (order ++ [chosen])
+
+def reorder (count entry : Nat) (annotated : List Annotated) : Decode Graph := do
+  let nodes := annotated.map Annotated.node
+  let candidates := nodes.filterMap Node.candidateDrop
+  let restricted := annotated.flatMap Annotated.restricted
+  require (!(restricted.any candidates.contains)) "candidate local is projected or borrowed"
+  require (entry < nodes.length) "invalid entry node"
+  let order ← topological nodes nodes.length (List.range nodes.length) []
+  let renamed ← order.mapM fun old => do
+    let some node := nodes[old]? | throw "invalid node permutation"
+    let successors ← node.successors.mapM fun successor => do
+      require (successor < nodes.length) "invalid graph successor"
+      pure (order.idxOf successor)
+    pure { node with successors := successors }
+  pure ⟨renamed, count, order.idxOf entry⟩
+
+/-- Decode and check the complete executable schema before projecting effects.
+The fixed nesting limit rejects exceptionally deep inputs rather than making
+the executable decoder partial. Both structured and unstructured bodies are
+reordered in Lean; every disconnected component participates in cycle checks. -/
+def decode (body : Json) : Except String Graph := do
+  let (tag, value) ← variant body
+  fields value ["span", "bound_body_regions", "locals", "body", "comments"]
+  let _ ← (← field value "bound_body_regions").getNat?
+  let count ← locals (← field value "locals")
+  match tag with
+  | "Unstructured" => reorder count 0 (← unstructured 4096 count (← field value "body"))
+  | "Structured" =>
+    let (entry, nodes) ← (structured 4096 count (← field value "body") []).run #[]
+    reorder count entry nodes.toList
+  | _ => throw "unsupported body constructor"
+
+/-- This is the proposition evaluated by each kernel-checked snapshot theorem. -/
+def acceptBody (body : Json) : Bool :=
+  match decode body with
+  | .error _ => false
+  | .ok graph => DropOwnership.accepted graph
+
+theorem accepted_of_decoded {body : Json} {graph : Graph}
+    (decoded : decode body = .ok graph) (checked : acceptBody body = true) :
+    DropOwnership.accepted graph = true := by
+  simpa [acceptBody, decoded] using checked
+
+/-- A certificate about a raw body entails the ownership theorem for the graph
+produced by this decoder. The separate compiler correspondence premise must
+relate source executions to that graph's modeled executions. -/
+theorem decoded_drop_empty {body : Json} {graph : Graph}
+    (decoded : decode body = .ok graph) (checked : acceptBody body = true)
+    {index slot : Nat} {owns : DropOwnership.Concrete}
+    (reached : DropOwnership.Reachable graph index owns)
+    (candidate : (graph.node index).candidateDrop = some slot) :
+    ¬ DropOwnership.execute (graph.node index).effects owns slot :=
+  DropOwnership.accepted_drop_empty (accepted_of_decoded decoded checked) reached candidate
+
+end AeneasSpecs.DropJson
diff --git a/verification/aeneas/lean/DropJsonTests.lean b/verification/aeneas/lean/DropJsonTests.lean
new file mode 100644
index 0000000000..83eb15761f
--- /dev/null
+++ b/verification/aeneas/lean/DropJsonTests.lean
@@ -0,0 +1,119 @@
+/- Copyright 2026 The Fuchsia Authors
+
+Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+<LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+This file may not be copied, modified, or distributed except according to
+those terms. -/
+
+import DropJson
+
+namespace AeneasSpecs.DropJson.Tests
+
+open Lean
+
+set_option maxRecDepth 16384
+set_option maxHeartbeats 2000000
+
+private def obj := Json.mkObj
+private def arr (xs : List Json) := Json.arr xs.toArray
+private def ctor (name : String) (value : Json) := obj [(name, value)]
+private def slot (i : Nat) := obj [("kind", ctor "Local" (toJson i)), ("ty", .null)]
+private def move (i : Nat) := ctor "Move" (slot i)
+private def copy (i : Nat) := ctor "Copy" (slot i)
+private def use (operand : Json) := ctor "Use" (arr [operand, .str "Yes"])
+private def assign (i : Nat) (rhs : Json) := ctor "Assign" (arr [slot i, rhs])
+private def statement (kind : Json) := obj
+  [("span", .null), ("kind", kind), ("comments_before", arr [])]
+private def block (statements : List Json) (terminator : Json) := obj
+  [("statements", arr (statements.map statement)), ("terminator", statement terminator)]
+private def goto (i : Nat) := ctor "Goto" (obj [("target", toJson i)])
+private def ret := block [] (.str "Return")
+private def function := obj [("kind", ctor "Fun" 0), ("generics", .null)]
+private def dropped (i : Nat) (normal unwind : Nat) (kind : String := "Conditional") := ctor "Drop"
+  (obj [("kind", .str kind), ("place", slot i), ("fn_ptr", function),
+    ("target", toJson normal), ("on_unwind", toJson unwind)])
+private def called (dest : Nat) (args : List Json) (normal unwind : Nat) := ctor "Call"
+  (obj [("call", obj [("func", ctor "Regular" function), ("args", arr args), ("dest", slot dest)]),
+    ("target", toJson normal), ("on_unwind", toJson unwind)])
+private def declarations := obj [("arg_count", 1), ("locals", arr
+  ((List.range 3).map fun i => obj [("index", toJson i), ("name", .null), ("span", .null),
+    ("ty", .null), ("drop_flag_for", .null)]))]
+private def body (tag : String) (code : Json) := ctor tag (obj
+  [("span", .null), ("bound_body_regions", 0), ("locals", declarations),
+    ("body", code), ("comments", arr [])])
+private def ullbc (blocks : List Json) := body "Unstructured" (arr blocks)
+private def projection (i : Nat) := obj
+  [("kind", ctor "Projection" (arr [slot i, .str "Deref"])), ("ty", .null)]
+private def unitConstant := ctor "Const" (ctor "Untagged"
+  (arr [ctor "Adt" (arr [.null, arr []]), .null]))
+private def boolConstant := ctor "Untagged" (arr [ctor "Bool" (.bool false), .null])
+private def branch (left right : Nat) := ctor "Switch" (obj
+  [("data", obj [("scrutinee", ctor "Value" (copy 0)),
+    ("branches", arr [arr [boolConstant, 0]]), ("fallback", 1)]),
+   ("branches", arr [toJson left, toJson right])])
+
+example : acceptBody (ullbc [block [assign 0 (use (move 1))] (dropped 1 1 1), ret]) = true := by with_unfolding_all rfl
+example : acceptBody (ullbc [block [] (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl
+example : acceptBody (ullbc [block [assign 0 (use (copy 1))] (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl
+
+-- Assignment restores uncertainty after evaluating every operand, including a
+-- self move. A later overwrite has the same conservative effect.
+example : acceptBody (ullbc [block [assign 1 (use (move 1))] (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl
+example : acceptBody (ullbc [block [assign 0 (use (move 1)), assign 1 (use unitConstant)]
+    (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl
+example : acceptBody (ullbc [block [assign 0 (use (move 1)), ctor "StorageDead" 1]
+    (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl
+example : acceptBody (ullbc [block [assign 0 (use (move 1)), ctor "StorageLive" 1]
+    (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl
+
+-- Every branch and unwind edge participates, including a call destination
+-- whose old value had already been moved away.
+example : acceptBody (ullbc [block [] (branch 1 2),
+    block [assign 0 (use (move 1))] (goto 3), block [] (goto 3),
+    block [] (dropped 1 4 4), ret]) = false := by with_unfolding_all rfl
+example : acceptBody (ullbc [block [assign 0 (use (move 1))] (called 1 [] 1 2), ret,
+    block [] (dropped 1 1 1)]) = false := by with_unfolding_all rfl
+example : acceptBody (ullbc [block [] (called 0 [move 1] 1 2), ret,
+    block [] (dropped 1 1 1)]) = true := by with_unfolding_all rfl
+
+-- Projecting or borrowing the candidate slot is forbidden throughout the
+-- complete body, even if an earlier move would otherwise justify its drop.
+example : acceptBody (ullbc [block [assign 0 (use (ctor "Move" (projection 1)))]
+    (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl
+example : acceptBody (ullbc [block [assign 0 (use (move 1)), assign 2 (ctor "Ref"
+    (obj [("place", slot 1), ("kind", .str "Shared"), ("ptr_metadata", unitConstant)]))]
+    (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl
+example : acceptBody (ullbc [block [assign 0 (use (move 1))]
+    (dropped 1 1 1 "Precise"), ret]) = false := by with_unfolding_all rfl
+example : acceptBody (ullbc [block [assign 0 (use (move 1))] (dropped 1 1 1), ret,
+    block [] (goto 2)]) = false := by with_unfolding_all rfl
+example : acceptBody (ullbc [ret, block [] (dropped 1 0 0)]) = false := by with_unfolding_all rfl
+
+-- Extra executable fields cannot hide an operand from the projection.
+example : acceptBody (ullbc [block [assign 0 (obj
+    [("Use", arr [move 1, .str "Yes"]), ("hidden", move 2)])]
+    (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl
+
+private def structuredStatement (kind : Json) := obj
+  [("span", .null), ("id", 0), ("kind", kind), ("comments_before", arr [])]
+private def structuredBlock (statements : List Json) := obj
+  [("span", .null), ("id", 0), ("statements", arr (statements.map structuredStatement))]
+private def llbc (statements : List Json) := body "Structured" (structuredBlock statements)
+private def structuredDrop (i : Nat) := ctor "Drop" (obj
+  [("kind", .str "Conditional"), ("place", slot i), ("fn_ptr", function),
+    ("on_unwind", structuredBlock [.str "UnwindResume"])])
+
+example : acceptBody (llbc [assign 0 (use (move 1)), structuredDrop 1, .str "Return"]) = true := by with_unfolding_all rfl
+
+-- The drop after Return is a disconnected conservative component. Connecting
+-- it to the preceding move would manufacture an invalid empty fact.
+example : acceptBody (llbc [assign 0 (use (move 1)), .str "Return", structuredDrop 1]) = false := by with_unfolding_all rfl
+example : acceptBody (llbc [assign 0 (use (move 1)), .str "UnwindResume", structuredDrop 1]) = false := by with_unfolding_all rfl
+example : acceptBody (llbc [assign 0 (use (move 1)), ctor "Abort" (.str "UnwindTerminate"),
+    structuredDrop 1]) = false := by with_unfolding_all rfl
+example : acceptBody (llbc [ctor "Loop" (structuredBlock []), structuredDrop 1]) = false := by with_unfolding_all rfl
+example : acceptBody (llbc [ctor "Break" 0, structuredDrop 1]) = false := by with_unfolding_all rfl
+example : acceptBody (llbc [ctor "Continue" 0, structuredDrop 1]) = false := by with_unfolding_all rfl
+
+end AeneasSpecs.DropJson.Tests
diff --git a/verification/aeneas/lean/DropOwnership.lean b/verification/aeneas/lean/DropOwnership.lean
new file mode 100644
index 0000000000..cf329f1038
--- /dev/null
+++ b/verification/aeneas/lean/DropOwnership.lean
@@ -0,0 +1,285 @@
+/- Copyright 2026 The Fuchsia Authors
+
+Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+<LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+This file may not be copied, modified, or distributed except according to
+those terms. -/
+
+module
+public import Std
+@[expose] public section
+
+namespace AeneasSpecs.DropOwnership
+
+/-!
+This module checks a small ownership model, not Rust's memory semantics. A
+concrete state records destruction obligations; it says nothing about bytes
+remaining in storage after a move. The caller must establish that its complete
+body projection preserves evaluation order, all edges, and whole-slot effects.
+It must also establish that an obligation-free conditional drop is silent in
+the compiler interpretation. Those bridges are deliberately separate premises.
+
+Every source component and the designated entry can start with any obligations
+on the declared locals. Consuming a whole slot removes its obligation; defining
+it restores one. Consequently, an assignment must list RHS effects before the
+destination definition. A call's destination must be defined on every successor,
+including unwind. Slot reuse and storage markers restore uncertainty too.
+-/
+
+inductive Effect where
+  | consume (slot : Nat)
+  | define (slot : Nat)
+  deriving Repr, DecidableEq, Inhabited
+
+structure Node where
+  effects : List Effect := []
+  candidateDrop : Option Nat := none
+  successors : List Nat := []
+  deriving Repr, DecidableEq, Inhabited
+
+structure Graph where
+  nodes : List Node
+  localCount : Nat
+  entry : Nat := 0
+  deriving Repr, DecidableEq, Inhabited
+
+def Graph.node (g : Graph) (index : Nat) : Node :=
+  g.nodes[index]?.getD default
+
+def Effect.slot : Effect → Nat
+  | .consume slot | .define slot => slot
+
+/-- Abstract states are conservative sets, represented by finite lists. List
+order and duplicate elements have no semantic significance. -/
+def applyEffect : Effect → List Nat → List Nat
+  | .consume slot, owns => owns.filter (· != slot)
+  | .define slot, owns => slot :: owns
+
+def transfer : List Effect → List Nat → List Nat
+  | [], owns => owns
+  | effect :: rest, owns => transfer rest (applyEffect effect owns)
+
+/-- A certificate gives the incoming may-own set at each node. It is untrusted:
+`check` validates every obligation used by the soundness proof. -/
+abbrev Certificate := Nat → List Nat
+
+def IsRoot (g : Graph) (index : Nat) : Prop :=
+  index = g.entry ∨ ∀ node ∈ g.nodes, index ∉ node.successors
+
+instance (g : Graph) (index : Nat) : Decidable (IsRoot g index) :=
+  inferInstanceAs (Decidable
+    (index = g.entry ∨ ∀ node ∈ g.nodes, index ∉ node.successors))
+
+/-- In addition to ownership closure, validate every slot and successor. The
+strict successor order rejects cycles anywhere, even in a disconnected or
+drop-free component. A candidate drop occurs after this node's ordered effects.
+-/
+def NodeValid (g : Graph) (certificate : Certificate) (index : Nat) : Prop :=
+  let node := g.node index
+  (∀ effect ∈ node.effects, effect.slot < g.localCount) ∧
+  (∀ slot ∈ node.candidateDrop,
+    slot < g.localCount ∧ slot ∉ transfer node.effects (certificate index)) ∧
+  (∀ next ∈ node.successors,
+    index < next ∧ next < g.nodes.length ∧
+      ∀ slot ∈ transfer node.effects (certificate index),
+        slot ∈ certificate next) ∧
+  (IsRoot g index →
+    ∀ slot ∈ List.range g.localCount, slot ∈ certificate index)
+
+instance (g : Graph) (certificate : Certificate) (index : Nat) :
+    Decidable (NodeValid g certificate index) :=
+  inferInstanceAs (Decidable
+    ((∀ effect ∈ (g.node index).effects, effect.slot < g.localCount) ∧
+    (∀ slot ∈ (g.node index).candidateDrop,
+      slot < g.localCount ∧
+        slot ∉ transfer (g.node index).effects (certificate index)) ∧
+    (∀ next ∈ (g.node index).successors,
+      index < next ∧ next < g.nodes.length ∧
+        ∀ slot ∈ transfer (g.node index).effects (certificate index),
+          slot ∈ certificate next) ∧
+    (IsRoot g index →
+      ∀ slot ∈ List.range g.localCount, slot ∈ certificate index)))
+
+def Valid (g : Graph) (certificate : Certificate) : Prop :=
+  g.entry < g.nodes.length ∧
+    ∀ index ∈ List.range g.nodes.length, NodeValid g certificate index
+
+instance (g : Graph) (certificate : Certificate) :
+    Decidable (Valid g certificate) :=
+  inferInstanceAs (Decidable (g.entry < g.nodes.length ∧
+    ∀ index ∈ List.range g.nodes.length, NodeValid g certificate index))
+
+def check (g : Graph) (certificate : Certificate) : Bool :=
+  decide (Valid g certificate)
+
+/-- Infer one finite certificate by forward propagation. Roots begin with all
+locals; joins take union. The result still goes through `check`, so inference
+needs no trusted solver and no completeness theorem. -/
+def infer (g : Graph) : Certificate :=
+  (List.range g.nodes.length).foldl (fun incoming index =>
+    let node := g.node index
+    let outgoing := transfer node.effects (incoming index)
+    fun next => if next ∈ node.successors then
+      outgoing ++ (incoming next).filter (fun slot => slot ∉ outgoing)
+    else incoming next)
+    (fun index => if IsRoot g index then List.range g.localCount else [])
+
+def accepted (g : Graph) : Bool := check g (infer g)
+
+/-- Every accepted edge advances its bounded node index. In particular, a path
+cannot revisit a node, including through an exceptional edge. This condition
+is checked for the whole graph rather than only for reachable drop sites. -/
+theorem checked_edge_forward {g : Graph} {certificate : Certificate}
+    (checked : check g certificate = true) {index next : Nat}
+    (inBounds : index < g.nodes.length)
+    (edge : next ∈ (g.node index).successors) :
+    index < next ∧ next < g.nodes.length := by
+  have valid : Valid g certificate := of_decide_eq_true checked
+  have closure := (valid.2 index (List.mem_range.mpr inBounds)).2.2.1 next edge
+  exact ⟨closure.1, closure.2.1⟩
+
+theorem accepted_edge_forward {g : Graph} (checked : accepted g = true)
+    {index next : Nat} (inBounds : index < g.nodes.length)
+    (edge : next ∈ (g.node index).successors) :
+    index < next ∧ next < g.nodes.length :=
+  checked_edge_forward checked inBounds edge
+
+/-!
+The concrete semantics permits every initial subset of the declared locals.
+It is intentionally independent of the inferred certificate. Branches choose
+any listed successor, so the theorem includes ordinary and exceptional paths.
+-/
+
+abbrev Concrete := Nat → Prop
+
+def concreteEffect : Effect → Concrete → Concrete
+  | .consume slot, owns => fun other => owns other ∧ other ≠ slot
+  | .define slot, owns => fun other => other = slot ∨ owns other
+
+def execute : List Effect → Concrete → Concrete
+  | [], owns => owns
+  | effect :: rest, owns => execute rest (concreteEffect effect owns)
+
+def Covers (possible : List Nat) (owns : Concrete) : Prop :=
+  ∀ slot, owns slot → slot ∈ possible
+
+theorem effect_covers (effect : Effect) {possible : List Nat} {owns : Concrete}
+    (covered : Covers possible owns) :
+    Covers (applyEffect effect possible) (concreteEffect effect owns) := by
+  cases effect with
+  | consume slot =>
+    intro other obligation
+    simp only [concreteEffect] at obligation
+    simp only [applyEffect, List.mem_filter, bne_iff_ne, ne_eq]
+    exact ⟨covered other obligation.1, obligation.2⟩
+  | define slot =>
+    intro other obligation
+    simp only [concreteEffect] at obligation
+    simp only [applyEffect, List.mem_cons]
+    exact obligation.elim Or.inl (fun owned => Or.inr (covered other owned))
+
+theorem transfer_covers (effects : List Effect)
+    {possible : List Nat} {owns : Concrete} (covered : Covers possible owns) :
+    Covers (transfer effects possible) (execute effects owns) := by
+  induction effects generalizing possible owns with
+  | nil => exact covered
+  | cons effect rest induction =>
+    exact induction (effect_covers effect covered)
+
+inductive Reachable (g : Graph) : Nat → Concrete → Prop where
+  | root (index : Nat) (owns : Concrete)
+      (inBounds : index < g.nodes.length) (root : IsRoot g index)
+      (declared : ∀ slot, owns slot → slot < g.localCount) :
+      Reachable g index owns
+  | step {index next : Nat} {owns : Concrete}
+      (before : Reachable g index owns)
+      (edge : next ∈ (g.node index).successors) :
+      Reachable g next (execute (g.node index).effects owns)
+
+/-- Every concrete execution is contained in a checked incoming invariant. -/
+theorem checked_invariant {g : Graph} {certificate : Certificate}
+    (checked : check g certificate = true) {index : Nat} {owns : Concrete}
+    (reached : Reachable g index owns) :
+    index < g.nodes.length ∧ Covers (certificate index) owns := by
+  have valid : Valid g certificate := of_decide_eq_true checked
+  induction reached with
+  | root index owns inBounds root declared =>
+    refine ⟨inBounds, ?_⟩
+    intro slot obligation
+    exact (valid.2 index (List.mem_range.mpr inBounds)).2.2.2 root slot
+      (List.mem_range.mpr (declared slot obligation))
+  | @step index next owns before edge induction =>
+    have nodeValid := valid.2 index (List.mem_range.mpr induction.1)
+    have closure := nodeValid.2.2.1 next edge
+    refine ⟨closure.2.1, ?_⟩
+    intro slot obligation
+    exact closure.2.2 slot (transfer_covers (g.node index).effects
+      induction.2 slot obligation)
+
+/-- The central guarantee: every candidate at every reached occurrence has no
+destruction obligation after its preceding effects. This includes a root in a
+disconnected component and a path chosen through an unwind successor. -/
+theorem checked_drop_empty {g : Graph} {certificate : Certificate}
+    (checked : check g certificate = true) {index slot : Nat} {owns : Concrete}
+    (reached : Reachable g index owns)
+    (candidate : (g.node index).candidateDrop = some slot) :
+    ¬ execute (g.node index).effects owns slot := by
+  have valid : Valid g certificate := of_decide_eq_true checked
+  have invariant := checked_invariant checked reached
+  have empty := (valid.2 index (List.mem_range.mpr invariant.1)).2.1 slot
+    (by simp [candidate])
+  intro obligation
+  exact empty.2 (transfer_covers (g.node index).effects invariant.2
+    slot obligation)
+
+theorem accepted_drop_empty {g : Graph} (checked : accepted g = true)
+    {index slot : Nat} {owns : Concrete} (reached : Reachable g index owns)
+    (candidate : (g.node index).candidateDrop = some slot) :
+    ¬ execute (g.node index).effects owns slot :=
+  checked_drop_empty checked reached candidate
+
+/-!
+This final relation states the conditional-drop interpretation assumed by the
+semantic bridge: when no obligation exists, the operation returns the same
+state silently; when one exists, it may invoke glue or unwind. The theorem
+rules out both active alternatives for an accepted candidate. It does not
+assert that an unconditional/precise drop has this interpretation.
+-/
+
+inductive DropOutcome where
+  | silent
+  | invokeGlue
+  | unwind
+  deriving Repr, DecidableEq
+
+inductive ConditionalDrop (slot : Nat) (before : Concrete) :
+    DropOutcome → Concrete → Prop where
+  | empty (absent : ¬ before slot) : ConditionalDrop slot before .silent before
+  | glue (present : before slot) (after : Concrete) :
+      ConditionalDrop slot before .invokeGlue after
+  | unwind (present : before slot) (after : Concrete) :
+      ConditionalDrop slot before .unwind after
+
+theorem empty_drop_iff {slot : Nat} {before after : Concrete}
+    {outcome : DropOutcome} (absent : ¬ before slot) :
+    ConditionalDrop slot before outcome after ↔
+      outcome = .silent ∧ after = before := by
+  constructor
+  · intro step
+    cases step with
+    | empty => exact ⟨rfl, rfl⟩
+    | glue present => exact False.elim (absent present)
+    | unwind present => exact False.elim (absent present)
+  · rintro ⟨rfl, rfl⟩
+    exact .empty absent
+
+theorem accepted_drop_noop {g : Graph} (checked : accepted g = true)
+    {index slot : Nat} {owns after : Concrete} {outcome : DropOutcome}
+    (reached : Reachable g index owns)
+    (candidate : (g.node index).candidateDrop = some slot) :
+    ConditionalDrop slot (execute (g.node index).effects owns) outcome after ↔
+      outcome = .silent ∧ after = execute (g.node index).effects owns :=
+  empty_drop_iff (accepted_drop_empty checked reached candidate)
+
+end AeneasSpecs.DropOwnership
diff --git a/verification/aeneas/lean/DropOwnershipTests.lean b/verification/aeneas/lean/DropOwnershipTests.lean
new file mode 100644
index 0000000000..faee90fb71
--- /dev/null
+++ b/verification/aeneas/lean/DropOwnershipTests.lean
@@ -0,0 +1,158 @@
+/- Copyright 2026 The Fuchsia Authors
+
+Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+<LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+This file may not be copied, modified, or distributed except according to
+those terms. -/
+
+module
+public import DropOwnership
+@[expose] public section
+
+namespace AeneasSpecs.DropOwnership.Tests
+
+/-!
+These propositions are checked by the kernel. They exercise graph ownership
+and validation; raw-schema, isolation, and exact-snapshot tests belong to the
+decoder and admission integration. A missing effect below models Copy; the raw
+decoder must distinguish that case from unsupported or omitted syntax.
+-/
+
+def moved : Graph :=
+  { nodes := [{ effects := [.consume 0], candidateDrop := some 0 }]
+    localCount := 1 }
+
+example : accepted moved = true := by decide
+
+-- An argument still carries an obligation until a supported move consumes it.
+example : accepted {
+    nodes := [{ candidateDrop := some 0 }], localCount := 1 } = false := by decide
+
+-- Copy leaves ownership unchanged, as does moving a different local.
+example : accepted {
+    nodes := [{ effects := [.consume 1], candidateDrop := some 0 }]
+    localCount := 2 } = false := by decide
+
+-- Whole-local definitions restore ownership, after all RHS operand effects.
+example : accepted {
+    nodes := [{ effects := [.consume 0, .define 0], candidateDrop := some 0 }]
+    localCount := 1 } = false := by decide
+
+-- In contrast, consuming the newly defined value really leaves the slot empty.
+example : accepted {
+    nodes := [{ effects := [.define 0, .consume 0], candidateDrop := some 0 }]
+    localCount := 1 } = true := by decide
+
+-- Slot reuse, storage markers, and call destinations must be definitions. They
+-- cannot establish empty ownership, even after an earlier move.
+example : accepted {
+    nodes := [
+      { effects := [.consume 0], successors := [1] },
+      { effects := [.define 0], successors := [2] },
+      { candidateDrop := some 0 }]
+    localCount := 1 } = false := by decide
+
+def joined (right : List Effect) : Graph :=
+  { nodes := [
+      { successors := [1, 2] },
+      { effects := [.consume 0], successors := [3] },
+      { effects := right, successors := [3] },
+      { candidateDrop := some 0 }]
+    localCount := 1 }
+
+-- Every incoming branch must establish emptiness. Taking union at a join
+-- preserves the obligation from an ordinary or exceptional failure path.
+example : accepted (joined []) = false := by decide
+example : accepted (joined [.consume 0]) = true := by decide
+example : accepted (joined [.consume 0, .define 0]) = false := by decide
+
+-- A call defines its destination on normal and unwind successors alike. Its
+-- preceding argument move does not justify dropping that destination.
+example : accepted {
+    nodes := [
+      { effects := [.consume 0, .define 0], successors := [1, 2] },
+      {},
+      { candidateDrop := some 0 }]
+    localCount := 1 } = false := by decide
+
+-- A disconnected component is independently seeded with every declared local.
+example : accepted {
+    nodes := [
+      { effects := [.consume 0], candidateDrop := some 0 },
+      { candidateDrop := some 0 }]
+    localCount := 1 } = false := by decide
+
+example : accepted {
+    nodes := [
+      { effects := [.consume 0], candidateDrop := some 0 },
+      { effects := [.consume 0], candidateDrop := some 0 }]
+    localCount := 1 } = true := by decide
+
+-- A designated entry is seeded even when it also has incoming edges. The
+-- body's entry cannot inherit a move from a disconnected predecessor.
+example : accepted {
+    nodes := [
+      { effects := [.consume 0], successors := [1] },
+      { candidateDrop := some 0 }]
+    localCount := 1, entry := 1 } = false := by decide
+
+-- Reject cycles everywhere, including disconnected components without drops.
+example : accepted {
+    nodes := [
+      { effects := [.consume 0], candidateDrop := some 0 },
+      { successors := [2] },
+      { successors := [1] }]
+    localCount := 1 } = false := by decide
+
+example : accepted {
+    nodes := [{
+      effects := [.consume 0]
+      candidateDrop := some 0
+      successors := [0] }]
+    localCount := 1 } = false := by decide
+
+-- No invalid graph can gain acceptance through an empty iteration or default
+-- lookup. This includes the entry, successors, move/define operands, and drops.
+example : accepted { nodes := [], localCount := 1 } = false := by decide
+example : accepted { nodes := [{}], localCount := 0, entry := 1 } = false := by decide
+example : accepted {
+    nodes := [{ successors := [1] }], localCount := 0 } = false := by decide
+example : accepted {
+    nodes := [{ effects := [.consume 1], candidateDrop := some 0 }]
+    localCount := 1 } = false := by decide
+example : accepted {
+    nodes := [{ effects := [.define 1] }], localCount := 1 } = false := by decide
+example : accepted {
+    nodes := [{ candidateDrop := some 1 }], localCount := 1 } = false := by decide
+example : accepted {
+    nodes := [{ candidateDrop := some 0 }], localCount := 0 } = false := by decide
+
+-- Untrusted certificates cannot remove initial obligations or forget an
+-- obligation when propagating an edge. This does not depend on `infer`.
+example : check {
+    nodes := [{ candidateDrop := some 0 }], localCount := 1 }
+    (fun _ => []) = false := by decide
+
+example : check {
+    nodes := [{ successors := [1] }, { candidateDrop := some 0 }]
+    localCount := 1 }
+    (fun index => if index = 0 then [0] else []) = false := by decide
+
+-- Instantiate the semantic theorem with an arbitrary concrete initial state.
+-- No test assumes the empty state that it is supposed to establish.
+example (owns : Concrete) (declared : ∀ slot, owns slot → slot < 1) :
+    ¬ execute [.consume 0] owns 0 := by
+  have reached : Reachable moved 0 owns :=
+    .root 0 owns (by decide) (Or.inl rfl) declared
+  exact accepted_drop_empty (by decide : accepted moved = true) reached rfl
+
+example (owns : Concrete) (declared : ∀ slot, owns slot → slot < 1)
+    (outcome : DropOutcome) (after : Concrete) :
+    ConditionalDrop 0 (execute [.consume 0] owns) outcome after ↔
+      outcome = .silent ∧ after = execute [.consume 0] owns := by
+  have reached : Reachable moved 0 owns :=
+    .root 0 owns (by decide) (Or.inl rfl) declared
+  exact accepted_drop_noop (by decide : accepted moved = true) reached rfl
+
+end AeneasSpecs.DropOwnership.Tests