diff --git a/AUDIT.md b/AUDIT.md
index da36459b1..96bbb9320 100644
--- a/AUDIT.md
+++ b/AUDIT.md
@@ -13,15 +13,29 @@ through synthetic compiler-output mutations, plus unsupported source constructs,
 contract `layout at`,
 registered-source symlink escape, and Lean importer digest sensitivity. It also
 checks safe transparent declarations, duplicate aliases, a deliberately
-malformed late declaration and complete registration rollback, plus the pinned
-compiler's checksum. The digest scope is documented in `TRUST_ASSUMPTIONS.md`; it is not a transitive build identity.
+malformed late declaration and complete registration rollback (including the
+named storage view), plus the pinned compiler's checksum. Named-storage checks
+cover `v.totalAssets` dot notation and `#print Storage.shareBalances`, a
+declaration-reorder mutation that moves solc slots while every proof still
+builds, a state-variable rename that makes `Spec.lean` fail to elaborate, and a
+Solidity variable named `Storage` rejected with a source position. Behaviour
+mutations must break both the exact-state lemma and the `*_meets_spec`
+theorem of the affected entry point, and three `Spec.lean` mutations that
+weaken a promise must fail inside the corresponding `*_meets_spec` theorem
+while leaving the exact-state lemmas green. The `spec_named_storage`
+lean_lint rule (in `make check`) rejects every raw `ContractState` accessor
+(the list is read from `Verity/Core.lean`), raw storage fields, direct
+`ContractState` mentions, positional projections, and `knownAddresses` in
+opted-in spec files. The digest scope is documented in `TRUST_ASSUMPTIONS.md`; it is not a transitive build identity.
 
 Evidence command:
 `python3 Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py`
 (after `lake build VaultFromSolidity` and installation of the pinned compiler).
 The focused runner builds and audits the imported execution proofs, changes
 accepted deposit/getter behavior while preserving source mtime and requires old
-proofs to fail, rejects unsupported source, checks unchanged artifacts, and
+proofs to fail at both the exact-state and spec layer, weakens the named spec
+and requires the spec theorems to fail, rejects unsupported source, checks
+unchanged artifacts, and
 exercises Lean-importer and compiler content invalidation. Mutations occur only
 in disposable copies. This is local acceptance evidence, not a new CI job,
 bytecode/runtime test, or proof of translation correctness.
diff --git a/AXIOMS.md b/AXIOMS.md
index b5a1e2e29..0f0ce1935 100644
--- a/AXIOMS.md
+++ b/AXIOMS.md
@@ -6,7 +6,7 @@ This file is the authoritative registry of axioms used by Verity proof code.
 
 `PrintAxioms.lean` includes the imported Vault execution theorems. The focused
 `solidity_importer_test.py` runs `#print axioms` in a disposable audit module for
-every theorem in `Contracts/VaultFromSolidity/Proofs/Execution.lean` and requires
+every theorem in `Contracts/VaultFromSolidity/Proofs/ExecutionProof.lean` and requires
 coverage of all declared theorems, rejecting `sorryAx` and project axioms.
 Its malformed-declaration probe also checks that kernel error recovery does not
 leave any partial declarations or fallback axioms in the import namespace.
diff --git a/Contracts/VaultFromSolidity/Importer/Importer.lean b/Contracts/VaultFromSolidity/Importer/Importer.lean
index 121bfc808..81c89329b 100644
--- a/Contracts/VaultFromSolidity/Importer/Importer.lean
+++ b/Contracts/VaultFromSolidity/Importer/Importer.lean
@@ -6,6 +6,11 @@ import Compiler.Sha256.Engine
 A proof-only Solidity frontend. This module invokes pinned `solc --standard-json`,
 validates a closed typed-AST/storage-layout subset, and directly registers safe,
 transparent Verity definitions. It emits neither an intermediate IR nor Lean source.
+
+Besides the executable model it registers a read-only storage view: `Storage` is a
+synonym for `ContractState`, `Storage.<var>` reads each state variable through its
+`<var>Slot` handle, and `view` coerces a state into it. Specs can then say
+`v.totalAssets` instead of naming a raw slot number.
 -/
 
 open Lean Meta Elab Command
@@ -324,6 +329,7 @@ private partial def validateNode (ctx : SourceContext) (j : Json) : MetaM Unit :
 
 private structure FieldInfo where
   id : Nat
+  var : String
   name : String
   getter : Option String
   slot : Nat
@@ -340,7 +346,8 @@ private structure Frontend where
 private def validName (name : String) : Bool :=
   match name.toList with
   | [] => false
-  | c :: cs => c.isAlpha && cs.all (fun c => c.isAlphanum || c == '_') && name != "sourceDigest"
+  | c :: cs => c.isAlpha && cs.all (fun c => c.isAlphanum || c == '_') &&
+      !["sourceDigest", "Storage", "view"].contains name
 
 private def identifier (ctx : SourceContext) (j : Json) : MetaM String := do
   let name ← str (← field j "name")
@@ -469,7 +476,7 @@ private def parseCompilerOutput (sourcePath : System.FilePath) (logicalPath : St
         let getter := if (← str (← field node "visibility")) == "public" then some name else none
         let slotText ← str (← field entry "slot")
         let some slot := slotText.toNat? | failAt ctx node "invalid storage slot"
-        fields := FieldInfo.mk id (name ++ "Slot") getter slot (typ.startsWith "mapping") :: fields
+        fields := FieldInfo.mk id name (name ++ "Slot") getter slot (typ.startsWith "mapping") :: fields
     | "ErrorDefinition" =>
         let ps ← arr (← field (← field node "parameters") "parameters")
         needAt ctx node ps.isEmpty "only zero-argument custom errors"
@@ -510,10 +517,10 @@ private def seq (m t : Expr) (k : Expr → MetaM Expr) : MetaM Expr :=
     let next ← k x
     mkAppM ``Verity.bind #[m, ← mkLambdaFVars #[x] next]
 
-private def register (name : Name) (value : Expr) : MetaM Unit := do
+private def register (name : Name) (value : Expr) (type? : Option Expr := none) : MetaM Unit := do
   if (← getEnv).contains name then throwError "declaration collision: {name}"
   let value ← instantiateMVars value
-  let type ← instantiateMVars (← inferType value)
+  let type ← instantiateMVars (← type?.getDM (inferType value))
   if value.hasMVar || value.hasFVar || type.hasMVar || type.hasFVar then
     throwError "unclosed imported declaration {name}"
   addDecl (.defnDecl { name, levelParams := [], type, value, hints := .regular 0, safety := .safe })
@@ -742,9 +749,10 @@ private partial def translateParams (frontend : Frontend) (params : List Json) (
 
 private def importFrontend (ns : Name) (frontend : Frontend) : MetaM Unit := do
   if debug.skipKernelTC.get (← getOptions) then throwError "kernel checking must be enabled"
-  let mut names := #[ns ++ `sourceDigest]
+  let mut names := #[ns ++ `sourceDigest, ns ++ `Storage, ns ++ `view]
   for f in frontend.fields do
     names := names.push (ns ++ Name.mkSimple f.name)
+    names := names.push (ns ++ `Storage ++ Name.mkSimple f.var)
     if let some getter := f.getter then names := names.push (ns ++ Name.mkSimple getter)
   for fn in frontend.functions do
     let name ← identifier frontend.source fn
@@ -759,6 +767,22 @@ private def importFrontend (ns : Name) (frontend : Frontend) : MetaM Unit := do
     let name := ns ++ Name.mkSimple f.name
     register name slot
     slots := (f.id, mkConst name) :: slots
+  -- Read-only named storage view. Every reader goes through the registered
+  -- `<var>Slot` handle, so `#print` shows which slot a name denotes.
+  let state := mkConst ``Verity.ContractState
+  let storageView := mkConst (ns ++ `Storage)
+  register (ns ++ `Storage) state
+  for f in frontend.fields do
+    let slot ← mkAppM ``Verity.StorageSlot.slot #[← lookupSlot slots f.id]
+    let value ← withLocalDeclD `v storageView fun v => do
+      if f.mapping then
+        withLocalDeclD `key address fun key =>
+          mkLambdaFVars #[v, key] (mkAppN (mkConst ``Verity.ContractState.readMap) #[v, slot, key])
+      else
+        mkLambdaFVars #[v] (mkAppN (mkConst ``Verity.ContractState.readSlot) #[v, slot])
+    register (ns ++ `Storage ++ Name.mkSimple f.var) value
+  let view ← withLocalDeclD `s state fun s => mkLambdaFVars #[s] s
+  register (ns ++ `view) view (some (← mkArrow state storageView))
   for f in frontend.fields do
     if let some getter := f.getter then
       let slot ← lookupSlot slots f.id
diff --git a/Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py b/Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py
index 4da220b79..b44d9a54a 100644
--- a/Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py
+++ b/Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py
@@ -137,15 +137,15 @@ def source_digest() -> str:
         finally:
             ux_probe.unlink(missing_ok=True)
 
-        proof = root / "Contracts/VaultFromSolidity/Proofs/Execution.lean"
+        proof = root / "Contracts/VaultFromSolidity/Proofs/ExecutionProof.lean"
         proof_text = proof.read_text()
         theorem_names = re.findall(r"^theorem\s+(\w+)", proof_text, re.M)
         audit_file = root / ".lake/solidity-import/AxiomAudit.lean"
         try:
             audit_file.write_text(
-                "import Contracts.VaultFromSolidity.Proofs.Execution\n"
+                "import Contracts.VaultFromSolidity.Proofs.ExecutionProof\n"
                 + "\n".join(
-                    "#print axioms Contracts.VaultFromSolidity.Proofs.Execution." + name
+                    "#print axioms Contracts.VaultFromSolidity.Proofs.ExecutionProof." + name
                     for name in theorem_names
                 )
                 + "\n"
@@ -154,7 +154,7 @@ def source_digest() -> str:
         finally:
             audit_file.unlink(missing_ok=True)
         entries = re.findall(
-            r"'Contracts.VaultFromSolidity.Proofs.Execution.(\w+)' depends on axioms: \[([^\]]*)\]", audit
+            r"'Contracts.VaultFromSolidity.Proofs.ExecutionProof.(\w+)' depends on axioms: \[([^\]]*)\]", audit
         )
         check(set(theorem_names) == {name for name, _ in entries},
               "every theorem appears in actual #print axioms output")
@@ -167,11 +167,14 @@ def source_digest() -> str:
             probe.write_text('''import Contracts.VaultFromSolidity.VaultFromSolidity
 open Lean Elab Command
 #print Contracts.VaultFromSolidity.deposit
+#check fun (v : Contracts.VaultFromSolidity.Storage) => v.totalAssets
+#print Contracts.VaultFromSolidity.Storage.shareBalances
 run_cmd do
   for suffix in ["totalAssetsSlot", "totalSupplySlot", "shareBalancesSlot",
                  "deposit", "withdraw", "balanceOf", "totalAssets", "totalSupply",
-                 "shareBalances", "sourceDigest"] do
-    let name := `Contracts.VaultFromSolidity ++ Name.mkSimple suffix
+                 "shareBalances", "sourceDigest", "Storage", "Storage.totalAssets",
+                 "Storage.totalSupply", "Storage.shareBalances", "view"] do
+    let name := `Contracts.VaultFromSolidity ++ suffix.toName
     let some (.defnInfo info) := (← getEnv).find? name
       | throwError "not a transparent definition: {name}"
     unless info.safety == .safe && !info.value.hasMVar && !info.value.hasFVar do
@@ -210,6 +213,11 @@ def source_digest() -> str:
             check("Verity.setMapping" in output and "Verity.setStorage" in output and
                   "safeAdd" in output,
                   "#print deposit exposes readable source-derived behavior")
+            check("fun v => v.totalAssets : Contracts.VaultFromSolidity.Storage → Verity.Uint256" in output,
+                  "named storage view supports v.totalAssets dot notation")
+            check("def Contracts.VaultFromSolidity.Storage.shareBalances" in output and
+                  "shareBalancesSlot.slot" in output and "readMap" in output,
+                  "#print Storage.shareBalances reads through the named slot handle")
         finally:
             probe.unlink(missing_ok=True)
 
@@ -234,23 +242,90 @@ def source_digest() -> str:
         edit_source(original)
         build()
 
-        for name, theorem, old, new in (
-            ("deposit behavior", "deposit_meets_spec", b"totalSupply += assets;", b"totalSupply = assets;"),
-            ("getter behavior", "balance_meets_spec", b"return shareBalances[account];", b"return totalAssets;"),
+        def slot_numbers() -> list[str]:
+            slot_probe = root / ".lake/solidity-import/SlotProbe.lean"
+            try:
+                slot_probe.write_text(
+                    "import Contracts.VaultFromSolidity.VaultFromSolidity\n"
+                    "#eval [Contracts.VaultFromSolidity.totalAssetsSlot.slot,"
+                    " Contracts.VaultFromSolidity.totalSupplySlot.slot,"
+                    " Contracts.VaultFromSolidity.shareBalancesSlot.slot]\n"
+                )
+                return re.findall(r"\[\d+, \d+, \d+\]", run(root, [LAKE, "env", "lean", str(slot_probe)]))
+            finally:
+                slot_probe.unlink(missing_ok=True)
+
+        declarations = b"    uint256 public totalAssets;\n    uint256 public totalSupply;\n"
+        check(original.count(declarations) == 1 and slot_numbers() == ["[0, 1, 2]"],
+              "baseline storage layout puts totalAssets, totalSupply, shareBalances at slots 0, 1, 2")
+        edit_source(original.replace(
+            declarations, b"    uint256 public totalSupply;\n    uint256 public totalAssets;\n"))
+        build()
+        check(slot_numbers() == ["[1, 0, 2]"],
+              "reordering state variables binds the spec names to the new slots and proofs still pass")
+        edit_source(original)
+        build()
+
+        edit_source(original.replace(b"totalAssets", b"assetsTotal"))
+        output = build(False, "Invalid field `totalAssets`")
+        check(re.search(r"Contracts/VaultFromSolidity/Spec\.lean:\d+:\d+:", output) is not None,
+              "renaming a state variable makes the named spec fail to elaborate")
+        edit_source(original)
+        build()
+
+        def broken_theorems(output: str) -> set[str]:
+            error_lines = [int(value) for value in re.findall(
+                r"Contracts/VaultFromSolidity/Proofs/ExecutionProof\.lean:(\d+):", output)]
+            return {name for name, (start, end) in theorem_ranges.items()
+                    if any(start <= line <= end for line in error_lines)}
+
+        # A behaviour change in Vault.sol must break both the internal exact-state
+        # lemma and the human-facing `*_meets_spec` theorem. Lean adds a failed
+        # theorem with `sorry`, so a spec theorem derived from the exact-state
+        # lemma would keep elaborating; requiring an error inside its own range
+        # shows the spec layer is proved against the imported definitions itself.
+        for name, theorems, old, new in (
+            ("deposit behavior", ("deposit_exact_state", "deposit_meets_spec"),
+             b"totalSupply += assets;", b"totalSupply = assets;"),
+            ("getter behavior", ("balance_exact_state", "balance_meets_spec"),
+             b"return shareBalances[account];", b"return totalAssets;"),
         ):
             check(original.count(old) == 1, name + " mutation has one source target")
             before = artifacts()
             edit_source(original.replace(old, new))
-            output = build(False, "Contracts.VaultFromSolidity.Proofs.Execution")
-            error_lines = [int(value) for value in re.findall(
-                r"Contracts/VaultFromSolidity/Proofs/Execution\.lean:(\d+):", output)]
-            start, end = theorem_ranges[theorem]
-            check(any(start <= line <= end for line in error_lines),
-                  name + f" mutation breaks {theorem}")
+            output = build(False, "Contracts.VaultFromSolidity.Proofs.ExecutionProof")
+            broken = broken_theorems(output)
+            for theorem in theorems:
+                check(theorem in broken, name + f" mutation breaks {theorem}")
             check(before != artifacts(), name + " preserved-mtime edit refreshes artifacts")
             edit_source(original)
             build()
 
+        # The spec layer is not vacuous: a wrong promise in Spec.lean is unprovable
+        # against the unchanged Solidity, and the failure lands in the spec
+        # theorem, not in the exact-state lemmas.
+        spec = root / "Contracts/VaultFromSolidity/Spec.lean"
+        spec_original = spec.read_bytes()
+        for name, theorem, old, new in (
+            ("deposit spec without the supply increment", "deposit_meets_spec",
+             b"post.totalSupply = pre.totalSupply + amount", b"post.totalSupply = pre.totalSupply"),
+            ("withdraw spec without the supply decrement", "withdraw_meets_spec",
+             b"post.totalSupply = pre.totalSupply - amount", b"post.totalSupply = pre.totalSupply"),
+            ("getter spec returning the wrong variable", "balance_meets_spec",
+             b"result = v.shareBalances account", b"result = v.totalSupply"),
+        ):
+            check(spec_original.count(old) == 1, name + " mutation has one spec target")
+            spec.write_bytes(spec_original.replace(old, new))
+            try:
+                output = build(False, "Contracts.VaultFromSolidity.Proofs.ExecutionProof")
+            finally:
+                spec.write_bytes(spec_original)
+            broken = broken_theorems(output)
+            check(theorem in broken, name + f" is unprovable: breaks {theorem}")
+            check(not any(candidate.endswith("_exact_state") for candidate in broken),
+                  name + " leaves the exact-state lemmas untouched")
+        build()
+
         for name, old, new, diagnostic in (
             ("contract layout at", b"contract Vault {", b"contract Vault layout at 100 {", "layout at"),
             ("initializer", b"uint256 public totalAssets;", b"uint256 public totalAssets = 1;", "initializer"),
@@ -258,6 +333,8 @@ def source_digest() -> str:
             ("loop", b"totalAssets += assets;", b"while (assets < totalAssets) { totalAssets += assets; }", "WhileStatement"),
             ("second contract", b"contract Vault {", b"contract Other {}\ncontract Vault {", "exactly one"),
             ("multiplication", b"totalAssets += assets;", b"totalAssets = totalAssets * assets;", "unsupported binary"),
+            ("reserved Storage name", b"uint256 public totalSupply;",
+             b"uint256 public totalSupply;\n    uint256 public Storage;", "unsupported/reserved name"),
         ):
             edit_source(original.replace(old, new))
             output = build(False, diagnostic)
@@ -395,8 +472,10 @@ def mutate(x):
     logInfo m!"EXPECTED_KERNEL_ERROR {e.toMessageData}"
   unless rejected do throwError "malformed declaration accepted"
   for suffix in ["totalAssetsSlot", "totalSupplySlot", "shareBalancesSlot",
-                 "totalAssets", "totalSupply", "shareBalances", "deposit", "sourceDigest"] do
-    if (← getEnv).contains (`Broken ++ Name.mkSimple suffix) then
+                 "totalAssets", "totalSupply", "shareBalances", "deposit", "sourceDigest",
+                 "Storage", "Storage.totalAssets", "Storage.totalSupply",
+                 "Storage.shareBalances", "view"] do
+    if (← getEnv).contains (`Broken ++ suffix.toName) then
       throwError "partial declaration escaped rollback: {suffix}"
   logInfo "KERNEL_REJECTION_ROLLED_BACK"
 ''')
diff --git a/Contracts/VaultFromSolidity/Proofs/Execution.lean b/Contracts/VaultFromSolidity/Proofs/Execution.lean
deleted file mode 100644
index be3f6f54a..000000000
--- a/Contracts/VaultFromSolidity/Proofs/Execution.lean
+++ /dev/null
@@ -1,90 +0,0 @@
-import Contracts.VaultFromSolidity.Spec
-
-/-!
-# Proofs about the Vault imported from Solidity
-
-Two layers, deliberately kept small:
-
-1. `*_meets_spec` -- each entry point produces exactly the state
-   `Spec` describes. These unfold the definitions `Importer.lean` registered
-   from `Vault.sol`, so they fail if the Solidity source changes behaviour.
-2. `*_preserves_solvency` -- the contract-level result. Neither a deposit nor a
-   withdrawal can break the one-for-one backing between assets and issued
-   shares. A reverting call leaves the state untouched (`Contract.run` rolls
-   back), so solvency can only ever be lost on a successful call, which is what
-   these two theorems rule out.
--/
-
-namespace Contracts.VaultFromSolidity.Proofs.Execution
-open Verity
-open Verity.Stdlib.Math
-
-macro "reduce_vault" : tactic => `(tactic|
-  simp_all [Spec.deposit_execution, Spec.withdraw_execution, Spec.balance_execution,
-    Spec.accountingState, deposit, withdraw, balanceOf, totalAssets, totalSupply,
-    shareBalances, totalAssetsSlot, totalSupplySlot, shareBalancesSlot,
-    Contract.run, Bind.bind, Pure.pure, Verity.instMonadContract, Verity.bind, Verity.pure,
-    msgValue, msgSender, Verity.require,
-    getStorage, setStorage, getMapping, setMapping, requireSomeUint, safeSub,
-    Verity.EVM.Uint256.sub, Nat.not_le_of_lt, Nat.not_lt_of_ge,
-    ContractState.readSlot, ContractState.writeSlot, ContractState.readMap,
-    ContractState.writeMap, ContractState.storage, ContractState.storageMap])
-
-/-! ## Exact behaviour of each entry point -/
-
-theorem balance_meets_spec (s : ContractState) (account : Address)
-    (h0 : s.msgValue = 0) : Spec.balance_execution s account := by
-  reduce_vault
-
-theorem deposit_meets_spec (s : ContractState) (amount : Uint256)
-    (h0 : s.msgValue = 0)
-    (hs : safeAdd (s.readMap 2 s.sender) amount = some (s.readMap 2 s.sender + amount))
-    (ha : safeAdd (s.readSlot 0) amount = some (s.readSlot 0 + amount))
-    (ht : safeAdd (s.readSlot 1) amount = some (s.readSlot 1 + amount)) :
-    Spec.deposit_execution s amount := by
-  reduce_vault
-
-theorem withdraw_meets_spec (s : ContractState) (amount : Uint256)
-    (h0 : s.msgValue = 0)
-    (hs : amount.val ≤ (s.readMap 2 s.sender).val)
-    (ha : amount.val ≤ (s.readSlot 0).val)
-    (ht : amount.val ≤ (s.readSlot 1).val) : Spec.withdraw_execution s amount := by
-  reduce_vault
-
-/-! ## The vault stays solvent -/
-
-/-- A successful deposit credits the caller's shares and both totals by the same
-amount, so assets still exactly back the issued shares. -/
-theorem deposit_preserves_solvency (s : ContractState) (amount : Uint256)
-    (h0 : s.msgValue = 0)
-    (hs : safeAdd (s.readMap 2 s.sender) amount = some (s.readMap 2 s.sender + amount))
-    (ha : safeAdd (s.readSlot 0) amount = some (s.readSlot 0 + amount))
-    (ht : safeAdd (s.readSlot 1) amount = some (s.readSlot 1 + amount))
-    (hsolvent : Spec.solvent s) :
-    Spec.solvent ((deposit amount).run s).snd := by
-  have h := deposit_meets_spec s amount h0 hs ha ht
-  rw [Spec.deposit_execution] at h
-  rw [h]
-  simp only [Spec.solvent, Spec.accountingState, ContractResult.snd,
-    ContractState.readSlot, ContractState.writeSlot, ContractState.writeMap,
-    ContractState.storage] at hsolvent ⊢
-  simp [hsolvent]
-
-/-- A successful withdrawal debits the caller's shares and both totals by the
-same amount, so assets still exactly back the issued shares. -/
-theorem withdraw_preserves_solvency (s : ContractState) (amount : Uint256)
-    (h0 : s.msgValue = 0)
-    (hs : amount.val ≤ (s.readMap 2 s.sender).val)
-    (ha : amount.val ≤ (s.readSlot 0).val)
-    (ht : amount.val ≤ (s.readSlot 1).val)
-    (hsolvent : Spec.solvent s) :
-    Spec.solvent ((withdraw amount).run s).snd := by
-  have h := withdraw_meets_spec s amount h0 hs ha ht
-  rw [Spec.withdraw_execution] at h
-  rw [h]
-  simp only [Spec.solvent, Spec.accountingState, ContractResult.snd,
-    ContractState.readSlot, ContractState.writeSlot, ContractState.writeMap,
-    ContractState.storage] at hsolvent ⊢
-  simp [hsolvent]
-
-end Contracts.VaultFromSolidity.Proofs.Execution
diff --git a/Contracts/VaultFromSolidity/Proofs/ExecutionProof.lean b/Contracts/VaultFromSolidity/Proofs/ExecutionProof.lean
new file mode 100644
index 000000000..b8d4b0c36
--- /dev/null
+++ b/Contracts/VaultFromSolidity/Proofs/ExecutionProof.lean
@@ -0,0 +1,126 @@
+import Contracts.VaultFromSolidity.Spec
+
+/-!
+# Proofs about the Vault imported from Solidity
+
+Three layers, deliberately kept small:
+
+1. `*_exact_state` -- internal: each entry point produces exactly this raw
+   `ContractState`, including Verity's ghost key-enumeration metadata. These
+   unfold the definitions `Importer.lean` registered from `Vault.sol`, so they
+   fail if the Solidity source changes behaviour.
+2. `*_meets_spec` -- the named-storage promise from `Spec`. Each states that
+   the call succeeds under its precondition and that the successful post-state
+   (or, for `balanceOf`, the returned value) satisfies the spec. These are
+   proved directly against the imported definitions, not derived from the
+   exact-state lemmas, so a behaviour change in `Vault.sol` breaks them on
+   their own.
+3. `*_preserves_solvency` -- the contract-level result. Neither a deposit nor a
+   withdrawal can break the one-for-one backing between assets and issued
+   shares. A reverting call leaves the state untouched (`Contract.run` rolls
+   back), so solvency can only ever be lost on a successful call, which is what
+   these two theorems rule out.
+
+Slots are only ever referenced through the imported `<var>Slot` handles, so the
+proofs do not depend on the storage-layout order solc picks.
+-/
+
+namespace Contracts.VaultFromSolidity.Proofs.ExecutionProof
+open Verity
+open Verity.Stdlib.Math
+open Spec
+
+/-- Exact post-state of a successful `deposit`/`withdraw`: the caller's share
+balance and both totals move together, including Verity's ghost
+key-enumeration metadata. -/
+def accountingState (s : ContractState) (shares assets supply : Uint256) : ContractState :=
+  let mapped := { s.writeMap shareBalancesSlot.slot s.sender shares with
+    knownAddresses := fun slotIdx => if slotIdx == shareBalancesSlot.slot then
+      (s.knownAddresses slotIdx).insert s.sender else s.knownAddresses slotIdx }
+  (mapped.writeSlot totalAssetsSlot.slot assets).writeSlot totalSupplySlot.slot supply
+
+macro "reduce_vault" : tactic => `(tactic|
+  simp_all [depositFits, withdrawCovered, accountingState, view,
+    Storage.totalAssets, Storage.totalSupply, Storage.shareBalances,
+    deposit, withdraw, balanceOf, totalAssets, totalSupply,
+    shareBalances, totalAssetsSlot, totalSupplySlot, shareBalancesSlot,
+    Contract.run, Bind.bind, Pure.pure, Verity.instMonadContract, Verity.bind, Verity.pure,
+    msgValue, msgSender, Verity.require,
+    getStorage, setStorage, getMapping, setMapping, requireSomeUint, safeAdd, safeSub,
+    Verity.EVM.Uint256.sub, Nat.not_le_of_lt, Nat.not_lt_of_ge,
+    ContractState.readSlot, ContractState.writeSlot, ContractState.readMap,
+    ContractState.writeMap, ContractState.storage, ContractState.storageMap])
+
+/-! ## Exact behaviour of each entry point -/
+
+theorem balance_exact_state (s : ContractState) (account : Address)
+    (h0 : s.msgValue = 0) :
+    (balanceOf account).run s = ContractResult.success ((view s).shareBalances account) s := by
+  reduce_vault
+
+theorem deposit_exact_state (s : ContractState) (amount : Uint256)
+    (h0 : s.msgValue = 0) (hfits : depositFits amount s.sender (view s)) :
+    (deposit amount).run s = ContractResult.success ()
+      (accountingState s ((view s).shareBalances s.sender + amount)
+        ((view s).totalAssets + amount) ((view s).totalSupply + amount)) := by
+  reduce_vault
+
+theorem withdraw_exact_state (s : ContractState) (amount : Uint256)
+    (h0 : s.msgValue = 0) (hcovered : withdrawCovered amount s.sender (view s)) :
+    (withdraw amount).run s = ContractResult.success ()
+      (accountingState s ((view s).shareBalances s.sender - amount)
+        ((view s).totalAssets - amount) ((view s).totalSupply - amount)) := by
+  reduce_vault
+
+/-! ## Each entry point meets its named-storage spec -/
+
+/-- `balanceOf` succeeds, leaves the state untouched, and returns the
+account's shares as `balanceOf_spec` promises. -/
+theorem balance_meets_spec (s : ContractState) (account : Address)
+    (h0 : s.msgValue = 0) :
+    ∃ result, (balanceOf account).run s = ContractResult.success result s ∧
+      balanceOf_spec account result (view s) := by
+  unfold balanceOf_spec
+  reduce_vault
+
+/-- Under `depositFits`, `deposit` succeeds and its post-state satisfies
+`deposit_spec`. -/
+theorem deposit_meets_spec (s : ContractState) (amount : Uint256)
+    (h0 : s.msgValue = 0) (hfits : depositFits amount s.sender (view s)) :
+    ∃ post, (deposit amount).run s = ContractResult.success () post ∧
+      deposit_spec amount s.sender (view s) (view post) := by
+  unfold deposit_spec
+  reduce_vault
+
+/-- Under `withdrawCovered`, `withdraw` succeeds and its post-state satisfies
+`withdraw_spec`. -/
+theorem withdraw_meets_spec (s : ContractState) (amount : Uint256)
+    (h0 : s.msgValue = 0) (hcovered : withdrawCovered amount s.sender (view s)) :
+    ∃ post, (withdraw amount).run s = ContractResult.success () post ∧
+      withdraw_spec amount s.sender (view s) (view post) := by
+  unfold withdraw_spec
+  reduce_vault
+
+/-! ## The vault stays solvent -/
+
+/-- A successful deposit credits the caller's shares and both totals by the same
+amount, so assets still exactly back the issued shares. -/
+theorem deposit_preserves_solvency (s : ContractState) (amount : Uint256)
+    (h0 : s.msgValue = 0) (hfits : depositFits amount s.sender (view s))
+    (hsolvent : solvent (view s)) :
+    solvent (view ((deposit amount).run s).snd) := by
+  obtain ⟨post, hrun, hassets, hsupply, _⟩ := deposit_meets_spec s amount h0 hfits
+  unfold solvent at hsolvent ⊢
+  rw [hrun, ContractResult.snd_success, hassets, hsupply, hsolvent]
+
+/-- A successful withdrawal debits the caller's shares and both totals by the
+same amount, so assets still exactly back the issued shares. -/
+theorem withdraw_preserves_solvency (s : ContractState) (amount : Uint256)
+    (h0 : s.msgValue = 0) (hcovered : withdrawCovered amount s.sender (view s))
+    (hsolvent : solvent (view s)) :
+    solvent (view ((withdraw amount).run s).snd) := by
+  obtain ⟨post, hrun, hassets, hsupply, _⟩ := withdraw_meets_spec s amount h0 hcovered
+  unfold solvent at hsolvent ⊢
+  rw [hrun, ContractResult.snd_success, hassets, hsupply, hsolvent]
+
+end Contracts.VaultFromSolidity.Proofs.ExecutionProof
diff --git a/Contracts/VaultFromSolidity/Spec.lean b/Contracts/VaultFromSolidity/Spec.lean
index 3c7e05dcf..426f5cb97 100644
--- a/Contracts/VaultFromSolidity/Spec.lean
+++ b/Contracts/VaultFromSolidity/Spec.lean
@@ -5,17 +5,20 @@ import Contracts.VaultFromSolidity.VaultFromSolidity
 # What the imported Vault is supposed to do
 
 `Importer.lean` turns `Vault.sol` into ordinary Verity definitions: `deposit`,
-`withdraw`, `balanceOf`, and one `StorageSlot` per state variable
-(slot `0 = totalAssets`, slot `1 = totalSupply`, slot `2 = shareBalances`).
+`withdraw`, `balanceOf`, and a read-only storage view named after the Solidity
+state variables. For `v : Storage`, `v.totalAssets`, `v.totalSupply` and
+`v.shareBalances` read those variables; `view s` is the view of a state `s`.
+The storage-layout slot behind each name comes from solc, not from this file,
+so reordering the Solidity declarations does not change anything here.
 
-This file states two things about them:
+This file only states the promise:
 
 * `solvent` -- the property that matters for the contract as a whole. Shares are
   issued one-for-one against assets, so every share outstanding must stay backed
   by an asset the vault accounts for.
-* `deposit_execution` / `withdraw_execution` / `balance_execution` -- the exact
-  state each entry point produces. These pin down behaviour precisely enough to
-  derive `solvent`, and they are what a Solidity mutation has to break.
+* `deposit_spec` / `withdraw_spec` / `balanceOf_spec` -- what each entry point
+  does to the named storage, under the preconditions `depositFits` /
+  `withdrawCovered`.
 -/
 
 namespace Contracts.VaultFromSolidity.Spec
@@ -23,35 +26,43 @@ namespace Contracts.VaultFromSolidity.Spec
 open Verity
 open Verity.EVM.Uint256
 
-/-- The vault's main invariant: issued shares are exactly backed by assets
-(`totalAssets = totalSupply`). If this ever breaks, shares stop being
-redeemable one-for-one and the vault is insolvent. -/
-def solvent (s : ContractState) : Prop :=
-  s.readSlot 0 = s.readSlot 1
-
-/-- Exact post-state of a successful `deposit`/`withdraw`: the caller's share
-balance and both totals move together, including Verity's ghost
-key-enumeration metadata. -/
-def accountingState (s : ContractState) (shares assets supply : Uint256) : ContractState :=
-  let mapped := { s.writeMap 2 s.sender shares with
-    knownAddresses := fun slotIdx => if slotIdx == 2 then
-      (s.knownAddresses slotIdx).insert s.sender else s.knownAddresses slotIdx }
-  (mapped.writeSlot 0 assets).writeSlot 1 supply
-
-def deposit_execution (s : ContractState) (amount : Uint256) : Prop :=
-  (Contracts.VaultFromSolidity.deposit amount).run s = ContractResult.success ()
-    (accountingState s (s.readMap 2 s.sender + amount)
-      (s.readSlot 0 + amount)
-      (s.readSlot 1 + amount))
-
-def withdraw_execution (s : ContractState) (amount : Uint256) : Prop :=
-  (Contracts.VaultFromSolidity.withdraw amount).run s = ContractResult.success ()
-    (accountingState s (s.readMap 2 s.sender - amount)
-      (s.readSlot 0 - amount)
-      (s.readSlot 1 - amount))
-
-def balance_execution (s : ContractState) (account : Address) : Prop :=
-  (Contracts.VaultFromSolidity.balanceOf account).run s =
-    ContractResult.success (s.readMap 2 account) s
+/-- The vault's main invariant: issued shares are exactly backed by assets.
+If this ever breaks, shares stop being redeemable one-for-one and the vault is
+insolvent. -/
+def solvent (v : Storage) : Prop :=
+  v.totalAssets = v.totalSupply
+
+/-- `deposit(amount)` credits the caller's shares and both totals by `amount`,
+and leaves every other account's shares alone. -/
+def deposit_spec (amount : Uint256) (caller : Address) (pre post : Storage) : Prop :=
+  post.totalAssets = pre.totalAssets + amount ∧
+  post.totalSupply = pre.totalSupply + amount ∧
+  post.shareBalances caller = pre.shareBalances caller + amount ∧
+  ∀ other, other ≠ caller → post.shareBalances other = pre.shareBalances other
+
+/-- `withdraw(amount)` debits the caller's shares and both totals by `amount`,
+and leaves every other account's shares alone. -/
+def withdraw_spec (amount : Uint256) (caller : Address) (pre post : Storage) : Prop :=
+  post.totalAssets = pre.totalAssets - amount ∧
+  post.totalSupply = pre.totalSupply - amount ∧
+  post.shareBalances caller = pre.shareBalances caller - amount ∧
+  ∀ other, other ≠ caller → post.shareBalances other = pre.shareBalances other
+
+/-- `balanceOf(account)` returns the account's shares. -/
+def balanceOf_spec (account : Address) (result : Uint256) (v : Storage) : Prop :=
+  result = v.shareBalances account
+
+/-- A deposit of `amount` overflows none of the three counters it increments. -/
+def depositFits (amount : Uint256) (caller : Address) (v : Storage) : Prop :=
+  (v.shareBalances caller).val + amount.val ≤ Verity.Core.MAX_UINT256 ∧
+  v.totalAssets.val + amount.val ≤ Verity.Core.MAX_UINT256 ∧
+  v.totalSupply.val + amount.val ≤ Verity.Core.MAX_UINT256
+
+/-- A withdrawal of `amount` is covered by the caller's shares and both totals,
+so none of the three guards in `withdraw` reverts. -/
+def withdrawCovered (amount : Uint256) (caller : Address) (v : Storage) : Prop :=
+  amount.val ≤ (v.shareBalances caller).val ∧
+  amount.val ≤ v.totalAssets.val ∧
+  amount.val ≤ v.totalSupply.val
 
 end Contracts.VaultFromSolidity.Spec
diff --git a/Makefile b/Makefile
index 8b7319078..7eda21144 100644
--- a/Makefile
+++ b/Makefile
@@ -165,6 +165,7 @@ check: ## Run local CI-equivalent checks job (no Lean build, no solc)
 	python3 scripts/generate_print_axioms.py --check
 	python3 scripts/generate_trust_surface_report.py --check
 	python3 scripts/lean_lint.py --only proof_length
+	python3 scripts/lean_lint.py --only spec_named_storage
 	python3 scripts/check_issue_1060_integrity.py
 	python3 scripts/update_doc_numbers.py --check
 	python3 -m unittest discover -s scripts -p 'test_*.py' -v
diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index ddc580fa9..da317732e 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -35,7 +35,7 @@ import Contracts.SimpleToken.Proofs.Isolation
 import Contracts.SimpleToken.Proofs.Supply
 import Contracts.Vault.Proofs.Correctness
 import Contracts.Vault.Proofs.Native
-import Contracts.VaultFromSolidity.Proofs.Execution
+import Contracts.VaultFromSolidity.Proofs.ExecutionProof
 import Verity.Proofs.CheckedExternalCallConsumer
 import Verity.Proofs.LoopSimulationResultAware
 import Verity.Proofs.Model.CommonExternalCallEquivalence
@@ -688,12 +688,15 @@ end Verity.AxiomAudit
   Contracts.Vault.Proofs.Native.vaultMinimal_runtime_lowers_native
   Contracts.Vault.Proofs.Native.vaultMinimal_totalAssets_nativeResultsMatchOn_revert_of_nonzero_value
 
-  -- Contracts/VaultFromSolidity/Proofs/Execution.lean
-  Contracts.VaultFromSolidity.Proofs.Execution.balance_meets_spec
-  Contracts.VaultFromSolidity.Proofs.Execution.deposit_meets_spec
-  Contracts.VaultFromSolidity.Proofs.Execution.withdraw_meets_spec
-  Contracts.VaultFromSolidity.Proofs.Execution.deposit_preserves_solvency
-  Contracts.VaultFromSolidity.Proofs.Execution.withdraw_preserves_solvency
+  -- Contracts/VaultFromSolidity/Proofs/ExecutionProof.lean
+  Contracts.VaultFromSolidity.Proofs.ExecutionProof.balance_exact_state
+  Contracts.VaultFromSolidity.Proofs.ExecutionProof.deposit_exact_state
+  Contracts.VaultFromSolidity.Proofs.ExecutionProof.withdraw_exact_state
+  Contracts.VaultFromSolidity.Proofs.ExecutionProof.balance_meets_spec
+  Contracts.VaultFromSolidity.Proofs.ExecutionProof.deposit_meets_spec
+  Contracts.VaultFromSolidity.Proofs.ExecutionProof.withdraw_meets_spec
+  Contracts.VaultFromSolidity.Proofs.ExecutionProof.deposit_preserves_solvency
+  Contracts.VaultFromSolidity.Proofs.ExecutionProof.withdraw_preserves_solvency
 
   -- Verity/Proofs/CheckedExternalCallConsumer.lean
   Verity.Proofs.CheckedExternalCallConsumer.lido_submit_entry_installs_caller_context
@@ -7523,4 +7526,4 @@ end Verity.AxiomAudit
   Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
 ]
 
--- Total: 6958 theorems/lemmas (4968 public, 1990 private, 0 sorry'd)
+-- Total: 6961 theorems/lemmas (4971 public, 1990 private, 0 sorry'd)
diff --git a/README.md b/README.md
index 93120319b..054b950eb 100644
--- a/README.md
+++ b/README.md
@@ -30,9 +30,31 @@ validates and translates them directly, then registers transparent,
 kernel-checked `Verity.Contract` definitions in memory. There is no Python
 frontend, custom serialized IR, generated `.lean`, CompilationModel, or
 bytecode. The example is independent of the
-handwritten `Contracts/Vault` contract. `Spec.lean` states the vault's solvency
-invariant plus the exact post-state of each entry point, and
-`Proofs/Execution.lean` proves them against the imported definitions.
+handwritten `Contracts/Vault` contract.
+
+The importer also registers a read-only storage view named after the Solidity
+state variables, so `Spec.lean` reads like the contract instead of naming raw
+slots:
+
+```lean
+-- before
+def solvent (s : ContractState) : Prop := s.readSlot 0 = s.readSlot 1
+
+-- after
+def solvent (v : Storage) : Prop := v.totalAssets = v.totalSupply
+
+def deposit_spec (amount : Uint256) (caller : Address) (pre post : Storage) : Prop :=
+  post.totalAssets = pre.totalAssets + amount ∧
+  post.totalSupply = pre.totalSupply + amount ∧
+  post.shareBalances caller = pre.shareBalances caller + amount ∧
+  ∀ other, other ≠ caller → post.shareBalances other = pre.shareBalances other
+```
+
+Each `Storage.<var>` reader goes through the `<var>Slot` handle solc's storage
+layout produced, so reordering the Solidity declarations moves the slots without
+touching the spec, and renaming a variable makes the spec fail to elaborate.
+`Proofs/ExecutionProof.lean` proves the spec and solvency preservation against
+the imported definitions.
 
 With the Lean/package prerequisites installed, put the official Linux-amd64 solc
 0.8.33 binary at `.lake/solidity-import/solc` and make it executable. Its accepted
diff --git a/TRUST_ASSUMPTIONS.md b/TRUST_ASSUMPTIONS.md
index d180ca025..64a0d8ce3 100644
--- a/TRUST_ASSUMPTIONS.md
+++ b/TRUST_ASSUMPTIONS.md
@@ -29,9 +29,13 @@ closed subset, resolves IDs/types/storage slots, and constructs expressions
 through explicit `translateExpr` / `translateStmt` cases. Declaration
 registration disables asynchronous kernel checking inside the transaction,
 restores the pre-import environment on failure, checks every body against its
-typed return signature, and registers safe transparent definitions. The
-frontend emits no generated Lean source and keeps no serialized AST/model
-cache.
+typed return signature, and registers safe transparent definitions. The same
+transaction registers the named storage view: `Storage` (a definition equal to
+`ContractState`), one `Storage.<var>` reader per state variable that reads
+through the imported `<var>Slot` handle, and `view : ContractState → Storage`.
+These are safe transparent `defnDecl`s like the rest; `Storage` and `view` are
+reserved Solidity names. The frontend emits no generated Lean source and keeps
+no serialized AST/model cache.
 
 The accepted fragment covers the existing Vault: full-width scalars,
 address-to-uint256 mappings and public getters, straight-line reads/writes,
@@ -49,8 +53,15 @@ withdrawal. Revert-path behaviour (nonpayability, insufficient
 shares/assets/supply, late-overflow rollback) is exercised by the acceptance
 suite, not proved here.
 
-The specification and execution proof file refer directly to the imported
-definitions. Zero-argument custom errors use Verity's `Name()` model convention;
+The specification states its promises over the imported storage view
+(`v.totalAssets`, `v.shareBalances account`) rather than raw slot numbers; the
+execution proof file relates that view to the imported definitions. Each
+`*_meets_spec` theorem asserts that the call succeeds under its precondition
+and that the successful post-state (or returned value) meets the spec, so a
+reverting implementation cannot satisfy it; the internal `*_exact_state` lemmas
+pin the full raw post-state. The view adds no
+trust: each reader unfolds to `ContractState.readSlot`/`readMap` at the slot
+solc's storage layout assigned. Zero-argument custom errors use Verity's `Name()` model convention;
 arithmetic panic strings remain a model representation, not an assertion of
 matching EVM revert bytes. The statements do not assert full equivalence of all
 executions or all public/deployment interfaces.
diff --git a/artifacts/verification_status.json b/artifacts/verification_status.json
index b93a6f999..9ab98a9a2 100644
--- a/artifacts/verification_status.json
+++ b/artifacts/verification_status.json
@@ -18,8 +18,8 @@
     "categories": 16,
     "coverage_percent": 76,
     "covered": 255,
-    "excluded": 79,
-    "non_stdlib_total": 334,
+    "excluded": 82,
+    "non_stdlib_total": 337,
     "per_contract": {
       "Counter": 31,
       "ERC20": 22,
@@ -36,11 +36,11 @@
       "SimpleStorage": 20,
       "SimpleToken": 61,
       "Vault": 9,
-      "VaultFromSolidity": 5
+      "VaultFromSolidity": 8
     },
-    "proven": 334,
+    "proven": 337,
     "stdlib": 0,
-    "total": 334
+    "total": 337
   },
   "toolchain": {
     "lean": "leanprover/lean4:v4.31.0",
diff --git a/docs-site/public/llms.txt b/docs-site/public/llms.txt
index 5abfb5b45..03056dd65 100644
--- a/docs-site/public/llms.txt
+++ b/docs-site/public/llms.txt
@@ -33,7 +33,7 @@ Every transition inside the proof envelope is either fully verified or recorded
 - **Language**: Lean 4.31.0
 - **Core Size**: 2040 lines
 - **Verified Contracts**: 16 (Counter, ERC20, ERC721, Ledger, LocalObligationMacroSmoke, Ownable, Owned, OwnedCounter, OwnedCounterComposed, ReentrancyExample, ReentrancyRelyGuarantee, SafeCounter, SimpleStorage, SimpleToken, Vault, VaultFromSolidity)
-- **Theorems**: 334 across 16 categories, 334 fully proven
+- **Theorems**: 337 across 16 categories, 337 fully proven
 - **Axioms**: 1 documented Lean axioms (see AXIOMS.md)
 - **Tests**: 528 Foundry tests, 239 property tests
 - **Build**: `lake build` verifies all proofs
diff --git a/docs/VERIFICATION_STATUS.md b/docs/VERIFICATION_STATUS.md
index ad95f3677..c8d367ce8 100644
--- a/docs/VERIFICATION_STATUS.md
+++ b/docs/VERIFICATION_STATUS.md
@@ -39,13 +39,13 @@ EVM Bytecode
 | ERC20 | 22 | Baseline | `Contracts/ERC20/Proofs/` |
 | ERC721 | 11 | Baseline | `Contracts/ERC721/Proofs/` |
 | Vault | 9 | Baseline | `Contracts/Vault/Proofs/` |
-| VaultFromSolidity | 5 | Proof-only import | `Contracts/VaultFromSolidity/Proofs/` |
+| VaultFromSolidity | 8 | Proof-only import | `Contracts/VaultFromSolidity/Proofs/` |
 | ReentrancyExample | 5 | Complete | `Contracts/ReentrancyExample/Contract.lean` |
 | ReentrancyRelyGuarantee | 10 | Semantic | `Contracts/ReentrancyRelyGuarantee/Contract.lean` |
 | CryptoHash | 0 | No specs | `Contracts/CryptoHash/Contract.lean` |
-| **Total** | **334** | **✅ 100%** | — |
+| **Total** | **337** | **✅ 100%** | — |
 
-> **Note**: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (334 total properties).
+> **Note**: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (337 total properties).
 
 Layer 1 uses macro-generated EDSL-to-`CompilationModel` bridge theorems backed by a generic typed-IR compilation-correctness theorem ([`TypedIRCompilerCorrectness.lean`](../Compiler/TypedIRCompilerCorrectness.lean)). Tuple/bytes/fixed-array/dynamic-array/string parameters now stay inside that proof path when they are carried as ABI head words/offsets. Advanced constructs beyond that typed-IR head-word surface (linked libraries, ECMs, fully custom ABI behavior) are still expressed directly in `CompilationModel` and trusted at that boundary. Higher-order internal helpers (function-pointer parameters, [#1747](https://github.com/lfglabs-dev/verity/issues/1747)) are eliminated by a compile-time monomorphization pre-pass that runs before any lowering, so the `CompilationModel` only ever contains first-order helpers: these calls are covered by the existing first-order proof path and introduce no new boundary trust.
 
@@ -203,7 +203,7 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co
 |----------|----------|------------|
 | ERC20 | 86% (19/22) | 3 proof-only |
 | Vault | 0% (0/9) | 9 proof-only |
-| VaultFromSolidity | 0% (0/5) | 5 proof-only |
+| VaultFromSolidity | 0% (0/8) | 8 proof-only |
 | ERC721 | 100% (11/11) | 0 |
 | SafeCounter | 100% (25/25) | 0 |
 | ReentrancyExample | 100% (5/5) | 0 |
@@ -219,11 +219,11 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co
 | Counter | 74% (23/31) | 8 proof-only |
 | Stdlib | 0% (0/0) | 0 proof-only |
 
-**Status**: 76% coverage (255/334), 79 remaining exclusions all proof-only
+**Status**: 76% coverage (255/337), 82 remaining exclusions all proof-only
 
-- **Total Properties**: 334
+- **Total Properties**: 337
 - **Covered**: 255
-- **Excluded**: 79 (all proof-only)
+- **Excluded**: 82 (all proof-only)
 
 **Proof-Only Properties (74 exclusions)**: Internal proof machinery that cannot be tested in Foundry.
 
diff --git a/lakefile.lean b/lakefile.lean
index ce4192c8c..4d1a06dd1 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -44,7 +44,7 @@ lean_lib «VaultSolidityImporter» where
 lean_lib «VaultFromSolidity» where
   globs := #[.one `Contracts.VaultFromSolidity.VaultFromSolidity,
     .one `Contracts.VaultFromSolidity.Spec,
-    .one `Contracts.VaultFromSolidity.Proofs.Execution]
+    .one `Contracts.VaultFromSolidity.Proofs.ExecutionProof]
   needs := #[vaultSolidity, vaultLeanImporter, vaultSolc, vaultBuildPolicy]
 
 lean_lib «Contracts» where
diff --git a/scripts/REFERENCE.md b/scripts/REFERENCE.md
index ccd19c252..e88b2d717 100644
--- a/scripts/REFERENCE.md
+++ b/scripts/REFERENCE.md
@@ -33,7 +33,7 @@ This document is the long-form reference for script responsibilities.
 
 Primary guards:
 - `property_pipeline.py`: consolidated property manifest/coverage pipeline (P7 Cluster C). Subcommands: `check [--only manifest|coverage|lean-sync]` (single manifest parse for all three checks), `extract` (regenerate `test/property_manifest.json`), `report` (coverage statistics; `--format`, `--fail-below`). The five legacy scripts (`check_property_manifest.py`, `check_property_coverage.py`, `check_property_manifest_sync.py`, `extract_property_manifest.py`, `report_property_coverage.py`) remain as thin shims.
-- `lean_lint.py`: consolidated Lean structure/hygiene lint runner (P7 Cluster E). Dispatcher over rule modules with `--only/--skip/--list`; rules: `contract_structure`, `paths`, `compilationmodel_split`, `axioms`, `trust_surface_registry`, `storage_layout`, `lean_hygiene`, `split_compiler_test_artifacts`, `rewrite_proof_metadata`, `proof_length`. Each rule module (the legacy `check_*.py` file) keeps its logic and stays directly runnable for arg-bearing CI invocations.
+- `lean_lint.py`: consolidated Lean structure/hygiene lint runner (P7 Cluster E). Dispatcher over rule modules with `--only/--skip/--list`; rules: `contract_structure`, `paths`, `compilationmodel_split`, `axioms`, `trust_surface_registry`, `storage_layout`, `lean_hygiene`, `split_compiler_test_artifacts`, `rewrite_proof_metadata`, `proof_length`, `spec_named_storage`. Each rule module (the legacy `check_*.py` file) keeps its logic and stays directly runnable for arg-bearing CI invocations.
 - `check_axioms.py`: validate AXIOMS.md registry locations and parse `PrintAxioms.lean` dependency output (lean_lint rule `axioms`).
 - `check_paths.py`: detect case-insensitive checkout hazards and enforce universal Layer-2 bridge quantification (lean_lint rule `paths`).
 - `check_property_manifest.py`: shim for `property_pipeline.py check --only manifest`.
@@ -50,6 +50,7 @@ Primary guards:
 - `generate_storage_layout_report.py`: emit the per-contract storage layout JSON artifact (`artifacts/storage_layout_report.json`) and human-readable summary (`artifacts/STORAGE_LAYOUT_SUMMARY.md`) for migration/audit review (#1897). The Lean executable `verity-storage-layout-report` is the JSON source of truth; `--check --no-lean` is the drift gate run by `make check`.
 - `check_lean_hygiene.py` (lean_lint rule `lean_hygiene`; the sorry/native_decide gate)
 - `check_proof_length.py` (lean_lint rule `proof_length`)
+- `check_spec_named_storage.py` (lean_lint rule `spec_named_storage`): opted-in human-facing specs (starting with `Contracts/VaultFromSolidity/Spec.lean`) must use named storage views: no raw `ContractState` accessor (list read from `Verity/Core.lean`), storage field, direct `ContractState` mention, positional projection, or `knownAddresses`.
 - `check_macro_health.py`
 - `check_compiler_boundaries.py`
 - `test_check_struct_mapping_surface_sync.py`: unit coverage for the struct-mapping doc sync guard.
diff --git a/scripts/check_spec_named_storage.py b/scripts/check_spec_named_storage.py
new file mode 100644
index 000000000..fa2b1a640
--- /dev/null
+++ b/scripts/check_spec_named_storage.py
@@ -0,0 +1,130 @@
+#!/usr/bin/env python3
+"""Named-storage gate for human-facing specs.
+
+A spec should say `v.totalAssets`, not `s.readSlot 0`: a wrong slot number
+silently points the promise at another variable, and the reader has to trust a
+comment to know what the number means. Opted-in spec files therefore must not
+touch `ContractState` directly at all: no raw accessor (`readSlot`, `readMap`,
+`readMapUint`, `readTransient`, ...), no raw storage field, no `ContractState`
+mention, no positional projection, and no Verity ghost `knownAddresses`
+bookkeeping. Names come from a generated storage view (see
+`Contracts/VaultFromSolidity/Importer/Importer.lean`); `Storage` is a
+transparent definition equal to `ContractState`, so the gate rejects the
+accessor names wherever they appear rather than trying to spot a numeric slot
+argument after them.
+
+The raw accessor list is read from `Verity/Core.lean` (every definition in the
+`ContractState` namespace plus the storage-backing fields), so a new accessor
+is covered without editing this file.
+
+The gate is opt-in per file: handwritten contracts still state specs over raw
+slots and are not listed yet.
+
+Usage:
+    python3 scripts/check_spec_named_storage.py
+"""
+
+from __future__ import annotations
+
+import re
+import sys
+from pathlib import Path
+
+from property_utils import ROOT, scrub_lean_code
+
+SPEC_FILES = (
+    "Contracts/VaultFromSolidity/Spec.lean",
+)
+
+CORE_LEAN = "Verity/Core.lean"
+
+# Fields of `ContractState` that back storage or its ghost bookkeeping.
+STORAGE_FIELDS = ("storageWords", "storageArray", "knownAddresses")
+
+# Ways to take a `Storage`/`ContractState` value apart without naming a field.
+STRUCTURE_ESCAPES = ("mk", "rec", "recOn", "casesOn", "noConfusion")
+
+_DEF_RE = re.compile(
+    r"^(?:@\[[^\]]*\]\s*)?(?:private\s+|protected\s+|noncomputable\s+)*"
+    r"(?:def|abbrev|theorem|instance)\s+([A-Za-z_][\w'?!]*)",
+    re.M,
+)
+
+
+def raw_accessors(core_text: str) -> frozenset[str]:
+    """Every name defined inside `namespace ContractState` in `core_text`."""
+    names: set[str] = set()
+    depth = 0
+    for line in scrub_lean_code(core_text).splitlines():
+        stripped = line.strip()
+        if stripped == "namespace ContractState":
+            depth += 1
+            continue
+        if stripped == "end ContractState":
+            depth = max(depth - 1, 0)
+            continue
+        if depth and (match := _DEF_RE.match(line)):
+            names.add(match.group(1))
+    return frozenset(names)
+
+
+RAW_ACCESSORS = raw_accessors((ROOT / CORE_LEAN).read_text(encoding="utf-8"))
+
+
+def _identifier_re(names: tuple[str, ...] | frozenset[str]) -> re.Pattern[str]:
+    alternatives = "|".join(re.escape(name) for name in sorted(names))
+    return re.compile(r"(?<![\w'])(?:" + alternatives + r")(?![\w'?!])")
+
+
+ACCESSOR_RE = _identifier_re(RAW_ACCESSORS)
+FIELD_RE = _identifier_re(STORAGE_FIELDS)
+CONTRACT_STATE_RE = re.compile(r"(?<![\w'])ContractState(?![\w'])")
+STRUCTURE_ESCAPE_RE = re.compile(
+    r"(?<![\w'])(?:Storage|ContractState)\.(?:" + "|".join(STRUCTURE_ESCAPES) + r")(?![\w'])"
+)
+# `v.1`, `(view s).2`: positional projections out of the storage view.
+PROJECTION_RE = re.compile(r"(?<=[A-Za-z_')\]])\.\d+")
+
+
+def find_violations(text: str) -> list[tuple[int, str]]:
+    """Return `(line, message)` for every raw storage reference in Lean `text`."""
+    violations: list[tuple[int, str]] = []
+    for line_no, line in enumerate(scrub_lean_code(text).splitlines(), 1):
+        for match in ACCESSOR_RE.finditer(line):
+            violations.append((line_no, f"raw `ContractState` accessor `{match.group(0)}`"))
+        for match in FIELD_RE.finditer(line):
+            if match.group(0) == "knownAddresses":
+                violations.append((line_no, "`knownAddresses` ghost bookkeeping"))
+            else:
+                violations.append((line_no, f"raw storage field `{match.group(0)}`"))
+        if CONTRACT_STATE_RE.search(line):
+            violations.append((line_no, "`ContractState` named directly"))
+        for match in STRUCTURE_ESCAPE_RE.finditer(line):
+            violations.append((line_no, f"structure eliminator `{match.group(0)}`"))
+        for match in PROJECTION_RE.finditer(line):
+            violations.append((line_no, f"positional projection `{match.group(0)}`"))
+    return violations
+
+
+def main() -> int:
+    errors: list[str] = []
+    if not RAW_ACCESSORS:
+        errors.append(f"{CORE_LEAN}: found no definitions in `namespace ContractState`")
+    for rel in SPEC_FILES:
+        path = ROOT / rel
+        if not path.is_file():
+            errors.append(f"{rel}: opted-in spec file is missing")
+            continue
+        for line_no, message in find_violations(path.read_text(encoding="utf-8")):
+            errors.append(f"{rel}:{line_no}: {message}; use the named storage view instead")
+    if errors:
+        print("Spec named-storage check failed:", file=sys.stderr)
+        for error in errors:
+            print(f"  - {error}", file=sys.stderr)
+        return 1
+    print(f"Spec named-storage check passed ({len(SPEC_FILES)} opted-in spec files).")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/scripts/lean_lint.py b/scripts/lean_lint.py
index 9fd2f3c1b..ad86c789d 100644
--- a/scripts/lean_lint.py
+++ b/scripts/lean_lint.py
@@ -35,6 +35,7 @@
     "split_compiler_test_artifacts": "check_split_compiler_test_artifacts",
     "rewrite_proof_metadata": "check_rewrite_proof_metadata",
     "proof_length": "check_proof_length",
+    "spec_named_storage": "check_spec_named_storage",
 }
 
 
diff --git a/scripts/test_check_spec_named_storage.py b/scripts/test_check_spec_named_storage.py
new file mode 100644
index 000000000..c82a258ed
--- /dev/null
+++ b/scripts/test_check_spec_named_storage.py
@@ -0,0 +1,123 @@
+#!/usr/bin/env python3
+"""Tests for the spec named-storage gate."""
+
+from __future__ import annotations
+
+import contextlib
+import io
+import tempfile
+import unittest
+from pathlib import Path
+
+import check_spec_named_storage
+
+NAMED_SPEC = '''\
+namespace Contracts.VaultFromSolidity.Spec
+/-- Never write `s.readSlot 0` or `ContractState.readMap s 2 a` here. -/
+def solvent (v : Storage) : Prop := v.totalAssets = v.totalSupply
+def balanceOf_spec (account : Address) (result : Uint256) (v : Storage) : Prop :=
+  result = v.shareBalances account
+def depositFits (amount : Uint256) (v : Storage) : Prop :=
+  v.totalAssets.val + amount.val ≤ Verity.Core.MAX_UINT256
+def label : String := "readMap 2"
+def storage2 (v : Storage) := v.totalSupply
+def readSlotted (v : Storage) := v.totalSupply
+end Contracts.VaultFromSolidity.Spec
+'''
+
+RAW_SPEC = '''\
+namespace Contracts.VaultFromSolidity.Spec
+def solvent (s : ContractState) : Prop := s.readSlot 0 = s.readSlot 1
+def balance (s : Storage) (a : Address) := ContractState.readMap s 2 a
+def raw (s : Storage) := s.storage (1)
+def ghost (s : Storage) := s.knownAddresses
+end Contracts.VaultFromSolidity.Spec
+'''
+
+# Each of these addressed storage by number while passing the first version of
+# the gate, which only looked for a numeric literal right after a short list of
+# accessor names on the same line.
+BYPASSES = (
+    ("def f (v : Storage) := v.readMapUint 3 k", "raw `ContractState` accessor `readMapUint`"),
+    ("def f (v : Storage) := v.readTransient 1", "raw `ContractState` accessor `readTransient`"),
+    ("def f (v : Storage) := v.readSlot\n    0", "raw `ContractState` accessor `readSlot`"),
+    ("def f (s : Storage) := ContractState.readSlot (s) 2", "`ContractState` named directly"),
+    ("def f (s : Storage) := s.readSlot <| 0", "raw `ContractState` accessor `readSlot`"),
+    ("def f (s : Storage) := (s.storage) 0", "raw `ContractState` accessor `storage`"),
+    ("def f (s : Storage) := s.readSlot totalAssetsSlot.slot", "raw `ContractState` accessor `readSlot`"),
+    ("def f (s : Storage) := s.storageWords key", "raw storage field `storageWords`"),
+    ("def f (s : Storage) := s.1 0", "positional projection `.1`"),
+    ("def f (s : Storage) := Storage.casesOn s fun w _ _ => w", "structure eliminator `Storage.casesOn`"),
+    ("def f (s : Storage) := Verity.ContractState.readSlot s 0", "`ContractState` named directly"),
+)
+
+
+class SpecNamedStorageTests(unittest.TestCase):
+    def run_gate(self, spec: str) -> tuple[int, str]:
+        with tempfile.TemporaryDirectory() as tmpdir:
+            root = Path(tmpdir)
+            target = root / check_spec_named_storage.SPEC_FILES[0]
+            target.parent.mkdir(parents=True)
+            target.write_text(spec, encoding="utf-8")
+            old_root = check_spec_named_storage.ROOT
+            output = io.StringIO()
+            try:
+                check_spec_named_storage.ROOT = root
+                with contextlib.redirect_stdout(output), contextlib.redirect_stderr(output):
+                    status = check_spec_named_storage.main()
+            finally:
+                check_spec_named_storage.ROOT = old_root
+            return status, output.getvalue()
+
+    def test_accessors_come_from_core(self) -> None:
+        accessors = check_spec_named_storage.RAW_ACCESSORS
+        for name in ("readSlot", "writeSlot", "readMap", "writeMap", "readMapUint",
+                     "readTransient", "storage", "storageMap", "readArray"):
+            self.assertIn(name, accessors)
+        self.assertNotIn("Contract", accessors)
+        self.assertEqual(check_spec_named_storage.raw_accessors("def readSlot := 0\n"), frozenset())
+
+    def test_named_spec_passes(self) -> None:
+        status, output = self.run_gate(NAMED_SPEC)
+        self.assertEqual(status, 0, output)
+
+    def test_raw_slot_spec_fails(self) -> None:
+        status, output = self.run_gate(RAW_SPEC)
+        self.assertEqual(status, 1)
+        self.assertEqual(
+            check_spec_named_storage.find_violations(RAW_SPEC),
+            [
+                (2, "raw `ContractState` accessor `readSlot`"),
+                (2, "raw `ContractState` accessor `readSlot`"),
+                (2, "`ContractState` named directly"),
+                (3, "raw `ContractState` accessor `readMap`"),
+                (3, "`ContractState` named directly"),
+                (4, "raw `ContractState` accessor `storage`"),
+                (5, "`knownAddresses` ghost bookkeeping"),
+            ],
+        )
+        self.assertIn("Spec.lean:2:", output)
+
+    def test_bypasses_are_rejected(self) -> None:
+        for spec, message in BYPASSES:
+            with self.subTest(spec=spec):
+                messages = [m for _, m in check_spec_named_storage.find_violations(spec)]
+                self.assertIn(message, messages)
+                self.assertEqual(self.run_gate(spec)[0], 1)
+
+    def test_missing_opted_in_file_fails(self) -> None:
+        old_root = check_spec_named_storage.ROOT
+        output = io.StringIO()
+        with tempfile.TemporaryDirectory() as tmpdir:
+            try:
+                check_spec_named_storage.ROOT = Path(tmpdir)
+                with contextlib.redirect_stderr(output):
+                    status = check_spec_named_storage.main()
+            finally:
+                check_spec_named_storage.ROOT = old_root
+        self.assertEqual(status, 1)
+        self.assertIn("opted-in spec file is missing", output.getvalue())
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/scripts/test_lean_lint.py b/scripts/test_lean_lint.py
index 4f170d47e..a39f3eaa0 100644
--- a/scripts/test_lean_lint.py
+++ b/scripts/test_lean_lint.py
@@ -24,6 +24,7 @@ def test_expected_rules_registered(self) -> None:
                 "split_compiler_test_artifacts",
                 "rewrite_proof_metadata",
                 "proof_length",
+                "spec_named_storage",
             },
         )
 
diff --git a/scripts/verify_sync_spec.json b/scripts/verify_sync_spec.json
index 62caf2be2..c52b5a357 100644
--- a/scripts/verify_sync_spec.json
+++ b/scripts/verify_sync_spec.json
@@ -814,6 +814,7 @@
     "python3 scripts/generate_evmyullean_native_lowering_report.py --check",
     "python3 scripts/generate_print_axioms.py --check",
     "python3 scripts/lean_lint.py --only proof_length",
+    "python3 scripts/lean_lint.py --only spec_named_storage",
     "python3 scripts/check_issue_1060_integrity.py",
     "python3 -m unittest discover -s scripts -p 'test_*.py' -v"
   ],
diff --git a/scripts/verify_sync_spec_source.py b/scripts/verify_sync_spec_source.py
index 2a62ca9eb..d15cd8ebc 100644
--- a/scripts/verify_sync_spec_source.py
+++ b/scripts/verify_sync_spec_source.py
@@ -700,6 +700,7 @@
                                       '--check',
                                       'python3 scripts/generate_print_axioms.py --check',
                                       'python3 scripts/lean_lint.py --only proof_length',
+                                      'python3 scripts/lean_lint.py --only spec_named_storage',
                                       'python3 scripts/check_issue_1060_integrity.py',
                                       "python3 -m unittest discover -s scripts -p 'test_*.py' -v"],
  'expected_checks_other_commands': [],
diff --git a/test/property_exclusions.json b/test/property_exclusions.json
index e8d020fa3..34f361f0f 100644
--- a/test/property_exclusions.json
+++ b/test/property_exclusions.json
@@ -16,9 +16,12 @@
   "vaultMinimal_totalAssets_nativeResultsMatchOn_revert_of_nonzero_value"
  ],
  "VaultFromSolidity": [
+  "balance_exact_state",
   "balance_meets_spec",
+  "deposit_exact_state",
   "deposit_meets_spec",
   "deposit_preserves_solvency",
+  "withdraw_exact_state",
   "withdraw_meets_spec",
   "withdraw_preserves_solvency"
  ],
diff --git a/test/property_manifest.json b/test/property_manifest.json
index db7b8830a..d3b27cbb0 100644
--- a/test/property_manifest.json
+++ b/test/property_manifest.json
@@ -359,9 +359,12 @@
     "vaultMinimal_totalAssets_nativeResultsMatchOn_revert_of_nonzero_value"
   ],
   "VaultFromSolidity": [
+    "balance_exact_state",
     "balance_meets_spec",
+    "deposit_exact_state",
     "deposit_meets_spec",
     "deposit_preserves_solvency",
+    "withdraw_exact_state",
     "withdraw_meets_spec",
     "withdraw_preserves_solvency"
   ]