diff --git a/Contracts/Smoke/Helpers.lean b/Contracts/Smoke/Helpers.lean
index 3be67609e..712c2fecf 100644
--- a/Contracts/Smoke/Helpers.lean
+++ b/Contracts/Smoke/Helpers.lean
@@ -30,4 +30,501 @@ def plusInt256Helper (a : Uint256) (b : Int256) : Uint256 :=
 def eqWordHelper (a : Uint256) (b : Uint256) : Uint256 :=
   if a = b then 1 else 0
 
+verity_contract ModifierInheritanceBase where
+  types
+    InheritedValue : Uint256
+  storage
+    owner : Address := slot 0
+
+  constructor (initialOwner : Address) := do
+    setStorageAddr owner initialOwner
+
+  modifier onlyOwner := do
+    let sender ← msgSender
+    let currentOwner ← getStorageAddr owner
+    require (sender == currentOwner) "Caller is not the owner"
+
+  function virtual value () : Uint256 := do
+    return 1
+
+verity_contract ModifierInheritanceChild is ModifierInheritanceBase where
+  storage
+    counter : Uint256 := slot 1
+
+  constructor (initialOwner : Address) ModifierInheritanceBase(initialOwner) := do
+    setStorage counter 7
+
+  function bump () with onlyOwner : Unit := do
+    -- Modifier-local bindings have their own scope and may be reused here.
+    let sender ← getStorage counter
+    setStorage counter (sender + 1)
+
+  -- Child signatures may use user-defined types declared by the parent.
+  function setInherited (next : InheritedValue) : Unit := do
+    setStorage counter next
+
+  function override value () : Uint256 := do
+    return 2
+
+#check_contract ModifierInheritanceBase
+#check_contract ModifierInheritanceChild
+
+-- An intermediate override may remain virtual for a further derived contract.
+verity_contract VirtualOverrideMiddle is ModifierInheritanceBase where
+  storage
+
+  constructor (initialOwner : Address) ModifierInheritanceBase(initialOwner) := do
+    pure ()
+
+  function virtual override value () : Uint256 := do
+    return 2
+
+verity_contract VirtualOverrideLeaf is VirtualOverrideMiddle where
+  storage
+
+  constructor (initialOwner : Address) VirtualOverrideMiddle(initialOwner) := do
+    pure ()
+
+  function override value () : Uint256 := do
+    return 3
+
+#check_contract VirtualOverrideMiddle
+#check_contract VirtualOverrideLeaf
+
+-- Constructor arguments are bound lexically: the parameter `owner` in the
+-- parent body must not rewrite the storage-field operand with the same name.
+verity_contract ConstructorHygieneBase where
+  storage
+    owner : Address := slot 0
+
+  constructor (owner : Address) := do
+    setStorageAddr owner owner
+
+verity_contract ConstructorHygieneChild is ConstructorHygieneBase where
+  storage
+
+  constructor (admin : Address) ConstructorHygieneBase(admin) := do
+    pure ()
+
+#check_contract ConstructorHygieneChild
+
+-- ABI-dynamic parent arguments must remain direct references to the child
+-- constructor parameter. Materializing `let items := values` loses the
+-- calldata parameter semantics and is rejected by the model translator.
+verity_contract DynamicConstructorBase where
+  storage
+
+  constructor (items : Array Uint256) := do
+    let count := arrayLength items
+    require (count != 0) "items must not be empty"
+
+verity_contract DynamicConstructorChild is DynamicConstructorBase where
+  storage
+
+  constructor (values : Array Uint256) DynamicConstructorBase(values) := do
+    pure ()
+
+#check_contract DynamicConstructorChild
+
+verity_contract NarrowConstructorBase where
+  storage
+
+  constructor (value : Uint8) := do
+    pure ()
+
+-- A literal parent argument is accepted at the declared narrow width and the
+-- inherited body must continue to see that width after constructor flattening.
+verity_contract TypedNarrowConstructorBase where
+  storage
+
+  constructor (value : Uint24) := do
+    let _sum ← narrowAddPanic value value
+    pure ()
+
+verity_contract TypedNarrowConstructorChild is TypedNarrowConstructorBase where
+  storage
+
+  constructor () TypedNarrowConstructorBase(1) := do
+    pure ()
+
+#check_contract TypedNarrowConstructorChild
+
+/--
+error: parent constructor parameter 'value' expects Verity.Macro.ValueType.uint8, got Verity.Macro.ValueType.uint256
+-/
+#guard_msgs in
+verity_contract NarrowConstructorMismatchRejected is NarrowConstructorBase where
+  storage
+
+  constructor (value : Uint256) NarrowConstructorBase(value) := do
+    pure ()
+
+/--
+error: parent constructor parameter 'owner' conflicts with a child constructor parameter; rename the child parameter
+-/
+#guard_msgs in
+verity_contract ConstructorBindingCollisionRejected is ConstructorHygieneBase where
+  storage
+
+  constructor (owner : Address, admin : Address) ConstructorHygieneBase(admin) := do
+    pure ()
+
+verity_contract AncestorConstructorBase where
+  storage
+
+  constructor (owner : Address) := do
+    pure ()
+
+verity_contract AncestorConstructorMiddle is AncestorConstructorBase where
+  storage
+
+  constructor (admin : Address) AncestorConstructorBase(admin) := do
+    pure ()
+
+/--
+error: ancestor constructor binding 'owner' conflicts with a child constructor parameter; rename the child parameter
+-/
+#guard_msgs in
+verity_contract AncestorConstructorCollisionRejected is AncestorConstructorMiddle where
+  storage
+
+  constructor (owner : Address, admin : Address) AncestorConstructorMiddle(admin) := do
+    pure ()
+
+verity_contract ConstructorLocalBase where
+  storage
+
+  constructor () := do
+    let sender ← msgSender
+    require (sender == sender) "sender"
+
+/--
+error: ancestor constructor binding 'sender' conflicts with a child constructor parameter; rename the child parameter
+-/
+#guard_msgs in
+verity_contract ConstructorLocalCollisionRejected is ConstructorLocalBase where
+  storage
+
+  constructor (sender : Address) ConstructorLocalBase() := do
+    pure ()
+
+verity_contract ConstructorTupleAliasBase where
+  storage
+
+  constructor () := do
+    let config_0 ← msgValue
+    require (config_0 == config_0) "config"
+
+/--
+error: ancestor constructor binding 'config_0' conflicts with a child constructor parameter; rename the child parameter
+-/
+#guard_msgs in
+verity_contract ConstructorTupleAliasCollisionRejected is ConstructorTupleAliasBase where
+  storage
+
+  constructor (config : Tuple [Uint256, Uint256]) ConstructorTupleAliasBase() := do
+    pure ()
+
+verity_contract InheritedImmutableBase where
+  storage
+
+  immutables
+    deployer : Address := initialOwner
+
+  constructor (initialOwner : Address) := do
+    pure ()
+
+verity_contract InheritedImmutableChild is InheritedImmutableBase where
+  storage
+
+  constructor (admin : Address) InheritedImmutableBase(admin) := do
+    pure ()
+
+#check_contract InheritedImmutableChild
+
+verity_contract InheritedInterfaceBase where
+  storage
+
+  interfaces
+    interface IOracle where
+      function price() view returns (Uint256)
+    end
+
+verity_contract InheritedInterfaceChild is InheritedInterfaceBase where
+  storage
+
+  function read (_oracle : IOracle) : Unit := do
+    pure ()
+
+#check_contract InheritedInterfaceChild
+
+-- Empty interfaces are valid marker types and must survive inheritance even
+-- though they generate no interface-backed external declarations.
+verity_contract InheritedEmptyInterfaceBase where
+  storage
+
+  interfaces
+    interface IMarker where
+    end
+
+verity_contract InheritedEmptyInterfaceChild is InheritedEmptyInterfaceBase where
+  storage
+
+  function acceptMarker (_marker : IMarker) : Unit := do
+    pure ()
+
+#check_contract InheritedEmptyInterfaceChild
+
+verity_contract InheritedTypeNameBase where
+  types
+    Amount : Uint256
+  storage
+
+namespace QualifiedTypeFixture
+abbrev Amount := Address
+end QualifiedTypeFixture
+
+/--
+error: unsupported type 'QualifiedTypeFixture.Amount'; expected Uint256, Int256, Uint8, Uint16, Address, Bytes32, Bool, String, Bytes, Array <type>, FixedArray <type> <size>, Tuple [...], Unit, a user-defined struct, or a user-defined type from the `types` or `inductive` section
+-/
+#guard_msgs in
+verity_contract QualifiedLocalTypeCaptureRejected where
+  types
+    Amount : Uint256
+  storage
+
+  function inspect (_value : QualifiedTypeFixture.Amount) : Unit := do
+    pure ()
+
+/--
+error: duplicate type name 'Amount'
+-/
+#guard_msgs in
+verity_contract InheritedTypeNameCollisionRejected is InheritedTypeNameBase where
+  types
+    Amount : Address
+  storage
+
+verity_contract NamespacedFieldBase where
+  storage_namespace "base"
+  storage
+    baseValue : Uint256 := slot 0
+
+verity_contract NamespacedFieldChild is NamespacedFieldBase where
+  storage_namespace "child"
+  storage
+    childValue : Uint256 := slot 0
+
+example : NamespacedFieldChild.spec.storageNamespace =
+    NamespacedFieldBase.spec.storageNamespace := by
+  rfl
+
+verity_contract EmptyNamespacedBase where
+  storage_namespace "empty-base"
+  storage
+
+verity_contract NamespacedFirstChild is EmptyNamespacedBase where
+  storage_namespace "first-child"
+  storage
+    childValue : Uint256 := slot 0
+
+example : NamespacedFirstChild.spec.storageNamespace = some NamespacedFirstChild.storageNamespace := by
+  rfl
+
+-- A child with no constructor has an implicit nonpayable constructor even
+-- when it runs a zero-argument payable parent initializer.
+verity_contract PayableConstructorBase where
+  storage
+
+  constructor () payable := do
+    pure ()
+
+verity_contract ImplicitConstructorChild is PayableConstructorBase where
+  storage
+
+example : ImplicitConstructorChild.spec.constructor.map (·.isPayable) = some false := by
+  rfl
+
+-- Overrides may preserve or narrow payability, but may not widen it.
+verity_contract NonpayableVirtualBase where
+  storage
+
+  function virtual value () : Uint256 := do
+    return 1
+
+/--
+error: function 'value' cannot widen a nonpayable inherited function to payable
+-/
+#guard_msgs in
+verity_contract PayableOverrideRejected is NonpayableVirtualBase where
+  storage
+
+  function payable override value () : Uint256 := do
+    return 2
+
+verity_contract ViewVirtualBase where
+  storage
+
+  function view virtual value () : Uint256 := do
+    return 1
+
+/--
+error: function 'value' cannot weaken an inherited view function to state-mutating
+-/
+#guard_msgs in
+verity_contract ViewOverrideRejected is ViewVirtualBase where
+  storage
+
+  function override value () : Uint256 := do
+    return 2
+
+verity_contract PureVirtualBase where
+  storage
+
+  function pure virtual value () : Uint256 := do
+    return 1
+
+/--
+error: function 'value' cannot weaken an inherited pure function
+-/
+#guard_msgs in
+verity_contract PureOverrideRejected is PureVirtualBase where
+  storage
+
+  function view override value () : Uint256 := do
+    return 2
+
+/--
+error: function 'value' must preserve inherited internal/external visibility
+-/
+#guard_msgs in
+verity_contract VisibilityOverrideRejected is NonpayableVirtualBase where
+  storage
+
+  function internal override value () : Uint256 := do
+    return 2
+
+/--
+error: function 'value' must preserve the inherited return type
+-/
+#guard_msgs in
+verity_contract ReturnTypeOverrideRejected is NonpayableVirtualBase where
+  storage
+
+  function override value () : Address := do
+    return zeroAddress
+
+verity_contract ModifierParameterCollisionBase where
+  storage
+
+  modifier captureSender := do
+    let sender ← msgSender
+    require (sender == sender) "sender"
+
+/--
+error: modifier 'captureSender' local 'sender' conflicts with a function parameter; rename one of them
+-/
+#guard_msgs in
+verity_contract ModifierParameterCollisionRejected is ModifierParameterCollisionBase where
+  storage
+
+  function check (sender : Address) with captureSender : Unit := do
+    pure ()
+
+verity_contract ModifierTupleAliasBase where
+  storage
+
+  modifier captureConfig := do
+    let config_0 ← msgValue
+    require (config_0 == config_0) "config"
+
+/--
+error: modifier 'captureConfig' local 'config_0' conflicts with a function parameter; rename one of them
+-/
+#guard_msgs in
+verity_contract ModifierTupleAliasCollisionRejected is ModifierTupleAliasBase where
+  storage
+
+  function check (config : Tuple [Uint256, Uint256]) with captureConfig : Unit := do
+    pure ()
+
+verity_contract ModifierLoopCollisionBase where
+  storage
+
+  modifier loopSender := do
+    forEach "sender" 1 (do
+      require (sender == 0) "sender")
+
+/--
+error: modifier 'loopSender' local 'sender' conflicts with a function parameter; rename one of them
+-/
+#guard_msgs in
+verity_contract ModifierLoopCollisionRejected is ModifierLoopCollisionBase where
+  storage
+
+  function check (sender : Uint256) with loopSender : Unit := do
+    pure ()
+
+-- Overloads introduced on opposite sides of the inheritance boundary receive
+-- distinct generated Lean identifiers after flattening.
+verity_contract InheritedOverloadBase where
+  storage
+
+  function inspect (value : Uint256) : Uint256 := do
+    return value
+
+verity_contract InheritedOverloadChild is InheritedOverloadBase where
+  storage
+
+  function inspect (value : Address) : Address := do
+    return value
+
+#check_contract InheritedOverloadChild
+
+verity_contract InheritedRoleBase where
+  storage
+    owner : Address := slot 0
+  roles
+    operator := owner
+
+verity_contract InheritedRoleChild is InheritedRoleBase where
+  storage
+  roles
+    auditor := owner
+
+  function audit () requires(auditor) : Unit := do
+    pure ()
+
+#check_contract InheritedRoleChild
+
+/--
+error: modifier 'earlyExit' contains a terminating return; modifiers must only contain non-terminating precondition statements
+-/
+#guard_msgs in
+verity_contract TerminatingModifierRejected where
+  storage
+
+  modifier earlyExit := do
+    returnValues [1, 2]
+
+  function pair () with earlyExit : Tuple [Uint256, Uint256] := do
+    return (3, 4)
+
+/--
+error: cross-namespace inheritance is not supported because inherited bodies must retain the parent's lexical namespace; declare the child in the parent's namespace
+-/
+#guard_msgs in
+verity_contract CrossNamespaceInheritanceRejected is Contracts.Counter where
+  storage
+
+/--
+error: role 'operator' duplicates an inherited role
+-/
+#guard_msgs in
+verity_contract InheritedRoleCollisionRejected is InheritedRoleBase where
+  storage
+    admin : Address := slot 0
+  roles
+    operator := admin
+
 end Contracts.Smoke
diff --git a/Contracts/Smoke/InheritanceImportBase.lean b/Contracts/Smoke/InheritanceImportBase.lean
new file mode 100644
index 000000000..39273eac3
--- /dev/null
+++ b/Contracts/Smoke/InheritanceImportBase.lean
@@ -0,0 +1,14 @@
+import Contracts.Common
+
+namespace Contracts.Smoke.InheritanceImport
+
+open Contracts
+open Verity hiding pure bind
+
+verity_contract ImportedInheritanceBase where
+  types
+    ImportedAmount : Uint256
+  storage
+    inheritedValue : Uint256 := slot 0
+
+end Contracts.Smoke.InheritanceImport
diff --git a/Contracts/Smoke/InheritanceImportChild.lean b/Contracts/Smoke/InheritanceImportChild.lean
new file mode 100644
index 000000000..99de915fc
--- /dev/null
+++ b/Contracts/Smoke/InheritanceImportChild.lean
@@ -0,0 +1,20 @@
+import Contracts.Smoke.InheritanceImportBase
+import Compiler.CheckContract
+
+namespace Contracts.Smoke.InheritanceImport
+
+open Contracts
+open Verity hiding pure bind
+
+-- The parent is loaded exclusively from InheritanceImportBase.olean. This
+-- fails if inheritance metadata is held in process-local state.
+verity_contract ImportedInheritanceChild is ImportedInheritanceBase where
+  storage
+    childValue : Uint256 := slot 1
+
+  function setImported (next : ImportedAmount) : Unit := do
+    setStorage inheritedValue next
+
+#check_contract ImportedInheritanceChild
+
+end Contracts.Smoke.InheritanceImport
diff --git a/Verity/Macro/Elaborate.lean b/Verity/Macro/Elaborate.lean
index f7e02efaf..11e27fafd 100644
--- a/Verity/Macro/Elaborate.lean
+++ b/Verity/Macro/Elaborate.lean
@@ -90,6 +90,7 @@ def elabVerityContract : CommandElab := fun stx => do
   validateExternalDeclsPublic externalDecls
   validateFunctionDeclsPublic fields errorDecls constDecls immutableDecls externalDecls ctor modifiers functions
 
+  let declarationNs ← getCurrNamespace
   elabCommand (← `(namespace $contractName))
   try
     for constant in constDecls do
@@ -149,6 +150,8 @@ def elabVerityContract : CommandElab := fun stx => do
       if fn.isPure then
         elabCommand (← mkPureTheoremCommand fn)
 
+    registerContractSyntax (declarationNs ++ contractName.getId) parsed
+
     -- Emit per-function _no_calls theorems for no_external_calls functions (#1729, Axis 3 Step 1c).
     for fn in functions do
       if fn.noExternalCalls then
diff --git a/Verity/Macro/Interfaces.lean b/Verity/Macro/Interfaces.lean
index be1205f32..5237a48c8 100644
--- a/Verity/Macro/Interfaces.lean
+++ b/Verity/Macro/Interfaces.lean
@@ -116,8 +116,6 @@ def parseInterface
   match stx with
   | `(verityInterface| interface $name:ident where $[$fns:verityInterfaceFunction]* end) =>
       let parsedFns ← fns.mapM (parseInterfaceFunction newtypes structDecls adtDecls)
-      if parsedFns.isEmpty then
-        throwErrorAt name s!"interface '{toString name.getId}' must declare at least one function"
       pure { ident := name, name := toString name.getId, functions := parsedFns }
   | _ => throwErrorAt stx "invalid interface declaration"
 
diff --git a/Verity/Macro/Syntax.lean b/Verity/Macro/Syntax.lean
index 5937fdfe9..94a1fa4ca 100644
--- a/Verity/Macro/Syntax.lean
+++ b/Verity/Macro/Syntax.lean
@@ -34,6 +34,7 @@ declare_syntax_cat verityNamespaceSpec
 declare_syntax_cat veritySpecialEntrypoint
 declare_syntax_cat verityModifier
 declare_syntax_cat verityModifierUse
+declare_syntax_cat verityDispatch
 declare_syntax_cat verityRoleDecl
 declare_syntax_cat verityFunction
 declare_syntax_cat verityIntrinsicClause
@@ -96,6 +97,8 @@ syntax "allow_post_interaction_writes" : verityMutability
 syntax "nonreentrant(" ident ")" : verityMutability
 syntax "cei_safe" : verityMutability
 syntax "reentrancy_trusted" : verityMutability
+syntax "virtual" : verityDispatch
+syntax "override" : verityDispatch
 syntax "modifies(" sepBy1(ident, ",") ")" : verityModifies
 syntax "requires(" ident ")" : verityRequiresRole
 syntax ident " : " term:max : verityNewtype
@@ -151,14 +154,14 @@ syntax "requireError " term:max ppSpace ident "(" sepBy(term, ",") ")" : doElem
 syntax (name := requireSomeUintErrorTerm) "requireSomeUintError " term:max ppSpace ident "(" sepBy(term, ",") ")" : term
 syntax "ecmBind " term:max ppSpace term:max ppSpace term:max : doElem
 syntax (priority := high) "unsafe " str " do " doSeq : doElem
-syntax "constructor " "(" sepBy(verityParam, ",") ")" (ppSpace verityLocalObligations)? " := " term : verityConstructor
-syntax "constructor " "(" sepBy(verityParam, ",") ")" " payable" (ppSpace verityLocalObligations)? " := " term : verityConstructor
+syntax "constructor " "(" sepBy(verityParam, ",") ")" (ppSpace ident "(" sepBy(term, ",") ")")? (ppSpace verityLocalObligations)? " := " term : verityConstructor
+syntax "constructor " "(" sepBy(verityParam, ",") ")" " payable" (ppSpace ident "(" sepBy(term, ",") ")")? (ppSpace verityLocalObligations)? " := " term : verityConstructor
 syntax "receive" (ppSpace verityLocalObligations)? " := " term : veritySpecialEntrypoint
 syntax "fallback" (ppSpace verityLocalObligations)? " := " term : veritySpecialEntrypoint
 syntax "modifier " ident " := " term : verityModifier
 syntax "with " sepBy1(ident, ",") : verityModifierUse
 syntax ident " := " ident : verityRoleDecl
-syntax "function " verityMutability* (pureMutabilityMarker)? verityMutability* ident " (" sepBy(verityParam, ",") ")" (ppSpace verityInitGuard)? (ppSpace verityModifierUse)? (ppSpace verityRequiresRole)? (ppSpace verityModifies)? (ppSpace verityLocalObligations)? " : " term " := " term : verityFunction
+syntax "function " verityMutability* (pureMutabilityMarker)? verityMutability* verityDispatch* ident " (" sepBy(verityParam, ",") ")" (ppSpace verityInitGuard)? (ppSpace verityModifierUse)? (ppSpace verityRequiresRole)? (ppSpace verityModifies)? (ppSpace verityLocalObligations)? " : " term " := " term : verityFunction
 
 -- verity_intrinsic syntax (minimal one-argument shape for consumer-owned intrinsics)
 -- `pure` is parsed as an identifier here to avoid reserving it as a global
@@ -190,7 +193,7 @@ syntax (name := verityIntrinsicCmd)
   ident " := " term ";" ident "[" sepBy(verityIntrinsicObligation, ",") "]" : command
 
 syntax (name := verityContractCmd)
-  "verity_contract " ident " where "
+  "verity_contract " ident (" is " ident)? " where "
   ("types " verityNewtype+)?
   ("inductive " verityAdtDecl+)?
   (verityNamespaceSpec)?
diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index 343e75091..1110b3866 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -2776,6 +2776,7 @@ private partial def offsetStorageAccessorTree (offset : Nat) : StorageAccessorTr
 
 structure ParsedContractSyntax where
   contractName : Ident
+  parentName? : Option Ident := none
   newtypeDecls : Array NewtypeDecl
   structDecls : Array StructDecl
   adtDecls : Array AdtDecl
@@ -2786,12 +2787,345 @@ structure ParsedContractSyntax where
   eventDecls : Array EventDecl
   constDecls : Array ConstantDecl
   immutableDecls : Array ImmutableDecl
+  interfaceDecls : Array InterfaceDecl
   externalDecls : Array ExternalDecl
   ctor : Option ConstructorDecl
   modifiers : Array ModifierDecl
   functions : Array FunctionDecl
   storageNamespace : Option Nat
 
+abbrev ContractSyntaxRegistry := List (Name × ParsedContractSyntax)
+
+private def addContractSyntaxEntry
+    (state : ContractSyntaxRegistry) (entry : Name × ParsedContractSyntax) : ContractSyntaxRegistry :=
+  entry :: state.filter (fun prior => prior.1 != entry.1)
+
+initialize contractSyntaxExt : SimplePersistentEnvExtension
+    (Name × ParsedContractSyntax) ContractSyntaxRegistry ←
+  registerSimplePersistentEnvExtension {
+    addEntryFn := addContractSyntaxEntry
+    addImportedFn := fun entries =>
+      mkStateFromImportedEntries addContractSyntaxEntry [] entries
+  }
+
+def registerContractSyntax (name : Name) (parsed : ParsedContractSyntax) : CommandElabM Unit :=
+  modifyEnv fun env => contractSyntaxExt.addEntry env (name, parsed)
+
+private def lookupContractSyntax (name : Name) : CommandElabM (Option ParsedContractSyntax) := do
+  pure (contractSyntaxExt.getState (← getEnv)
+    |>.find? (fun entry => entry.1 == name) |>.map (·.2))
+
+private def doElems (body : Term) : CommandElabM (Array (TSyntax `doElem)) := do
+  match body with
+  | `(term| do $[$elems:doElem]*) => pure elems
+  | _ => throwErrorAt body "constructor body must be a do block"
+
+private partial def localBinderNames (stx : Syntax) : CommandElabM (Array String) := do
+  let here ←
+    if stx.getKind == `Lean.Parser.Term.doLet then
+      let binder := stx[3][0][0]
+      match binder with
+      | .ident _ raw _ _ => pure #[raw.toString]
+      | _ => pure <| (tupleBinderNames? binder).getD #[] |>.filterMap id
+    else if stx.getKind == `Lean.Parser.Term.doLetArrow then
+      let binder := stx[3][0]
+      match binder with
+      | .ident _ raw _ _ => pure #[raw.toString]
+      | _ => pure <| (tupleBinderNames? binder).getD #[] |>.filterMap id
+    else
+      match (⟨stx⟩ : TSyntax `doElem) with
+      | `(doElem| forEach $name:term $_count:term $_body:term) =>
+          pure #[← expectStringOrIdent name]
+      | `(doElem| forEachSetBit $name:term $_bitmap:term $_body:term) =>
+          pure #[← expectStringOrIdent name]
+      | `(doElem| ecmBind $names:term $_module:term $_args:term) =>
+          expectStringList names
+      | _ => pure #[]
+  let nested ← stx.getArgs.mapM localBinderNames
+  pure (nested.foldl (· ++ ·) here)
+
+private partial def substitutePureInitializerParamSyntax
+    (bindings : Array (String × Syntax)) (node : Syntax) : Syntax :=
+    match node with
+    | .ident _ _ name _ =>
+        bindings.find? (fun binding => binding.1 == name.toString)
+          |>.map (·.2) |>.getD node
+    | _ =>
+        let args := node.getArgs
+        if node.getKind == `Lean.Parser.Term.app && !args.isEmpty then
+          -- The application head names a helper/constant, not a constructor
+          -- parameter reference.  Rebind only its argument expressions.
+          node.setArgs (args.mapIdx fun idx arg =>
+            if idx == 0 then arg else substitutePureInitializerParamSyntax bindings arg)
+        else
+          node.setArgs (args.map (substitutePureInitializerParamSyntax bindings))
+
+private def substitutePureInitializerParams
+    (bindings : Array (String × Syntax)) (body : Term) : Term :=
+  ⟨substitutePureInitializerParamSyntax bindings body.raw⟩
+
+/-- Rebind direct dynamic parent-constructor parameters to the child ABI
+    parameter that supplies them. Dynamic values cannot be materialized as
+    model locals: their offsets remain meaningful only as parameter
+    references. Storage helper field operands are declarations, rather than
+    value references, so they must remain untouched when a field and parent
+    parameter intentionally share a name. -/
+private partial def substituteDynamicParentParamSyntax
+    (bindings : Array (String × Syntax)) (node : Syntax) : Syntax :=
+  match node with
+  | .ident _ _ name _ =>
+      bindings.find? (fun binding => declaredNameMatches name.toString binding.1)
+        |>.map (·.2) |>.getD node
+  | _ =>
+      let args := node.getArgs
+      if node.getKind == `Lean.Parser.Term.app && !args.isEmpty then
+        let headName? := match args[0]? with
+          | some (.ident _ _ name _) => some name.toString
+          | _ => none
+        let fieldOperandIsDeclaration := headName?.any fun head =>
+          #["getStorage", "getStorageAddr", "getStorageArrayLength",
+            "getStorageArrayElement", "setStorage", "setStorageAddr",
+            "setStorageArrayElement", "getMapping", "getMappingAddr",
+            "getMappingUint", "getMappingUintAddr", "getMappingWord",
+            "getMapping2", "getMappingN", "setMapping", "setMappingAddr",
+            "setMappingUint", "setMappingUintAddr", "setMappingWord",
+            "setMapping2", "setMappingN", "tload", "tstore"].contains head
+        node.setArgs (args.mapIdx fun idx arg =>
+          if idx == 0 || (idx == 1 && fieldOperandIsDeclaration) then arg
+          else substituteDynamicParentParamSyntax bindings arg)
+      else
+        node.setArgs (args.map (substituteDynamicParentParamSyntax bindings))
+
+private def substituteDynamicParentParams
+    (bindings : Array (String × Syntax)) (body : Term) : Term :=
+  ⟨substituteDynamicParentParamSyntax bindings body.raw⟩
+
+/-- Whether a parameter reserves `name` in the lowered function namespace.
+Tuple parameters synthesize aliases such as `config_0` for their components. -/
+private def paramReservesName (param : ParamDecl) (name : String) : Bool :=
+  param.name == name || match param.ty with
+    | .tuple elemTys => (elemTys.toArray.zipIdx).any fun (_, idx) =>
+        s!"{param.name}_{idx}" == name
+    | _ => false
+
+private partial def normalizeParentConstructorArg
+    (paramTy : ValueType) (arg : Term) : CommandElabM Term := do
+  match paramTy with
+  | .uintN bits => `(narrowUInt $(natTerm bits) $arg)
+  | .intN bits => `(narrowInt $(natTerm bits) $arg)
+  | .bytesN bytes => `(narrowBytes $(natTerm bytes) $arg)
+  | .int256 => `(toInt256 $arg)
+  | .newtype _ baseType => normalizeParentConstructorArg baseType arg
+  | _ => pure arg
+
+private def composeConstructors
+    (parentName : Ident) (parentContract childContract : ParsedContractSyntax) :
+    CommandElabM (Option ConstructorDecl) := do
+  match parentContract.ctor, childContract.ctor with
+  | none, none => pure none
+  | none, some child =>
+      if child.parentName?.isSome then
+        throwErrorAt child.parentName?.get! "parent constructor call supplied, but the parent has no constructor"
+      pure (some child)
+  | some parent, none =>
+      if !parent.params.isEmpty then
+        throwErrorAt parentName s!"parent constructor '{toString parentName.getId}' expects {parent.params.size} argument(s); add an explicit parent constructor call"
+      -- An omitted child constructor is an implicit nonpayable constructor.
+      -- Running a payable parent initializer must not widen that external ABI.
+      pure (some { parent with isPayable := false, parentName? := none, parentArgs := #[] })
+  | some parent, some child =>
+      let calledParent ← match child.parentName? with
+        | some called => pure called
+        | none => throwErrorAt parentName s!"constructor must call parent constructor '{toString parentName.getId}'"
+      if calledParent.getId != parentName.getId then
+        throwErrorAt calledParent s!"constructor calls '{calledParent.getId}', expected direct parent '{parentName.getId}'"
+      if child.parentArgs.size != parent.params.size then
+        throwErrorAt calledParent s!"parent constructor '{parentName.getId}' expects {parent.params.size} argument(s), got {child.parentArgs.size}"
+      for (param, arg) in parent.params.zip child.parentArgs do
+        let argTy ← inferPureExprType
+          (parentContract.fields ++ childContract.fields)
+          (parentContract.constDecls ++ childContract.constDecls)
+          (parentContract.immutableDecls ++ childContract.immutableDecls)
+          (parentContract.externalDecls ++ childContract.externalDecls)
+          child.params #[] arg
+        unless argumentTypeMatchesParam arg argTy param.ty do
+          throwErrorAt arg
+            s!"parent constructor parameter '{param.name}' expects {renderValueType param.ty}, got {renderValueType argTy}"
+      let inheritedBinderNames := parent.boundParentParamNames ++ (← localBinderNames parent.body.raw)
+      if let some captured := inheritedBinderNames.find? (fun name =>
+          child.params.any (fun childParam => paramReservesName childParam name)) then
+        throwErrorAt calledParent s!"ancestor constructor binding '{captured}' conflicts with a child constructor parameter; rename the child parameter"
+      -- Bind parent arguments in a nested lexical scope instead of rewriting
+      -- identifier syntax.  The latter is not hygienic: a parameter named
+      -- `owner` must not rewrite the storage-field operand in
+      -- `setStorageAddr owner owner` (nor a nested local binder).
+      let mut parentBindings : Array (TSyntax `doElem) := #[]
+      let mut dynamicParamBindings : Array (String × Syntax) := #[]
+      let mut boundParentParamNames := inheritedBinderNames
+      for (param, arg) in parent.params.zip child.parentArgs do
+        -- Reuse an identically named child parameter directly.  Introducing
+        -- a redundant `let x := x` would be rejected as parameter shadowing.
+        let directChildParam? := match stripParens arg with
+          | `(term| $name:ident) =>
+              child.params.find? (fun (childParam : ParamDecl) =>
+                declaredNameMatches (toString name.getId) childParam.name)
+          | _ => child.params.find? (fun childParam =>
+              (stripParens arg).raw.reprint.getD "" == childParam.name)
+        let isIdentityArg := directChildParam?.any (fun childParam => childParam.name == param.name)
+        if !isIdentityArg then
+          if child.params.any (fun childParam => paramReservesName childParam param.name) then
+            throwErrorAt arg s!"parent constructor parameter '{param.name}' conflicts with a child constructor parameter; rename the child parameter"
+          if valueTypeUsesDynamicData param.ty && directChildParam?.isSome then
+            -- Keep ABI-dynamic data attached to its actual child parameter;
+            -- a `let parent := child` would turn it into an unsupported (and
+            -- semantically incorrect) local value.
+            dynamicParamBindings := dynamicParamBindings.push (param.name, arg.raw)
+          else
+            -- Parent arguments have already been checked against `param.ty`,
+            -- but Lean and the model typer otherwise infer literals at their
+            -- default type. Normalize width-sensitive values before binding so
+            -- inherited bodies retain the parent's declared semantics.
+            let normalizedArg ← normalizeParentConstructorArg param.ty arg
+            let binding ← `(doElem| let $param.ident := $normalizedArg)
+            parentBindings := parentBindings.push binding
+            boundParentParamNames := boundParentParamNames.push param.name
+      let parentBody := substituteDynamicParentParams dynamicParamBindings parent.body
+      let parentElems ← doElems parentBody
+      let scopedParent ← `(doElem| if true then
+        $[$parentBindings:doElem]*
+        $[$parentElems:doElem]*
+        else
+          pure ())
+      let childElems ← doElems child.body
+      let combinedBody ← `(do $scopedParent:doElem $[$childElems:doElem]*)
+      pure (some {
+        child with
+        -- The child constructor is the externally visible constructor.  A
+        -- payable parent initializer must not widen its mutability.
+        isPayable := child.isPayable
+        localObligations := parent.localObligations ++ child.localObligations
+        boundParentParamNames := boundParentParamNames
+        parentName? := none
+        parentArgs := #[]
+        body := combinedBody
+      })
+
+private def flattenSingleInheritance
+    (parentName : Ident) (parent child : ParsedContractSyntax) : CommandElabM ParsedContractSyntax := do
+  let duplicateFields := child.fields.filter fun field => parent.fields.any (fun inherited => inherited.name == field.name)
+  if let some field := duplicateFields[0]? then
+    throwErrorAt field.ident s!"storage field '{field.name}' duplicates an inherited field"
+  let duplicateModifiers := child.modifiers.filter fun modDecl =>
+    parent.modifiers.any (fun inherited => inherited.name == modDecl.name)
+  if let some modDecl := duplicateModifiers[0]? then
+    throwErrorAt modDecl.ident s!"modifier '{modDecl.name}' duplicates an inherited modifier"
+  let duplicateRoles := child.roleDecls.filter fun roleDecl =>
+    parent.roleDecls.any (fun inherited => inherited.name == roleDecl.name)
+  if let some roleDecl := duplicateRoles[0]? then
+    throwErrorAt roleDecl.ident s!"role '{roleDecl.name}' duplicates an inherited role"
+  let mut functions := parent.functions
+  for fn in child.functions do
+    let inherited? := functions.find? (fun inherited => functionSignatureKey inherited == functionSignatureKey fn)
+    match fn.isOverride, inherited? with
+    | true, none =>
+        throwErrorAt fn.ident s!"function '{fn.name}' is marked override, but no inherited function has the same signature"
+    | true, some inherited =>
+        if !inherited.isVirtual then
+          throwErrorAt fn.ident s!"function '{fn.name}' overrides a non-virtual inherited function"
+        if !inherited.isPayable && fn.isPayable then
+          throwErrorAt fn.ident s!"function '{fn.name}' cannot widen a nonpayable inherited function to payable"
+        if inherited.isPayable && !fn.isPayable then
+          throwErrorAt fn.ident s!"function '{fn.name}' cannot change an inherited payable function to nonpayable"
+        if inherited.isPure && !fn.isPure then
+          throwErrorAt fn.ident s!"function '{fn.name}' cannot weaken an inherited pure function"
+        if inherited.isView && !fn.isView && !fn.isPure then
+          throwErrorAt fn.ident s!"function '{fn.name}' cannot weaken an inherited view function to state-mutating"
+        if inherited.isInternal != fn.isInternal then
+          throwErrorAt fn.ident s!"function '{fn.name}' must preserve inherited internal/external visibility"
+        if inherited.returnTy != fn.returnTy then
+          throwErrorAt fn.ident s!"function '{fn.name}' must preserve the inherited return type"
+        functions := functions.map fun candidate =>
+          if functionSignatureKey candidate == functionSignatureKey fn then
+            { fn with isOverride := false }
+          else
+            candidate
+    | false, some _ =>
+        throwErrorAt fn.ident s!"function '{fn.name}' has the same signature as an inherited function; add override (the inherited function must be virtual)"
+    | false, none =>
+        functions := functions.push fn
+  let inheritedImmutables :=
+    match parent.ctor, child.ctor with
+    | some parentCtor, some childCtor =>
+        let bindings := parentCtor.params.zip childCtor.parentArgs |>.map fun (param, arg) =>
+          (param.name, arg.raw)
+        parent.immutableDecls.map fun imm =>
+          { imm with body := substitutePureInitializerParams bindings imm.body }
+    | _, _ => parent.immutableDecls
+  let ctor ← composeConstructors parentName parent child
+  pure {
+    child with
+    parentName? := some parentName
+    newtypeDecls := parent.newtypeDecls ++ child.newtypeDecls
+    structDecls := parent.structDecls ++ child.structDecls
+    adtDecls := parent.adtDecls ++ child.adtDecls
+    fields := parent.fields ++ child.fields
+    roleDecls := parent.roleDecls ++ child.roleDecls
+    storageStructAccessors := parent.storageStructAccessors ++ child.storageStructAccessors
+    errorDecls := parent.errorDecls ++ child.errorDecls
+    eventDecls := parent.eventDecls ++ child.eventDecls
+    constDecls := parent.constDecls ++ child.constDecls
+    immutableDecls := inheritedImmutables ++ child.immutableDecls
+    interfaceDecls := parent.interfaceDecls ++ child.interfaceDecls
+    externalDecls := parent.externalDecls ++ child.externalDecls
+    ctor := ctor
+    modifiers := parent.modifiers ++ child.modifiers
+    -- Parent and child overload identifiers were assigned independently.
+    -- Reassign them across the flattened set so cross-boundary overloads are
+    -- collision-free as well.
+    functions := assignOverloadInternalIdents functions
+    -- Flattening emits parent fields first, so report the namespace belonging
+    -- to whichever contract contributes the first field in the final layout.
+    storageNamespace :=
+      if !parent.fields.isEmpty then parent.storageNamespace
+      else if !child.fields.isEmpty then child.storageNamespace
+      else child.storageNamespace.orElse (fun _ => parent.storageNamespace)
+  }
+
+private def inlineModifierPrefixes
+    (modifiers : Array ModifierDecl) (functions : Array FunctionDecl) : CommandElabM (Array FunctionDecl) :=
+  functions.mapM fun fn => do
+    if fn.modifiers.isEmpty then
+      pure fn
+    else
+      let mut prelude : Array (TSyntax `doElem) := #[]
+      for modifierIdent in fn.modifiers do
+        let modifierName := toString modifierIdent.getId
+        let some modDecl := modifiers.find? (fun candidate => candidate.name == modifierName)
+          | throwErrorAt modifierIdent s!"function '{fn.name}' references unknown modifier '{modifierName}'"
+        let modifierElems ← doElems modDecl.body
+        let modifierLocals ← localBinderNames modDecl.body.raw
+        if let some captured := modifierLocals.find? (fun name =>
+            fn.params.any (fun param => paramReservesName param name)) then
+          throwErrorAt modifierIdent s!"modifier '{modifierName}' local '{captured}' conflicts with a function parameter; rename one of them"
+        -- A modifier's locals have their own lexical scope in Solidity.  An
+        -- always-taken branch preserves that scope in the flattened EDSL IR,
+        -- so modifier-local names may be reused by later modifiers or by the
+        -- function body.
+        let scopedElem ← `(doElem| if true then $[$modifierElems:doElem]* else
+          require false "unreachable modifier scope")
+        prelude := prelude.push scopedElem
+      let bodyElems ← doElems fn.body
+      let inlined ← `(do $[$prelude:doElem]* $[$bodyElems:doElem]*)
+      pure { fn with modifiers := #[], body := inlined }
+
+private partial def modifierSyntaxTerminates (stx : Syntax) : Bool :=
+  stx.getKind == ``Lean.Parser.Term.doReturn ||
+    (match stx with
+    | .ident _ _ name _ =>
+        #["returnValues", "returnArray", "returnBytes", "returnStorageWords", "returnCodeData"]
+          |>.contains name.toString
+    | _ => stx.getArgs.any modifierSyntaxTerminates)
+
 private def roleKindOfStorageField? (field : StorageFieldDecl) : Option RoleKind :=
   match field.ty with
   | .scalar .address | .scalar (.newtype _ .address) => some .scalarAddress
@@ -2825,18 +3159,42 @@ def parseContractSyntax
     (stx : Syntax)
     : CommandElabM ParsedContractSyntax := do
   match stx with
-  | `(command| verity_contract $contractName:ident where $[types $[$newtypeDecls:verityNewtype]*]? $[inductive $[$adtDecls:verityAdtDecl]*]? $[$nsSpec:verityNamespaceSpec]? storage $[$storageItems:verityStorageItem]* $[roles $[$roleDecls:verityRoleDecl]*]? $[$structDecls:verityStructDecl]* $[errors $[$errorDecls:verityError]*]? $[event_defs $[$eventDecls:verityEvent]*]? $[constants $[$constantDecls:verityConstant]*]? $[immutables $[$immutableDecls:verityImmutable]*]? $[interfaces $[$interfaceDecls:verityInterface]*]? $[linked_externals $[$externalDecls:verityExternal]*]? $[$ctor:verityConstructor]? $[$entrypoints:veritySpecialEntrypoint]* $[$modifierDecls:verityModifier]* $[$functions:verityFunction]*) =>
+  | `(command| verity_contract $contractName:ident $[is $parentName:ident]? where $[types $[$newtypeDecls:verityNewtype]*]? $[inductive $[$adtDecls:verityAdtDecl]*]? $[$nsSpec:verityNamespaceSpec]? storage $[$storageItems:verityStorageItem]* $[roles $[$roleDecls:verityRoleDecl]*]? $[$structDecls:verityStructDecl]* $[errors $[$errorDecls:verityError]*]? $[event_defs $[$eventDecls:verityEvent]*]? $[constants $[$constantDecls:verityConstant]*]? $[immutables $[$immutableDecls:verityImmutable]*]? $[interfaces $[$interfaceDecls:verityInterface]*]? $[linked_externals $[$externalDecls:verityExternal]*]? $[$ctor:verityConstructor]? $[$entrypoints:veritySpecialEntrypoint]* $[$modifierDecls:verityModifier]* $[$functions:verityFunction]*) =>
+      -- Resolve inheritance before parsing the child: inherited user-defined
+      -- types are valid in every child declaration and function signature.
+      let currentNs ← getCurrNamespace
+      let mut parent? : Option ParsedContractSyntax := none
+      if let some parentIdent := parentName then
+        let candidates := [currentNs ++ parentIdent.getId, parentIdent.getId]
+        let mut resolvedParentName? : Option Name := none
+        for candidate in candidates do
+          if parent?.isNone then
+            parent? ← lookupContractSyntax candidate
+            if parent?.isSome then
+              resolvedParentName? := some candidate
+        if parent?.isNone then
+          throwErrorAt parentIdent s!"unknown parent contract '{parentIdent.getId}'; import or declare the parent before the child"
+        if let some resolvedParentName := resolvedParentName? then
+          if resolvedParentName.getPrefix != currentNs then
+            throwErrorAt parentIdent
+              "cross-namespace inheritance is not supported because inherited bodies must retain the parent's lexical namespace; declare the child in the parent's namespace"
       -- Parse newtypes first — they are needed by all downstream type resolution
       let parsedNewtypes ←
         match newtypeDecls with
         | some decls => decls.mapM parseNewtype
         | none => pure #[]
+      let typeNewtypes := parent?.map (fun p => p.newtypeDecls ++ parsedNewtypes) |>.getD parsedNewtypes
       -- Validate: no duplicate type names
-      let mut seenNames : Array String := #[]
+      let inheritedTypeNames := parent?.map (fun p =>
+        (p.newtypeDecls.map (fun decl => localDeclName decl.name)) ++
+        (p.structDecls.map (fun decl => localDeclName decl.name)) ++
+        (p.adtDecls.map (fun decl => localDeclName decl.name))) |>.getD #[]
+      let mut seenNames : Array String := inheritedTypeNames
       for nt in parsedNewtypes do
-        if seenNames.contains nt.name then
+        let ntLocalName := localDeclName nt.name
+        if seenNames.contains ntLocalName then
           throwErrorAt nt.ident s!"duplicate type name '{nt.name}'"
-        seenNames := seenNames.push nt.name
+        seenNames := seenNames.push ntLocalName
       -- Validate: type names don't shadow built-in types
       let builtinTypeNames := #["Uint256", "Int256", "Uint8", "Address", "Bytes32", "Bool", "String", "Bytes", "Unit", "Array", "Tuple"]
       for nt in parsedNewtypes do
@@ -2844,23 +3202,28 @@ def parseContractSyntax
           throwErrorAt nt.ident s!"type name '{nt.name}' shadows a built-in type"
       let mut parsedStructs : Array StructDecl := #[]
       for structStx in structDecls do
-        let parsedStruct ← parseStructDecl parsedNewtypes parsedStructs structStx
-        if seenNames.contains parsedStruct.name then
+        let inheritedStructs := parent?.map (fun p => p.structDecls) |>.getD #[]
+        let parsedStruct ← parseStructDecl typeNewtypes (inheritedStructs ++ parsedStructs) structStx
+        let structLocalName := localDeclName parsedStruct.name
+        if seenNames.contains structLocalName then
           throwErrorAt parsedStruct.ident s!"duplicate type name '{parsedStruct.name}'"
         if builtinTypeNames.contains parsedStruct.name then
           throwErrorAt parsedStruct.ident s!"struct name '{parsedStruct.name}' shadows a built-in type"
-        seenNames := seenNames.push parsedStruct.name
+        seenNames := seenNames.push structLocalName
         parsedStructs := parsedStructs.push parsedStruct
       -- Parse ADT declarations (#1727, Axis 1 Step 5a)
       let parsedAdts ←
         match adtDecls with
-        | some decls => decls.mapM (parseAdtDecl parsedNewtypes)
+        | some decls => decls.mapM (parseAdtDecl typeNewtypes)
         | none => pure #[]
+      let typeStructs := parent?.map (fun p => p.structDecls ++ parsedStructs) |>.getD parsedStructs
+      let typeAdts := parent?.map (fun p => p.adtDecls ++ parsedAdts) |>.getD parsedAdts
       -- Validate: no duplicate ADT names
       for adtDecl in parsedAdts do
-        if seenNames.contains adtDecl.name then
+        let adtLocalName := localDeclName adtDecl.name
+        if seenNames.contains adtLocalName then
           throwErrorAt adtDecl.ident s!"duplicate type name '{adtDecl.name}'"
-        seenNames := seenNames.push adtDecl.name
+        seenNames := seenNames.push adtLocalName
       -- Validate: ADT names don't shadow built-in types
       for adtDecl in parsedAdts do
         if builtinTypeNames.contains adtDecl.name then
@@ -2890,26 +3253,27 @@ def parseContractSyntax
       let namespaceFromContractSpec : Bool := nsSpec.isSome
       let parsedErrors ←
         match errorDecls with
-        | some decls => decls.mapM (parseError parsedNewtypes parsedStructs parsedAdts)
+        | some decls => decls.mapM (parseError typeNewtypes typeStructs typeAdts)
         | none => pure #[]
       let parsedEvents ←
         match eventDecls with
-        | some decls => decls.mapM (parseEvent parsedNewtypes parsedStructs parsedAdts)
+        | some decls => decls.mapM (parseEvent typeNewtypes typeStructs typeAdts)
         | none => pure #[]
       let parsedConstants ←
         match constantDecls with
-        | some decls => decls.mapM (parseConstant parsedNewtypes)
+        | some decls => decls.mapM (parseConstant typeNewtypes)
         | none => pure #[]
       let parsedImmutables ←
         match immutableDecls with
-        | some decls => decls.mapM (parseImmutable parsedNewtypes)
+        | some decls => decls.mapM (parseImmutable typeNewtypes)
         | none => pure #[]
       let parsedInterfaces ←
         match interfaceDecls with
-        | some decls => decls.mapM (parseInterface parsedNewtypes parsedStructs parsedAdts)
+        | some decls => decls.mapM (parseInterface typeNewtypes typeStructs typeAdts)
         | none => pure #[]
-      let seenTypeLocalNames := seenNames.map localDeclName
-      let mut seenInterfaceNames : Array String := #[]
+      let seenTypeLocalNames := seenNames
+      let mut seenInterfaceNames : Array String := parent?.map (fun p =>
+        p.interfaceDecls.map (fun iface => localDeclName iface.name)) |>.getD #[]
       for iface in parsedInterfaces do
         let ifaceLocalName := localDeclName iface.name
         if seenTypeLocalNames.contains ifaceLocalName then
@@ -2919,10 +3283,12 @@ def parseContractSyntax
         if seenInterfaceNames.contains ifaceLocalName then
           throwErrorAt iface.ident s!"duplicate interface name '{ifaceLocalName}'"
         seenInterfaceNames := seenInterfaceNames.push ifaceLocalName
-      let interfaceNames := parsedInterfaces.map (·.name)
+      let inheritedInterfaceNames := parent?.map (fun p =>
+        p.interfaceDecls.map (·.name)) |>.getD #[]
+      let interfaceNames := inheritedInterfaceNames ++ parsedInterfaces.map (·.name)
       let parsedExternals ←
         match externalDecls with
-        | some decls => decls.mapM (parseExternal parsedNewtypes parsedStructs parsedAdts)
+        | some decls => decls.mapM (parseExternal typeNewtypes typeStructs typeAdts)
         | none => pure #[]
       let parsedExternals := interfaceExternals parsedInterfaces ++ parsedExternals
       -- Apply namespace offsets to parsed storage fields (#1730).  In-storage
@@ -2947,12 +3313,12 @@ def parseContractSyntax
               firstNamespaceOpt := some offset
               firstNamespaceLocked := true
         | none =>
-            match (← parseTransientStorageItem parsedNewtypes parsedStructs parsedAdts item) with
+            match (← parseTransientStorageItem typeNewtypes typeStructs typeAdts item) with
             | some field =>
                 parsedFields := parsedFields.push { field with slotNum := field.slotNum + currentNamespaceOffset }
                 firstNamespaceLocked := true
             | none =>
-                match (← parseStorageStructItem parsedNewtypes parsedStructs parsedAdts item) with
+                match (← parseStorageStructItem typeNewtypes typeStructs typeAdts item) with
                 | some (structFields, accessor) =>
                     parsedFields := parsedFields ++
                       (structFields.map fun field => { field with slotNum := field.slotNum + currentNamespaceOffset })
@@ -2965,7 +3331,7 @@ def parseContractSyntax
                 | none =>
                     match (← storageFieldFromItem? item) with
                     | some fieldStx =>
-                        let field ← parseStorageField parsedNewtypes parsedStructs parsedAdts fieldStx
+                        let field ← parseStorageField typeNewtypes typeStructs typeAdts fieldStx
                         parsedFields := parsedFields.push { field with slotNum := field.slotNum + currentNamespaceOffset }
                         firstNamespaceLocked := true
                     | none =>
@@ -2978,17 +3344,29 @@ def parseContractSyntax
               throwErrorAt field.ident
                 "transient fixed arrays are not supported until fixed-array lowering uses tload/tstore"
           | _ => pure ()
+      let roleFields := parent?.map (fun p => p.fields ++ parsedFields) |>.getD parsedFields
       let parsedRoles ←
         match roleDecls with
-        | some decls => decls.mapM (parseRoleDecl parsedFields)
+        | some decls => decls.mapM (parseRoleDecl roleFields)
         | none => pure #[]
       let mut seenRoleNames : Array String := #[]
       for role in parsedRoles do
         if seenRoleNames.contains role.name then
           throwErrorAt role.ident s!"duplicate role declaration '{role.name}'"
         seenRoleNames := seenRoleNames.push role.name
-      pure {
+      let parsedModifiers ← modifierDecls.mapM parseModifier
+      for modDecl in parsedModifiers do
+        if modifierSyntaxTerminates modDecl.body.raw then
+          throwErrorAt modDecl.body
+            s!"modifier '{modDecl.name}' contains a terminating return; modifiers must only contain non-terminating precondition statements"
+      let parsedFunctions :=
+        assignOverloadInternalIdents
+          (← monomorphizeHigherOrderHelpers
+            ((← entrypoints.mapM parseSpecialEntrypoint) ++
+              (← functions.mapM (parseFunction typeNewtypes typeStructs typeAdts interfaceNames))))
+      let own : ParsedContractSyntax := {
         contractName := contractName
+        parentName? := parentName
         newtypeDecls := parsedNewtypes
         structDecls := parsedStructs
         adtDecls := parsedAdts
@@ -2999,16 +3377,20 @@ def parseContractSyntax
         eventDecls := parsedEvents
         constDecls := parsedConstants
         immutableDecls := parsedImmutables
+        interfaceDecls := parsedInterfaces
         externalDecls := parsedExternals
-        ctor := (← ctor.mapM (parseConstructor parsedNewtypes parsedStructs parsedAdts))
-        modifiers := (← modifierDecls.mapM parseModifier)
-        functions :=
-          assignOverloadInternalIdents
-            (← monomorphizeHigherOrderHelpers
-              ((← entrypoints.mapM parseSpecialEntrypoint) ++
-                (← functions.mapM (parseFunction parsedNewtypes parsedStructs parsedAdts interfaceNames))))
+        ctor := (← ctor.mapM (parseConstructor typeNewtypes typeStructs typeAdts))
+        modifiers := parsedModifiers
+        functions := parsedFunctions
         storageNamespace := firstNamespaceOpt
       }
+      match parentName with
+      | none => pure { own with functions := (← inlineModifierPrefixes own.modifiers own.functions) }
+      | some parentIdent =>
+          let some parent := parent? | unreachable!
+          let flattened ← flattenSingleInheritance parentIdent parent own
+          pure { flattened with
+            functions := (← inlineModifierPrefixes flattened.modifiers flattened.functions) }
   | _ => throwErrorAt stx "invalid verity_contract declaration"
 
 private def mkConstantDefCommand (constant : ConstantDecl) : CommandElabM Cmd := do
diff --git a/Verity/Macro/Translate/Parsing.lean b/Verity/Macro/Translate/Parsing.lean
index 798e06f8c..55443845c 100644
--- a/Verity/Macro/Translate/Parsing.lean
+++ b/Verity/Macro/Translate/Parsing.lean
@@ -525,7 +525,7 @@ def parseModifierUse (stx : TSyntax `verityModifierUse) : CommandElabM (Array Id
 
 def parseFunction (newtypes : Array NewtypeDecl) (structDecls : Array StructDecl := #[]) (adtDecls : Array AdtDecl := #[]) (interfaceNames : Array String := #[]) (stx : Syntax) : CommandElabM FunctionDecl := do
   match stx with
-  | `(verityFunction| function $[$modsBefore:verityMutability]* $[$pureMod?:pureMutabilityMarker]? $[$modsAfter:verityMutability]* $name:ident ($[$params:verityParam],*) $[$guard?:verityInitGuard]? $[$modifierUse?:verityModifierUse]? $[$requiresRoleClause?:verityRequiresRole]? $[$modifiesClause?:verityModifies]? $[$localObligations?:verityLocalObligations]? : $retTy:term := $body:term) => do
+  | `(verityFunction| function $[$modsBefore:verityMutability]* $[$pureMod?:pureMutabilityMarker]? $[$modsAfter:verityMutability]* $[$dispatch:verityDispatch]* $name:ident ($[$params:verityParam],*) $[$guard?:verityInitGuard]? $[$modifierUse?:verityModifierUse]? $[$requiresRoleClause?:verityRequiresRole]? $[$modifiesClause?:verityModifies]? $[$localObligations?:verityLocalObligations]? : $retTy:term := $body:term) => do
       let mut_ ← parseMutabilityModifiers (modsBefore ++ modsAfter) stx
       let mut_ := { mut_ with isPure := pureMod?.isSome }
       let parsedParams ← params.mapM (parseFunctionParamWithInterfaces newtypes structDecls adtDecls interfaceNames)
@@ -553,6 +553,24 @@ def parseFunction (newtypes : Array NewtypeDecl) (structDecls : Array StructDecl
         match localObligations? with
         | some obligations => parseLocalObligations obligations
         | none => pure #[]
+      let isVirtual := dispatch.any fun d =>
+        match d with
+        | `(verityDispatch| virtual) => true
+        | _ => false
+      let isOverride := dispatch.any fun d =>
+        match d with
+        | `(verityDispatch| override) => true
+        | _ => false
+      let virtualCount := dispatch.countP fun d =>
+        match d with
+        | `(verityDispatch| virtual) => true
+        | _ => false
+      let overrideCount := dispatch.countP fun d =>
+        match d with
+        | `(verityDispatch| override) => true
+        | _ => false
+      if virtualCount > 1 || overrideCount > 1 then
+        throwErrorAt name s!"function '{toString name.getId}' has a duplicate dispatch annotation"
       pure {
         ident := name
         name := toString name.getId
@@ -572,12 +590,46 @@ def parseFunction (newtypes : Array NewtypeDecl) (structDecls : Array StructDecl
         modifies := parsedModifies
         localObligations := parsedLocalObligations
         modifiers := parsedModifiers
+        isVirtual := isVirtual
+        isOverride := isOverride
         body := body
       }
   | _ => throwErrorAt stx "invalid function declaration"
 
 def parseConstructor (newtypes : Array NewtypeDecl) (structDecls : Array StructDecl := #[]) (adtDecls : Array AdtDecl := #[]) (stx : Syntax) : CommandElabM ConstructorDecl := do
   match stx with
+  | `(verityConstructor| constructor ($[$params:verityParam],*) payable $parent:ident($[$args:term],*) local_obligations [ $[$obligations:verityLocalObligation],* ] := $body:term) =>
+      pure {
+        params := ← params.mapM (parseParam newtypes structDecls adtDecls)
+        isPayable := true
+        localObligations := ← obligations.mapM parseLocalObligation
+        parentName? := some parent
+        parentArgs := args
+        body := body
+      }
+  | `(verityConstructor| constructor ($[$params:verityParam],*) payable $parent:ident($[$args:term],*) := $body:term) =>
+      pure {
+        params := ← params.mapM (parseParam newtypes structDecls adtDecls)
+        isPayable := true
+        parentName? := some parent
+        parentArgs := args
+        body := body
+      }
+  | `(verityConstructor| constructor ($[$params:verityParam],*) $parent:ident($[$args:term],*) local_obligations [ $[$obligations:verityLocalObligation],* ] := $body:term) =>
+      pure {
+        params := ← params.mapM (parseParam newtypes structDecls adtDecls)
+        localObligations := ← obligations.mapM parseLocalObligation
+        parentName? := some parent
+        parentArgs := args
+        body := body
+      }
+  | `(verityConstructor| constructor ($[$params:verityParam],*) $parent:ident($[$args:term],*) := $body:term) =>
+      pure {
+        params := ← params.mapM (parseParam newtypes structDecls adtDecls)
+        parentName? := some parent
+        parentArgs := args
+        body := body
+      }
   | `(verityConstructor| constructor ($[$params:verityParam],*) payable local_obligations [ $[$obligations:verityLocalObligation],* ] := $body:term) =>
       pure {
         params := ← params.mapM (parseParam newtypes structDecls adtDecls)
diff --git a/Verity/Macro/Types.lean b/Verity/Macro/Types.lean
index 32523c76c..37d22693e 100644
--- a/Verity/Macro/Types.lean
+++ b/Verity/Macro/Types.lean
@@ -238,6 +238,8 @@ structure FunctionDecl where
   modifies : Array Ident := #[]
   localObligations : Array LocalObligationDecl := #[]
   modifiers : Array Ident := #[]
+  isVirtual : Bool := false
+  isOverride : Bool := false
   body : Term
 
 structure InterfaceFunctionDecl where
@@ -261,6 +263,11 @@ structure ConstructorDecl where
   params : Array ParamDecl
   isPayable : Bool := false
   localObligations : Array LocalObligationDecl := #[]
+  /-- Parent-parameter names introduced as lexical bindings while flattening
+      ancestor constructors.  Used to reject capture by later descendants. -/
+  boundParentParamNames : Array String := #[]
+  parentName? : Option Ident := none
+  parentArgs : Array Term := #[]
   body : Term
 
 def strTerm (s : String) : Term := ⟨Syntax.mkStrLit s⟩
@@ -350,7 +357,20 @@ partial def valueTypeFromSyntax
       pure (.tuple elems.toList)
   | `(term| Unit) => pure .unit
   | `(term| $id:ident) =>
-      let tyName := toString id.getId
+      -- Use the source spelling when deciding whether this is one of the
+      -- contract-local declarations. `getId` may contain a namespace added
+      -- while inherited syntax was elaborated, while `rawVal` still records
+      -- whether the author actually wrote a qualifier. In particular, an
+      -- explicitly qualified `Other.Amount` must never capture local
+      -- `Amount` merely because both names have the same final component.
+      let sourceName := match id.raw with
+        | .ident _ rawVal _ _ => rawVal.toString
+        | _ => toString id.getId
+      -- Inherited declarations have already been elaborated, so an
+      -- unqualified type written in the child may carry its resolved
+      -- namespace here.  Contract-local type tables store the source-local
+      -- name; the source spelling preserves that unqualified identity.
+      let tyName := sourceName
       if let some bits := parseNarrowTypeSuffix "Uint" tyName then
         if validIntegerWidth bits then pure (.uintN bits)
         else throwErrorAt ty s!"invalid Solidity unsigned integer width {bits}; expected a multiple of 8 from 8 through 248"
diff --git a/artifacts/macro_property_tests/PropertyConstructorHygieneChild.t.sol b/artifacts/macro_property_tests/PropertyConstructorHygieneChild.t.sol
new file mode 100644
index 000000000..3480b0c08
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyConstructorHygieneChild.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyConstructorHygieneChildTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyConstructorHygieneChildTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYulWithArgs("ConstructorHygieneChild", abi.encode(alice));
+        require(target != address(0), "Deploy failed");
+    }
+
+}
diff --git a/artifacts/macro_property_tests/PropertyConstructorTupleAliasBase.t.sol b/artifacts/macro_property_tests/PropertyConstructorTupleAliasBase.t.sol
new file mode 100644
index 000000000..1a76abaab
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyConstructorTupleAliasBase.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyConstructorTupleAliasBaseTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyConstructorTupleAliasBaseTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("ConstructorTupleAliasBase");
+        require(target != address(0), "Deploy failed");
+    }
+
+}
diff --git a/artifacts/macro_property_tests/PropertyDynamicConstructorBase.t.sol b/artifacts/macro_property_tests/PropertyDynamicConstructorBase.t.sol
new file mode 100644
index 000000000..d1b32d90b
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyDynamicConstructorBase.t.sol
@@ -0,0 +1,25 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyDynamicConstructorBaseTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyDynamicConstructorBaseTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYulWithArgs("DynamicConstructorBase", abi.encode(_singletonUintArray(1)));
+        require(target != address(0), "Deploy failed");
+    }
+
+
+    function _singletonUintArray(uint256 x) internal pure returns (uint256[] memory arr) {
+        arr = new uint256[](1);
+        arr[0] = x;
+    }
+}
diff --git a/artifacts/macro_property_tests/PropertyDynamicConstructorChild.t.sol b/artifacts/macro_property_tests/PropertyDynamicConstructorChild.t.sol
new file mode 100644
index 000000000..40a2736e2
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyDynamicConstructorChild.t.sol
@@ -0,0 +1,25 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyDynamicConstructorChildTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyDynamicConstructorChildTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYulWithArgs("DynamicConstructorChild", abi.encode(_singletonUintArray(1)));
+        require(target != address(0), "Deploy failed");
+    }
+
+
+    function _singletonUintArray(uint256 x) internal pure returns (uint256[] memory arr) {
+        arr = new uint256[](1);
+        arr[0] = x;
+    }
+}
diff --git a/artifacts/macro_property_tests/PropertyEffectCompositionSmoke.t.sol b/artifacts/macro_property_tests/PropertyEffectCompositionSmoke.t.sol
index e56b5b44a..d57928574 100644
--- a/artifacts/macro_property_tests/PropertyEffectCompositionSmoke.t.sol
+++ b/artifacts/macro_property_tests/PropertyEffectCompositionSmoke.t.sol
@@ -28,13 +28,19 @@ contract PropertyEffectCompositionSmokeTest is YulTestBase {
         uint256 actual = abi.decode(ret, (uint256));
         assertEq(actual, expected, "getCounter should return storage slot 0");
     }
-    // Property 2: setOwner has no unexpected revert
+    // Property 2: increment has no unexpected revert
+    function testAuto_Increment_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("increment()"));
+        require(ok, "increment reverted unexpectedly");
+    }
+    // Property 3: setOwner has no unexpected revert
     function testAuto_SetOwner_NoUnexpectedRevert() public {
         vm.prank(alice);
         (bool ok,) = target.call(abi.encodeWithSignature("setOwner(address)", alice));
         require(ok, "setOwner reverted unexpectedly");
     }
-    // Property 3: deposit has no unexpected revert
+    // Property 4: deposit has no unexpected revert
     function testAuto_Deposit_NoUnexpectedRevert() public {
         vm.prank(alice);
         (bool ok,) = target.call(abi.encodeWithSignature("deposit(uint256)", uint256(1)));
diff --git a/artifacts/macro_property_tests/PropertyEmptyNamespacedBase.t.sol b/artifacts/macro_property_tests/PropertyEmptyNamespacedBase.t.sol
new file mode 100644
index 000000000..713f38425
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyEmptyNamespacedBase.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyEmptyNamespacedBaseTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyEmptyNamespacedBaseTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("EmptyNamespacedBase");
+        require(target != address(0), "Deploy failed");
+    }
+
+}
diff --git a/artifacts/macro_property_tests/PropertyFullComboSmoke.t.sol b/artifacts/macro_property_tests/PropertyFullComboSmoke.t.sol
index d869dd24e..86d17896c 100644
--- a/artifacts/macro_property_tests/PropertyFullComboSmoke.t.sol
+++ b/artifacts/macro_property_tests/PropertyFullComboSmoke.t.sol
@@ -17,7 +17,19 @@ contract PropertyFullComboSmokeTest is YulTestBase {
         require(target != address(0), "Deploy failed");
     }
 
-    // Property 1: getBalance reads storage slot 1 and decodes the result
+    // Property 1: deposit enforces its required role
+    function testAuto_Deposit_RejectsUnauthorizedCaller() public {
+        vm.prank(address(0x2222));
+        (bool ok,) = target.call(abi.encodeWithSignature("deposit(uint256)", uint256(1)));
+        require(!ok, "deposit accepted an unauthorized caller");
+    }
+    // Property 2: freeze enforces its required role
+    function testAuto_Freeze_RejectsUnauthorizedCaller() public {
+        vm.prank(address(0x2222));
+        (bool ok,) = target.call(abi.encodeWithSignature("freeze()"));
+        require(!ok, "freeze accepted an unauthorized caller");
+    }
+    // Property 3: getBalance reads storage slot 1 and decodes the result
     function testAuto_GetBalance_ReadsConfiguredStorage() public {
         uint256 expected = uint256(1);
         vm.store(target, bytes32(uint256(1)), bytes32(uint256(expected)));
diff --git a/artifacts/macro_property_tests/PropertyImplicitConstructorChild.t.sol b/artifacts/macro_property_tests/PropertyImplicitConstructorChild.t.sol
new file mode 100644
index 000000000..c90e8ff31
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyImplicitConstructorChild.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyImplicitConstructorChildTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyImplicitConstructorChildTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("ImplicitConstructorChild");
+        require(target != address(0), "Deploy failed");
+    }
+
+}
diff --git a/artifacts/macro_property_tests/PropertyImportedInheritanceBase.t.sol b/artifacts/macro_property_tests/PropertyImportedInheritanceBase.t.sol
new file mode 100644
index 000000000..5fb9e72f7
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyImportedInheritanceBase.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyImportedInheritanceBaseTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/InheritanceImportBase.lean
+ */
+contract PropertyImportedInheritanceBaseTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("ImportedInheritanceBase");
+        require(target != address(0), "Deploy failed");
+    }
+
+}
diff --git a/artifacts/macro_property_tests/PropertyImportedInheritanceChild.t.sol b/artifacts/macro_property_tests/PropertyImportedInheritanceChild.t.sol
new file mode 100644
index 000000000..785171876
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyImportedInheritanceChild.t.sol
@@ -0,0 +1,26 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyImportedInheritanceChildTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/InheritanceImportChild.lean
+ */
+contract PropertyImportedInheritanceChildTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("ImportedInheritanceChild");
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: setImported has no unexpected revert
+    function testAuto_SetImported_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("setImported(uint256)", uint256(1)));
+        require(ok, "setImported reverted unexpectedly");
+    }
+}
diff --git a/artifacts/macro_property_tests/PropertyInheritedEmptyInterfaceBase.t.sol b/artifacts/macro_property_tests/PropertyInheritedEmptyInterfaceBase.t.sol
new file mode 100644
index 000000000..6f4680e6a
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyInheritedEmptyInterfaceBase.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyInheritedEmptyInterfaceBaseTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyInheritedEmptyInterfaceBaseTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("InheritedEmptyInterfaceBase");
+        require(target != address(0), "Deploy failed");
+    }
+
+}
diff --git a/artifacts/macro_property_tests/PropertyInheritedEmptyInterfaceChild.t.sol b/artifacts/macro_property_tests/PropertyInheritedEmptyInterfaceChild.t.sol
new file mode 100644
index 000000000..7fbedbbef
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyInheritedEmptyInterfaceChild.t.sol
@@ -0,0 +1,26 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyInheritedEmptyInterfaceChildTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyInheritedEmptyInterfaceChildTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("InheritedEmptyInterfaceChild");
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: acceptMarker has no unexpected revert
+    function testAuto_AcceptMarker_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("acceptMarker(address)", alice));
+        require(ok, "acceptMarker reverted unexpectedly");
+    }
+}
diff --git a/artifacts/macro_property_tests/PropertyInheritedImmutableChild.t.sol b/artifacts/macro_property_tests/PropertyInheritedImmutableChild.t.sol
new file mode 100644
index 000000000..c1f4ee870
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyInheritedImmutableChild.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyInheritedImmutableChildTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyInheritedImmutableChildTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYulWithArgs("InheritedImmutableChild", abi.encode(alice));
+        require(target != address(0), "Deploy failed");
+    }
+
+}
diff --git a/artifacts/macro_property_tests/PropertyInheritedOverloadChild.t.sol b/artifacts/macro_property_tests/PropertyInheritedOverloadChild.t.sol
new file mode 100644
index 000000000..3cb0567ad
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyInheritedOverloadChild.t.sol
@@ -0,0 +1,38 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyInheritedOverloadChildTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyInheritedOverloadChildTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("InheritedOverloadChild");
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: inspect returns the direct parameter value
+    function testAuto_Inspect_ReturnsDirectParam() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("inspect(uint256)", uint256(1)));
+        require(ok, "inspect reverted unexpectedly");
+        assertEq(ret.length, 32, "inspect ABI return length mismatch (expected 32 bytes)");
+        uint256 actual = abi.decode(ret, (uint256));
+        assertEq(actual, uint256(1), "inspect should preserve the expected value");
+    }
+    // Property 2: inspect returns the direct parameter value
+    function testAuto_Inspect_ReturnsDirectParam() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("inspect(address)", alice));
+        require(ok, "inspect reverted unexpectedly");
+        assertEq(ret.length, 32, "inspect ABI return length mismatch (expected 32 bytes)");
+        address actual = abi.decode(ret, (address));
+        assertEq(actual, alice, "inspect should preserve the expected value");
+    }
+}
diff --git a/artifacts/macro_property_tests/PropertyInheritedRoleBase.t.sol b/artifacts/macro_property_tests/PropertyInheritedRoleBase.t.sol
new file mode 100644
index 000000000..b62493bec
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyInheritedRoleBase.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyInheritedRoleBaseTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyInheritedRoleBaseTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("InheritedRoleBase");
+        require(target != address(0), "Deploy failed");
+    }
+
+}
diff --git a/artifacts/macro_property_tests/PropertyInheritedRoleChild.t.sol b/artifacts/macro_property_tests/PropertyInheritedRoleChild.t.sol
new file mode 100644
index 000000000..148b99f95
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyInheritedRoleChild.t.sol
@@ -0,0 +1,26 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyInheritedRoleChildTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyInheritedRoleChildTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("InheritedRoleChild");
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: audit enforces its required role
+    function testAuto_Audit_RejectsUnauthorizedCaller() public {
+        vm.prank(address(0x2222));
+        (bool ok,) = target.call(abi.encodeWithSignature("audit()"));
+        require(!ok, "audit accepted an unauthorized caller");
+    }
+}
diff --git a/artifacts/macro_property_tests/PropertyInheritedTypeNameBase.t.sol b/artifacts/macro_property_tests/PropertyInheritedTypeNameBase.t.sol
new file mode 100644
index 000000000..1e4bf20b3
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyInheritedTypeNameBase.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyInheritedTypeNameBaseTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyInheritedTypeNameBaseTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("InheritedTypeNameBase");
+        require(target != address(0), "Deploy failed");
+    }
+
+}
diff --git a/artifacts/macro_property_tests/PropertyInitializerSmoke.t.sol b/artifacts/macro_property_tests/PropertyInitializerSmoke.t.sol
index 143e3e866..e3879cc27 100644
--- a/artifacts/macro_property_tests/PropertyInitializerSmoke.t.sol
+++ b/artifacts/macro_property_tests/PropertyInitializerSmoke.t.sol
@@ -17,4 +17,16 @@ contract PropertyInitializerSmokeTest is YulTestBase {
         require(target != address(0), "Deploy failed");
     }
 
+    // Property 1: initOwner has no unexpected revert
+    function testAuto_InitOwner_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("initOwner(address)", alice));
+        require(ok, "initOwner reverted unexpectedly");
+    }
+    // Property 2: upgradeToV2 has no unexpected revert
+    function testAuto_UpgradeToV2_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("upgradeToV2()"));
+        require(ok, "upgradeToV2 reverted unexpectedly");
+    }
 }
diff --git a/artifacts/macro_property_tests/PropertyLocalObligationMacroSmoke.t.sol b/artifacts/macro_property_tests/PropertyLocalObligationMacroSmoke.t.sol
index eaf58476f..60b6602de 100644
--- a/artifacts/macro_property_tests/PropertyLocalObligationMacroSmoke.t.sol
+++ b/artifacts/macro_property_tests/PropertyLocalObligationMacroSmoke.t.sol
@@ -17,4 +17,19 @@ contract PropertyLocalObligationMacroSmokeTest is YulTestBase {
         require(target != address(0), "Deploy failed");
     }
 
+    // Property 1: unsafeEdge has no unexpected revert
+    function testAuto_UnsafeEdge_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("unsafeEdge()"));
+        require(ok, "unsafeEdge reverted unexpectedly");
+    }
+    // Property 2: dischargedEdge decodes and matches the inferred straight-line result
+    function testAuto_DischargedEdge_ReturnsInferredStraightLineResult() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("dischargedEdge(uint256)", uint256(1)));
+        require(ok, "dischargedEdge reverted unexpectedly");
+        assertEq(ret.length, 32, "dischargedEdge ABI return length mismatch (expected 32 bytes)");
+        uint256 actual = abi.decode(ret, (uint256));
+        assertEq(actual, uint256(1), "dischargedEdge should preserve the inferred result");
+    }
 }
diff --git a/artifacts/macro_property_tests/PropertyModifierInheritanceBase.t.sol b/artifacts/macro_property_tests/PropertyModifierInheritanceBase.t.sol
new file mode 100644
index 000000000..7f50b869b
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyModifierInheritanceBase.t.sol
@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyModifierInheritanceBaseTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyModifierInheritanceBaseTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYulWithArgs("ModifierInheritanceBase", abi.encode(alice));
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: value returns the declared constant result
+    function testAuto_Value_ReturnsDeclaredConstant() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("value()"));
+        require(ok, "value reverted unexpectedly");
+        assertEq(ret.length, 32, "value ABI return length mismatch (expected 32 bytes)");
+        uint256 actual = abi.decode(ret, (uint256));
+        assertEq(actual, 1, "value should return the declared constant");
+    }
+}
diff --git a/artifacts/macro_property_tests/PropertyModifierInheritanceChild.t.sol b/artifacts/macro_property_tests/PropertyModifierInheritanceChild.t.sol
new file mode 100644
index 000000000..e52cbeb27
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyModifierInheritanceChild.t.sol
@@ -0,0 +1,41 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyModifierInheritanceChildTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyModifierInheritanceChildTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYulWithArgs("ModifierInheritanceChild", abi.encode(alice));
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: value returns the declared constant result
+    function testAuto_Value_ReturnsDeclaredConstant() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("value()"));
+        require(ok, "value reverted unexpectedly");
+        assertEq(ret.length, 32, "value ABI return length mismatch (expected 32 bytes)");
+        uint256 actual = abi.decode(ret, (uint256));
+        assertEq(actual, 2, "value should return the declared constant");
+    }
+    // Property 2: bump has no unexpected revert
+    function testAuto_Bump_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("bump()"));
+        require(ok, "bump reverted unexpectedly");
+    }
+    // Property 3: setInherited has no unexpected revert
+    function testAuto_SetInherited_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("setInherited(uint256)", uint256(1)));
+        require(ok, "setInherited reverted unexpectedly");
+    }
+}
diff --git a/artifacts/macro_property_tests/PropertyModifierTupleAliasBase.t.sol b/artifacts/macro_property_tests/PropertyModifierTupleAliasBase.t.sol
new file mode 100644
index 000000000..9304e7d90
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyModifierTupleAliasBase.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyModifierTupleAliasBaseTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyModifierTupleAliasBaseTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("ModifierTupleAliasBase");
+        require(target != address(0), "Deploy failed");
+    }
+
+}
diff --git a/artifacts/macro_property_tests/PropertyModifiesNamespaceSmoke.t.sol b/artifacts/macro_property_tests/PropertyModifiesNamespaceSmoke.t.sol
index a334c3467..b93766327 100644
--- a/artifacts/macro_property_tests/PropertyModifiesNamespaceSmoke.t.sol
+++ b/artifacts/macro_property_tests/PropertyModifiesNamespaceSmoke.t.sol
@@ -17,7 +17,19 @@ contract PropertyModifiesNamespaceSmokeTest is YulTestBase {
         require(target != address(0), "Deploy failed");
     }
 
-    // Property 1: getCounter reads storage slot 0 and decodes the result
+    // Property 1: increment has no unexpected revert
+    function testAuto_Increment_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("increment()"));
+        require(ok, "increment reverted unexpectedly");
+    }
+    // Property 2: transferOwnership has no unexpected revert
+    function testAuto_TransferOwnership_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("transferOwnership(address)", alice));
+        require(ok, "transferOwnership reverted unexpectedly");
+    }
+    // Property 3: getCounter reads storage slot 0 and decodes the result
     function testAuto_GetCounter_ReadsConfiguredStorage() public {
         uint256 expected = uint256(1);
         vm.store(target, bytes32(uint256(0)), bytes32(uint256(expected)));
diff --git a/artifacts/macro_property_tests/PropertyModifiesRolesSmoke.t.sol b/artifacts/macro_property_tests/PropertyModifiesRolesSmoke.t.sol
index 448145b08..39b4fe4a3 100644
--- a/artifacts/macro_property_tests/PropertyModifiesRolesSmoke.t.sol
+++ b/artifacts/macro_property_tests/PropertyModifiesRolesSmoke.t.sol
@@ -17,7 +17,19 @@ contract PropertyModifiesRolesSmokeTest is YulTestBase {
         require(target != address(0), "Deploy failed");
     }
 
-    // Property 1: getCounter reads storage slot 1 and decodes the result
+    // Property 1: setCounter enforces its required role
+    function testAuto_SetCounter_RejectsUnauthorizedCaller() public {
+        vm.prank(address(0x2222));
+        (bool ok,) = target.call(abi.encodeWithSignature("setCounter(uint256)", uint256(1)));
+        require(!ok, "setCounter accepted an unauthorized caller");
+    }
+    // Property 2: setCounterAndFlag enforces its required role
+    function testAuto_SetCounterAndFlag_RejectsUnauthorizedCaller() public {
+        vm.prank(address(0x2222));
+        (bool ok,) = target.call(abi.encodeWithSignature("setCounterAndFlag(uint256,uint256)", uint256(1), uint256(1)));
+        require(!ok, "setCounterAndFlag accepted an unauthorized caller");
+    }
+    // Property 3: getCounter reads storage slot 1 and decodes the result
     function testAuto_GetCounter_ReadsConfiguredStorage() public {
         uint256 expected = uint256(1);
         vm.store(target, bytes32(uint256(1)), bytes32(uint256(expected)));
diff --git a/artifacts/macro_property_tests/PropertyModifiesSmoke.t.sol b/artifacts/macro_property_tests/PropertyModifiesSmoke.t.sol
index f3ca1e142..37628132a 100644
--- a/artifacts/macro_property_tests/PropertyModifiesSmoke.t.sol
+++ b/artifacts/macro_property_tests/PropertyModifiesSmoke.t.sol
@@ -17,7 +17,25 @@ contract PropertyModifiesSmokeTest is YulTestBase {
         require(target != address(0), "Deploy failed");
     }
 
-    // Property 1: getCounter reads storage slot 0 and decodes the result
+    // Property 1: increment has no unexpected revert
+    function testAuto_Increment_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("increment()"));
+        require(ok, "increment reverted unexpectedly");
+    }
+    // Property 2: transferOwnership has no unexpected revert
+    function testAuto_TransferOwnership_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("transferOwnership(address)", alice));
+        require(ok, "transferOwnership reverted unexpectedly");
+    }
+    // Property 3: deposit has no unexpected revert
+    function testAuto_Deposit_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("deposit(uint256)", uint256(1)));
+        require(ok, "deposit reverted unexpectedly");
+    }
+    // Property 4: getCounter reads storage slot 0 and decodes the result
     function testAuto_GetCounter_ReadsConfiguredStorage() public {
         uint256 expected = uint256(1);
         vm.store(target, bytes32(uint256(0)), bytes32(uint256(expected)));
diff --git a/artifacts/macro_property_tests/PropertyNamespacedFieldBase.t.sol b/artifacts/macro_property_tests/PropertyNamespacedFieldBase.t.sol
new file mode 100644
index 000000000..312ea6af1
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyNamespacedFieldBase.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyNamespacedFieldBaseTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyNamespacedFieldBaseTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("NamespacedFieldBase");
+        require(target != address(0), "Deploy failed");
+    }
+
+}
diff --git a/artifacts/macro_property_tests/PropertyNamespacedFieldChild.t.sol b/artifacts/macro_property_tests/PropertyNamespacedFieldChild.t.sol
new file mode 100644
index 000000000..6110e8028
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyNamespacedFieldChild.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyNamespacedFieldChildTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyNamespacedFieldChildTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("NamespacedFieldChild");
+        require(target != address(0), "Deploy failed");
+    }
+
+}
diff --git a/artifacts/macro_property_tests/PropertyNamespacedFirstChild.t.sol b/artifacts/macro_property_tests/PropertyNamespacedFirstChild.t.sol
new file mode 100644
index 000000000..eb1069b1d
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyNamespacedFirstChild.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyNamespacedFirstChildTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyNamespacedFirstChildTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("NamespacedFirstChild");
+        require(target != address(0), "Deploy failed");
+    }
+
+}
diff --git a/artifacts/macro_property_tests/PropertyNarrowConstructorBase.t.sol b/artifacts/macro_property_tests/PropertyNarrowConstructorBase.t.sol
new file mode 100644
index 000000000..c236d8c8b
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyNarrowConstructorBase.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyNarrowConstructorBaseTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyNarrowConstructorBaseTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYulWithArgs("NarrowConstructorBase", abi.encode(uint8(27)));
+        require(target != address(0), "Deploy failed");
+    }
+
+}
diff --git a/artifacts/macro_property_tests/PropertyNewtypeModifiesSmoke.t.sol b/artifacts/macro_property_tests/PropertyNewtypeModifiesSmoke.t.sol
index 9d2a60b42..7c564caba 100644
--- a/artifacts/macro_property_tests/PropertyNewtypeModifiesSmoke.t.sol
+++ b/artifacts/macro_property_tests/PropertyNewtypeModifiesSmoke.t.sol
@@ -17,7 +17,13 @@ contract PropertyNewtypeModifiesSmokeTest is YulTestBase {
         require(target != address(0), "Deploy failed");
     }
 
-    // Property 1: getNextId reads storage slot 0 and decodes the result
+    // Property 1: mint has no unexpected revert
+    function testAuto_Mint_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("mint(uint256,uint256)", uint256(1), uint256(1)));
+        require(ok, "mint reverted unexpectedly");
+    }
+    // Property 2: getNextId reads storage slot 0 and decodes the result
     function testAuto_GetNextId_ReadsConfiguredStorage() public {
         uint256 expected = uint256(1);
         vm.store(target, bytes32(uint256(0)), bytes32(uint256(expected)));
diff --git a/artifacts/macro_property_tests/PropertyNonreentrantModifiesSmoke.t.sol b/artifacts/macro_property_tests/PropertyNonreentrantModifiesSmoke.t.sol
index 99bcc1a4a..14d36662a 100644
--- a/artifacts/macro_property_tests/PropertyNonreentrantModifiesSmoke.t.sol
+++ b/artifacts/macro_property_tests/PropertyNonreentrantModifiesSmoke.t.sol
@@ -17,7 +17,16 @@ contract PropertyNonreentrantModifiesSmokeTest is YulTestBase {
         require(target != address(0), "Deploy failed");
     }
 
-    // Property 1: getBalance reads storage slot 2 and decodes the result
+    // Property 1: TODO decode and assert `deposit` result
+    function testTODO_Deposit_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("deposit(uint256)", uint256(1)));
+        require(ok, "deposit reverted unexpectedly");
+        assertEq(ret.length, 32, "deposit ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 2: getBalance reads storage slot 2 and decodes the result
     function testAuto_GetBalance_ReadsConfiguredStorage() public {
         uint256 expected = uint256(1);
         vm.store(target, bytes32(uint256(2)), bytes32(uint256(expected)));
diff --git a/artifacts/macro_property_tests/PropertyRolesCEISmoke.t.sol b/artifacts/macro_property_tests/PropertyRolesCEISmoke.t.sol
index b5647fa5a..7473cf518 100644
--- a/artifacts/macro_property_tests/PropertyRolesCEISmoke.t.sol
+++ b/artifacts/macro_property_tests/PropertyRolesCEISmoke.t.sol
@@ -17,7 +17,13 @@ contract PropertyRolesCEISmokeTest is YulTestBase {
         require(target != address(0), "Deploy failed");
     }
 
-    // Property 1: getCounter reads storage slot 1 and decodes the result
+    // Property 1: setAndCall enforces its required role
+    function testAuto_SetAndCall_RejectsUnauthorizedCaller() public {
+        vm.prank(address(0x2222));
+        (bool ok,) = target.call(abi.encodeWithSignature("setAndCall(uint256)", uint256(1)));
+        require(!ok, "setAndCall accepted an unauthorized caller");
+    }
+    // Property 2: getCounter reads storage slot 1 and decodes the result
     function testAuto_GetCounter_ReadsConfiguredStorage() public {
         uint256 expected = uint256(1);
         vm.store(target, bytes32(uint256(1)), bytes32(uint256(expected)));
diff --git a/artifacts/macro_property_tests/PropertyRolesDeclaredSmoke.t.sol b/artifacts/macro_property_tests/PropertyRolesDeclaredSmoke.t.sol
index 0bb8112b0..974a2ba47 100644
--- a/artifacts/macro_property_tests/PropertyRolesDeclaredSmoke.t.sol
+++ b/artifacts/macro_property_tests/PropertyRolesDeclaredSmoke.t.sol
@@ -17,4 +17,28 @@ contract PropertyRolesDeclaredSmokeTest is YulTestBase {
         require(target != address(0), "Deploy failed");
     }
 
+    // Property 1: setByOwner enforces its required role
+    function testAuto_SetByOwner_RejectsUnauthorizedCaller() public {
+        vm.prank(address(0x2222));
+        (bool ok,) = target.call(abi.encodeWithSignature("setByOwner(uint256)", uint256(1)));
+        require(!ok, "setByOwner accepted an unauthorized caller");
+    }
+    // Property 2: setByAdmin enforces its required role
+    function testAuto_SetByAdmin_RejectsUnauthorizedCaller() public {
+        vm.prank(address(0x2222));
+        (bool ok,) = target.call(abi.encodeWithSignature("setByAdmin(uint256)", uint256(1)));
+        require(!ok, "setByAdmin accepted an unauthorized caller");
+    }
+    // Property 3: mintLike enforces its required role
+    function testAuto_MintLike_RejectsUnauthorizedCaller() public {
+        vm.prank(address(0x2222));
+        (bool ok,) = target.call(abi.encodeWithSignature("mintLike(uint256)", uint256(1)));
+        require(!ok, "mintLike accepted an unauthorized caller");
+    }
+    // Property 4: relayLike enforces its required role
+    function testAuto_RelayLike_RejectsUnauthorizedCaller() public {
+        vm.prank(address(0x2222));
+        (bool ok,) = target.call(abi.encodeWithSignature("relayLike(uint256)", uint256(1)));
+        require(!ok, "relayLike accepted an unauthorized caller");
+    }
 }
diff --git a/artifacts/macro_property_tests/PropertyRolesMappingSmoke.t.sol b/artifacts/macro_property_tests/PropertyRolesMappingSmoke.t.sol
index 6953fca77..bf18537d7 100644
--- a/artifacts/macro_property_tests/PropertyRolesMappingSmoke.t.sol
+++ b/artifacts/macro_property_tests/PropertyRolesMappingSmoke.t.sol
@@ -17,7 +17,13 @@ contract PropertyRolesMappingSmokeTest is YulTestBase {
         require(target != address(0), "Deploy failed");
     }
 
-    // Property 1: getCounter reads storage slot 1 and decodes the result
+    // Property 1: setCounter enforces its required role
+    function testAuto_SetCounter_RejectsUnauthorizedCaller() public {
+        vm.prank(address(0x2222));
+        (bool ok,) = target.call(abi.encodeWithSignature("setCounter(uint256)", uint256(1)));
+        require(!ok, "setCounter accepted an unauthorized caller");
+    }
+    // Property 2: getCounter reads storage slot 1 and decodes the result
     function testAuto_GetCounter_ReadsConfiguredStorage() public {
         uint256 expected = uint256(1);
         vm.store(target, bytes32(uint256(1)), bytes32(uint256(expected)));
diff --git a/artifacts/macro_property_tests/PropertyRolesSmoke.t.sol b/artifacts/macro_property_tests/PropertyRolesSmoke.t.sol
index 8086a92b8..f1b8b2acd 100644
--- a/artifacts/macro_property_tests/PropertyRolesSmoke.t.sol
+++ b/artifacts/macro_property_tests/PropertyRolesSmoke.t.sol
@@ -17,7 +17,13 @@ contract PropertyRolesSmokeTest is YulTestBase {
         require(target != address(0), "Deploy failed");
     }
 
-    // Property 1: getCounter reads storage slot 1 and decodes the result
+    // Property 1: setCounter enforces its required role
+    function testAuto_SetCounter_RejectsUnauthorizedCaller() public {
+        vm.prank(address(0x2222));
+        (bool ok,) = target.call(abi.encodeWithSignature("setCounter(uint256)", uint256(1)));
+        require(!ok, "setCounter accepted an unauthorized caller");
+    }
+    // Property 2: getCounter reads storage slot 1 and decodes the result
     function testAuto_GetCounter_ReadsConfiguredStorage() public {
         uint256 expected = uint256(1);
         vm.store(target, bytes32(uint256(1)), bytes32(uint256(expected)));
diff --git a/artifacts/macro_property_tests/PropertyTypedNarrowConstructorBase.t.sol b/artifacts/macro_property_tests/PropertyTypedNarrowConstructorBase.t.sol
new file mode 100644
index 000000000..736537d17
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyTypedNarrowConstructorBase.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyTypedNarrowConstructorBaseTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyTypedNarrowConstructorBaseTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYulWithArgs("TypedNarrowConstructorBase", abi.encode(uint24(1)));
+        require(target != address(0), "Deploy failed");
+    }
+
+}
diff --git a/artifacts/macro_property_tests/PropertyTypedNarrowConstructorChild.t.sol b/artifacts/macro_property_tests/PropertyTypedNarrowConstructorChild.t.sol
new file mode 100644
index 000000000..6a0776e92
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyTypedNarrowConstructorChild.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyTypedNarrowConstructorChildTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyTypedNarrowConstructorChildTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("TypedNarrowConstructorChild");
+        require(target != address(0), "Deploy failed");
+    }
+
+}
diff --git a/artifacts/macro_property_tests/PropertyVirtualOverrideLeaf.t.sol b/artifacts/macro_property_tests/PropertyVirtualOverrideLeaf.t.sol
new file mode 100644
index 000000000..940f52df5
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyVirtualOverrideLeaf.t.sol
@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyVirtualOverrideLeafTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyVirtualOverrideLeafTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYulWithArgs("VirtualOverrideLeaf", abi.encode(alice));
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: value returns the declared constant result
+    function testAuto_Value_ReturnsDeclaredConstant() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("value()"));
+        require(ok, "value reverted unexpectedly");
+        assertEq(ret.length, 32, "value ABI return length mismatch (expected 32 bytes)");
+        uint256 actual = abi.decode(ret, (uint256));
+        assertEq(actual, 3, "value should return the declared constant");
+    }
+}
diff --git a/artifacts/macro_property_tests/PropertyVirtualOverrideMiddle.t.sol b/artifacts/macro_property_tests/PropertyVirtualOverrideMiddle.t.sol
new file mode 100644
index 000000000..70e2f35d4
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyVirtualOverrideMiddle.t.sol
@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyVirtualOverrideMiddleTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Helpers.lean
+ */
+contract PropertyVirtualOverrideMiddleTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYulWithArgs("VirtualOverrideMiddle", abi.encode(alice));
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: value returns the declared constant result
+    function testAuto_Value_ReturnsDeclaredConstant() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("value()"));
+        require(ok, "value reverted unexpectedly");
+        assertEq(ret.length, 32, "value ABI return length mismatch (expected 32 bytes)");
+        uint256 actual = abi.decode(ret, (uint256));
+        assertEq(actual, 2, "value should return the declared constant");
+    }
+}
diff --git a/docs/MODIFIERS_AND_INHERITANCE.md b/docs/MODIFIERS_AND_INHERITANCE.md
new file mode 100644
index 000000000..2be38952f
--- /dev/null
+++ b/docs/MODIFIERS_AND_INHERITANCE.md
@@ -0,0 +1,26 @@
+# Modifiers and inheritance
+
+`verity_contract` supports precondition-only user-defined modifiers, flattened
+single inheritance, direct parent-constructor calls, and compile-time
+`virtual`/`override` specialization.
+
+Modifiers are declared with `modifier name := do ...` and attached with
+`with name`. Their statements are inserted, in declaration order, before the
+function body in both executable semantics and the compilation model. The
+current stage is intended for checks such as `onlyOwner`; Solidity-style `_`
+placement and postcondition code are not supported.
+
+A child uses `verity_contract Child is Parent where`. The parent must be
+declared earlier in the same module. Storage, declarations, modifiers, and
+functions are flattened into the child. A child constructor calls its direct
+parent with `constructor (...) Parent(args...) := do ...`; parent initialization
+runs before the child body.
+
+Mark a parent slot with `function virtual ...` and replace the same ABI
+signature in the child with `function override ...`. Missing targets,
+overrides of non-virtual functions, and accidental signature collisions are
+compile-time errors. Dispatch is specialized during elaboration, so no runtime
+dispatch table or additional proof axiom is introduced.
+
+Multiple inheritance/C3 linearization, abstract body-less functions,
+parameterized modifiers, and modifier postludes remain out of scope.
diff --git a/docs/parity/erc4337.md b/docs/parity/erc4337.md
index 1a567731f..bbcd6d6ef 100644
--- a/docs/parity/erc4337.md
+++ b/docs/parity/erc4337.md
@@ -154,8 +154,8 @@ issues [#1724](https://github.com/lfglabs-dev/verity/issues/1724),
 | error | `NotFromEntryPoint(address,address,address)` | ✅ | |
 | error | `ERC165Error(address, bytes4)` | ❌ | `bytes4` payload. |
 | error | `MustOverride()` | ✅ | |
-| inheritance | `is IPaymaster, Stakeable` (via `Ownable2Step`) | ❌ | No `is X, Y`. |
-| constructor | `constructor(IEntryPoint, address) Ownable(owner)` | ❌ | Parent-constructor call + inheritance. |
+| inheritance | `is IPaymaster, Stakeable` (via `Ownable2Step`) | 🚧 | Flattened single inheritance is supported; this multiple-inheritance chain still needs C3 linearization. |
+| constructor | `constructor(IEntryPoint, address) Ownable(owner)` | 🚧 | Direct parent-constructor calls are supported; the remaining gap is the surrounding multiple-inheritance chain. |
 | fn | `entryPoint() public view returns (IEntryPoint)` | 🚧 | Return as `address`. |
 | fn | `_validateEntryPointInterface(IEntryPoint) internal` | ❌ | Uses `type(IEntryPoint).interfaceId` (`bytes4`) + `IERC165(...).supportsInterface`. |
 | fn | `validatePaymasterUserOp(...) external` | 🚧 | Body dispatches to internal template; template itself is ❌ (abstract). |
@@ -163,7 +163,7 @@ issues [#1724](https://github.com/lfglabs-dev/verity/issues/1724),
 | fn | `postOp(PostOpMode,...) external` | ❌ | Enum arg. |
 | fn | `_postOp(...) internal virtual` | ❌ | Abstract + enum. |
 | fn | `deposit() public payable` | ✅ | |
-| fn | `withdrawTo(address payable, uint256) public onlyOwner` | ❌ | Modifier system + inherited `Ownable`. |
+| fn | `withdrawTo(address payable, uint256) public onlyOwner` | ✅ | Precondition-only user modifiers and inherited modifiers inline at compile time. |
 | fn | `getDeposit() public view returns (uint256)` | ✅ | |
 | fn | `_requireFromEntryPoint() internal` | ✅ | |
 
@@ -192,7 +192,7 @@ issues [#1724](https://github.com/lfglabs-dev/verity/issues/1724),
 | storage | `address public owner` | ✅ | |
 | storage | `IEntryPoint private immutable _entryPoint` | 🚧 | As `address`. |
 | event | `SimpleAccountInitialized(IEntryPoint indexed, address indexed)` | ✅ | |
-| modifier | `onlyOwner()` | ❌ | Only `nonReentrant` supported (#2076). Workaround: inline `require`. |
+| modifier | `onlyOwner()` | ✅ | Precondition-only user modifiers inline as require prefixes. |
 | error | `NotOwner(address,address,address)` | ✅ | |
 | error | `NotOwnerOrEntryPoint(address,address,address,address)` | ✅ | |
 | inheritance | `is BaseAccount, TokenCallbackHandler, UUPSUpgradeable, Initializable` | ❌ | No multi-inheritance. |
diff --git a/docs/parity/lido.md b/docs/parity/lido.md
index 7e6ad0146..8a2a065c3 100644
--- a/docs/parity/lido.md
+++ b/docs/parity/lido.md
@@ -29,7 +29,7 @@ errors with scalar payloads, `require`, bounded `for`, `if/else`, ternary,
 low-level `call`/`staticcall`/`delegatecall` (no proof coverage). ❌:
 `uint128/64/32/24/16`, `int128`, `bytes4/20`, `enum`, storage `string`/`bytes`,
 top-level `struct` as storage root, `mapping` depth ≥ 3 (no proof),
-inheritance, modifiers as first class, `abi.encode`/`abi.encodePacked`,
+multiple inheritance, modifier postludes, `abi.encode`/`abi.encodePacked`,
 `try/catch`, `while`, `break/continue`, `CREATE`/`CREATE2`, `transfer`/`send`,
 `receive`/`fallback`.
 
@@ -287,7 +287,7 @@ inline.
 
 | Construct | Status | Feature gap |
 |---|---|---|
-| `contract AccountingOracle is BaseOracle` | ❌ | inheritance |
+| `contract AccountingOracle is BaseOracle` | ✅ | flattened single inheritance; virtual overrides specialize at compile time |
 | `initialize(...)` / `finalizeUpgrade_v5(uint256)` | ❌ | modifiers |
 | `submitReportData(ReportData calldata, uint256)` | ❌ | large calldata struct with nested fields |
 | `_checkStakingRouterModuleBalances(sanityChecker, data, timeElapsed)` (SRV3-P3 P4 anchor) | 🚧 | staticcall + bounded loop |
diff --git a/docs/parity/morpho.md b/docs/parity/morpho.md
index eacc4c110..dff397ec2 100644
--- a/docs/parity/morpho.md
+++ b/docs/parity/morpho.md
@@ -29,8 +29,9 @@ storage projections and is therefore excluded from the parity target.
 3. No mapping-of-mapping-of-mapping with proofs (2 max) — `position[id][user]`
    is fine (mapping2), and `MarketParams` inside `idToMarketParams[id]` is a
    struct-in-mapping.
-4. No inheritance, no first-class modifiers, no `abi.encode`, no `try/catch`,
-   no callback (`onMorphoSupply`, `onMorphoRepay`, `onMorphoSupplyCollateral`,
+4. Single inheritance and precondition-only modifiers are supported; multiple
+   inheritance, modifier postludes, `abi.encode`, and `try/catch` remain gaps.
+5. No callback (`onMorphoSupply`, `onMorphoRepay`, `onMorphoSupplyCollateral`,
    `onMorphoLiquidate`, `onMorphoFlashLoan`) trust-boundary primitive.
 
 Rows marked 🚧 with "packed struct in mapping (#1976)" assume the EDSL packs
@@ -74,8 +75,8 @@ Total constructs counted: **72**.
 | # | Construct | Solidity | Verity status | Note |
 |---|-----------|----------|---------------|------|
 | 17 | Constructor | `constructor(address newOwner)` | ✅ | `keccak256(abi.encode(...))` inside → 🚧 (see row 20). |
-| 18 | Modifier | `modifier onlyOwner()` | ❌ | **First-class modifiers** not in EDSL — inline `require(msg.sender == owner)`. |
-| 19 | Inheritance | `contract Morpho is IMorphoStaticTyping` | ❌ | **Inheritance** not supported. Match the ABI structurally. |
+| 18 | Modifier | `modifier onlyOwner()` | ✅ | Precondition-only modifiers are inlined as require prefixes. |
+| 19 | Inheritance | `contract Morpho is IMorphoStaticTyping` | ✅ | Flattened single inheritance is supported. |
 | 20 | Call | `keccak256(abi.encode(DOMAIN_TYPEHASH, block.chainid, address(this)))` | ❌ | **`abi.encode`** not supported. |
 
 ### 1.4 Owner functions
diff --git a/scripts/check_macro_property_test_generation.py b/scripts/check_macro_property_test_generation.py
index afb8030ec..fdb421605 100644
--- a/scripts/check_macro_property_test_generation.py
+++ b/scripts/check_macro_property_test_generation.py
@@ -44,6 +44,23 @@
     # fuzz stubs can pick a target that reverts. Lean/Yul/trust-report tests
     # cover the ABI layout.
     "CallbackABISmoke",
+    # Inheritance regression fixtures are exercised together through their
+    # child contracts in Contracts/Smoke/Helpers.lean.  Standalone generated
+    # Foundry stubs for these bases would not cover the flattening behavior.
+    "ConstructorHygieneBase",
+    "AncestorConstructorBase",
+    "AncestorConstructorMiddle",
+    "ConstructorLocalBase",
+    "InheritedImmutableBase",
+    "InheritedInterfaceBase",
+    "InheritedInterfaceChild",
+    "PayableConstructorBase",
+    "NonpayableVirtualBase",
+    "ViewVirtualBase",
+    "PureVirtualBase",
+    "ModifierParameterCollisionBase",
+    "ModifierLoopCollisionBase",
+    "InheritedOverloadBase",
 }
 
 
diff --git a/scripts/generate_macro_property_tests.py b/scripts/generate_macro_property_tests.py
index b588ade62..e7b457b23 100644
--- a/scripts/generate_macro_property_tests.py
+++ b/scripts/generate_macro_property_tests.py
@@ -14,12 +14,17 @@
 
 import argparse
 import re
-from dataclasses import dataclass, field
+from dataclasses import dataclass, field, replace
 from pathlib import Path
 
 from property_utils import ROOT
 
-CONTRACT_RE = re.compile(r"^\s*verity_contract\s+([A-Za-z_][A-Za-z0-9_]*)\s+where\s*$")
+CONTRACT_RE = re.compile(
+    r"^\s*verity_contract\s+([A-Za-z_][A-Za-z0-9_]*)"
+    r"(?:\s+is\s+([A-Za-z_][A-Za-z0-9_.]*))?\s+where\s*$"
+)
+NAMESPACE_RE = re.compile(r"^\s*namespace\s+([A-Za-z_][A-Za-z0-9_.]*)\s*$")
+END_NAMESPACE_RE = re.compile(r"^\s*end\s+([A-Za-z_][A-Za-z0-9_.]*)\s*$")
 CHECK_CONTRACT_RE = re.compile(r"^\s*#check_contract\s+([A-Za-z_][A-Za-z0-9_]*)\s*$")
 # Optional leading mutability modifiers (`function <modifier>* <name> (...)`,
 # Verity/Macro/Syntax.lean). They sit between `function` and the name, so the
@@ -31,12 +36,20 @@
 _FUNCTION_MODIFIER = (
     r"(?:payable|view|pure|no_external_calls"
     r"|allow_post_interaction_writes|cei_safe|reentrancy_trusted"
-    r"|nonreentrant\([^)]*\))"
+    r"|nonreentrant\([^)]*\)|virtual|override)"
 )
 FUNCTION_RE = re.compile(
-    rf"^\s*function\s+(?:{_FUNCTION_MODIFIER}\s+)*([A-Za-z_][A-Za-z0-9_]*)\s*\(([^)]*)\)\s*:\s*(.+?)\s*:=\s*",
+    rf"^\s*function\s+(?:{_FUNCTION_MODIFIER}\s+)*([A-Za-z_][A-Za-z0-9_]*)\s*\(([^)]*)\)"
+    rf"(?:\s+(?:initializer\([^)]+\)|reinitializer\([^)]+\)))?"
+    rf"(?:\s+with\s+[A-Za-z_][A-Za-z0-9_]*(?:\s*,\s*[A-Za-z_][A-Za-z0-9_]*)*)?"
+    rf"(?:\s+requires\([^)]+\))?"
+    rf"(?:\s+modifies\([^)]+\))?"
+    rf"(?:\s+local_obligations\s*\[[^]]*\])?\s*:\s*(.+?)\s*:=\s*",
 )
-CONSTRUCTOR_RE = re.compile(r"^\s*constructor\s*\(([^)]*)\)\s*:=\s*")
+# Constructor ABI parameters are the first balanced group and cannot themselves
+# contain parentheses in the supported type grammar.  Match only that prefix;
+# the remaining macro syntax may contain arbitrarily nested parent-call terms.
+CONSTRUCTOR_RE = re.compile(r"^\s*constructor\s*\(([^)]*)\)")
 # `_IDENT` captures a user-facing identifier with optional `«…»` raw-identifier
 # escape (verity#1847). The capture group excludes the guillemets so downstream
 # name lookups stay consistent with the compiled CompilationModel param/field
@@ -134,6 +147,7 @@ class FunctionDecl:
     params: tuple[ParamDecl, ...]
     return_type: str
     body: tuple[str, ...] = ()
+    requires_role: bool = False
 
 
 @dataclass(frozen=True)
@@ -155,9 +169,12 @@ class ContractDecl:
     functions: tuple[FunctionDecl, ...]
     storage_slots: dict[str, int]
     source: Path
+    namespace: tuple[str, ...] = ()
+    parent_name: str | None = None
     storage_types: dict[str, str] = field(default_factory=dict)
     transient_slots: frozenset[str] = frozenset()
     newtypes: dict[str, str] = field(default_factory=dict)
+    structs: dict[str, tuple[ParamDecl, ...]] = field(default_factory=dict)
     constants: dict[str, ValueDecl] = field(default_factory=dict)
     immutables: dict[str, ValueDecl] = field(default_factory=dict)
 
@@ -299,6 +316,9 @@ def _resolve_decl_types_in_params(
 def parse_contracts(text: str, source: Path) -> dict[str, ContractDecl]:
     contracts: dict[str, ContractDecl] = {}
     current_name: str | None = None
+    current_namespace: tuple[str, ...] = ()
+    namespace_stack: list[tuple[str, ...]] = []
+    current_parent_name: str | None = None
     current_constructor: ConstructorDecl | None = None
     current_storage_slots: dict[str, int] = {}
     current_transient_slots: set[str] = set()
@@ -338,6 +358,7 @@ def flush_function() -> None:
             params=current_function.params,
             return_type=current_function.return_type,
             body=tuple(current_body),
+            requires_role=current_function.requires_role,
         )
         # Higher-order internal helpers (#1747) are monomorphized away before
         # lowering, so they never reach the external ABI; drop them here to
@@ -348,13 +369,20 @@ def flush_function() -> None:
         current_body = []
 
     def flush_current() -> None:
-        nonlocal current_name, current_constructor, current_storage_slots, current_transient_slots, current_storage_types, current_newtypes, current_structs, current_constants, current_immutables, current_functions, in_types_block, in_storage_block, in_constants_block, in_immutables_block, pending_storage_lines, current_struct_block_comment
+        nonlocal current_name, current_namespace, current_parent_name, current_constructor, current_storage_slots, current_transient_slots, current_storage_types, current_newtypes, current_structs, current_constants, current_immutables, current_functions, in_types_block, in_storage_block, in_constants_block, in_immutables_block, pending_storage_lines, current_struct_block_comment
         if current_name is None:
             return
         flush_struct()
         flush_function()
+        if current_name in contracts:
+            raise ValueError(
+                f"duplicate contract '{current_name}' in {source}; "
+                "namespace-qualified property registry keys are required"
+            )
         contracts[current_name] = ContractDecl(
             name=current_name,
+            namespace=current_namespace,
+            parent_name=current_parent_name,
             constructor=current_constructor,
             functions=tuple(current_functions),
             storage_slots=dict(current_storage_slots),
@@ -362,10 +390,13 @@ def flush_current() -> None:
             storage_types=dict(current_storage_types),
             transient_slots=frozenset(current_transient_slots),
             newtypes=dict(current_newtypes),
+            structs=dict(current_structs),
             constants=dict(current_constants),
             immutables=dict(current_immutables),
         )
         current_name = None
+        current_namespace = ()
+        current_parent_name = None
         current_constructor = None
         current_storage_slots = {}
         current_transient_slots = set()
@@ -383,6 +414,16 @@ def flush_current() -> None:
         pending_storage_lines = []
 
     for line in text.splitlines():
+        namespace_match = NAMESPACE_RE.match(line)
+        if namespace_match:
+            flush_current()
+            namespace_stack.append(tuple(namespace_match.group(1).split(".")))
+            continue
+        end_namespace_match = END_NAMESPACE_RE.match(line)
+        if end_namespace_match and namespace_stack:
+            flush_current()
+            namespace_stack.pop()
+            continue
         if line.strip() == "#guard_msgs in":
             flush_current()
             guard_pending = True
@@ -394,6 +435,8 @@ def flush_current() -> None:
                 continue
             flush_current()
             current_name = cm.group(1)
+            current_namespace = tuple(part for ns in namespace_stack for part in ns)
+            current_parent_name = cm.group(2)
             continue
 
         # Clear guard_pending on any non-blank, non-comment line that isn't
@@ -529,6 +572,7 @@ def flush_current() -> None:
                     _split_params(params_src), current_newtypes, current_structs
                 ),
                 return_type=ret_ty,
+                requires_role=" requires(" in line,
             )
             in_storage_block = False
             in_constants_block = False
@@ -643,7 +687,79 @@ def collect_contracts(paths: list[Path]) -> dict[str, ContractDecl]:
                 prev = all_contracts[name].source
                 raise ValueError(f"duplicate contract '{name}' in {prev} and {contract.source}")
             all_contracts[name] = contract
-    return all_contracts
+    resolved: dict[str, ContractDecl] = {}
+    qualified_contracts = {
+        ".".join((*contract.namespace, contract.name)): contract
+        for contract in all_contracts.values()
+    }
+
+    def resolve(name: str) -> ContractDecl:
+        if name in resolved:
+            return resolved[name]
+        child = all_contracts[name]
+        if child.parent_name is None:
+            resolved[name] = child
+            return child
+        if "." in child.parent_name:
+            parent_decl = qualified_contracts.get(child.parent_name)
+        else:
+            relative_parent = ".".join((*child.namespace, child.parent_name))
+            parent_decl = qualified_contracts.get(relative_parent)
+            if parent_decl is None:
+                parent_decl = qualified_contracts.get(child.parent_name)
+        if parent_decl is None:
+            raise ValueError(
+                f"unresolved parent contract '{child.parent_name}' for '{child.name}'"
+            )
+        parent_key = parent_decl.name
+        parent = resolve(parent_key)
+        merged_newtypes = parent.newtypes | child.newtypes
+        merged_structs = parent.structs | child.structs
+        child_functions = tuple(
+            replace(
+                fn,
+                params=_resolve_decl_types_in_params(fn.params, merged_newtypes, merged_structs),
+                return_type=_resolve_decl_type(fn.return_type, merged_newtypes, merged_structs),
+            )
+            for fn in child.functions
+        )
+        child_constructor = child.constructor
+        if child_constructor is not None:
+            child_constructor = replace(
+                child_constructor,
+                params=_resolve_decl_types_in_params(child_constructor.params, merged_newtypes, merged_structs),
+            )
+        inherited_functions = {
+            (fn.name, tuple(param.lean_type for param in fn.params)): fn
+            for fn in parent.functions
+        }
+        for fn in child_functions:
+            inherited_functions[(fn.name, tuple(param.lean_type for param in fn.params))] = fn
+        merged = replace(
+            child,
+            constructor=child_constructor,
+            functions=tuple(inherited_functions.values()),
+            storage_slots=parent.storage_slots | child.storage_slots,
+            storage_types={
+                field_name: _resolve_decl_type(field_type, merged_newtypes, merged_structs)
+                for field_name, field_type in parent.storage_types.items()
+            }
+            | {
+                field_name: _resolve_decl_type(field_type, merged_newtypes, merged_structs)
+                for field_name, field_type in child.storage_types.items()
+            },
+            transient_slots=parent.transient_slots | child.transient_slots,
+            newtypes=merged_newtypes,
+            structs=merged_structs,
+            constants=parent.constants | child.constants,
+            immutables=parent.immutables | child.immutables,
+        )
+        resolved[name] = merged
+        return merged
+
+    for contract_name in all_contracts:
+        resolve(contract_name)
+    return resolved
 
 
 def _parse_tuple_elements(inner: str) -> list[str]:
@@ -2916,7 +3032,15 @@ def render_contract_test(contract: ContractDecl) -> str:
         encode_args = ", ".join([f'"{sig}"', *call_args]) if call_args else f'"{sig}"'
         fn_camel = _fn_camel(fn.name)
 
-        if _normalize_type(fn.return_type) == "Unit":
+        if fn.requires_role:
+            body = f"""    // Property {idx}: {fn.name} enforces its required role
+    function testAuto_{fn_camel}_RejectsUnauthorizedCaller() public {{
+        vm.prank(address(0x2222));
+        (bool ok,) = target.call(abi.encodeWithSignature({encode_args}));
+        require(!ok, "{fn.name} accepted an unauthorized caller");
+    }}
+"""
+        elif _normalize_type(fn.return_type) == "Unit":
             body = f"""    // Property {idx}: {fn.name} has no unexpected revert
     function testAuto_{fn_camel}_NoUnexpectedRevert() public {{
         vm.prank(alice);
diff --git a/scripts/test_generate_macro_property_tests.py b/scripts/test_generate_macro_property_tests.py
index a4e5a3933..dbc303279 100644
--- a/scripts/test_generate_macro_property_tests.py
+++ b/scripts/test_generate_macro_property_tests.py
@@ -16,6 +16,145 @@
 
 
 class ParseContractsTests(unittest.TestCase):
+    def test_parse_inherited_constructor_with_nested_parent_argument(self) -> None:
+        src = textwrap.dedent(
+            """
+            verity_contract Child is Base where
+              storage
+              constructor (x : Uint256) Base(helper(x)) := do
+                pure ()
+            """
+        )
+        parsed = gen.parse_contracts(src, Path("dummy.lean"))
+        self.assertEqual(parsed["Child"].constructor.params[0].name, "x")
+
+    def test_collect_contracts_rejects_unresolved_parent(self) -> None:
+        with tempfile.TemporaryDirectory() as tmpdir:
+            source = Path(tmpdir) / "Child.lean"
+            source.write_text(
+                "verity_contract Child is Missing where\n  storage\n",
+                encoding="utf-8",
+            )
+            with self.assertRaisesRegex(ValueError, "unresolved parent contract 'Missing'"):
+                gen.collect_contracts([source])
+
+    def test_collect_contracts_rejects_missing_qualified_parent(self) -> None:
+        with tempfile.TemporaryDirectory() as tmpdir:
+            source = Path(tmpdir) / "Contracts.lean"
+            source.write_text(
+                "verity_contract Base where\n  storage\n\n"
+                "verity_contract Child is Other.Base where\n  storage\n",
+                encoding="utf-8",
+            )
+            with self.assertRaisesRegex(ValueError, "unresolved parent contract 'Other.Base'"):
+                gen.collect_contracts([source])
+
+    def test_collect_contracts_rejects_unrelated_namespace_parent_alias(self) -> None:
+        with tempfile.TemporaryDirectory() as tmpdir:
+            child_source = Path(tmpdir) / "Child.lean"
+            child_source.write_text(
+                "namespace A\n"
+                "verity_contract Child is Base where\n  storage\n"
+                "end A\n",
+                encoding="utf-8",
+            )
+            unrelated_source = Path(tmpdir) / "Base.lean"
+            unrelated_source.write_text(
+                "namespace B\n"
+                "verity_contract Base where\n  storage\n"
+                "end B\n",
+                encoding="utf-8",
+            )
+            with self.assertRaisesRegex(ValueError, "unresolved parent contract 'Base'"):
+                gen.collect_contracts([child_source, unrelated_source])
+
+    def test_collect_contracts_falls_back_to_root_parent(self) -> None:
+        with tempfile.TemporaryDirectory() as tmpdir:
+            source = Path(tmpdir) / "Contracts.lean"
+            source.write_text(
+                "verity_contract Base where\n  storage\n\n"
+                "namespace A\n"
+                "verity_contract Child is Base where\n  storage\n"
+                "end A\n",
+                encoding="utf-8",
+            )
+            contracts = gen.collect_contracts([source])
+            self.assertEqual(contracts["Child"].parent_name, "Base")
+
+    def test_collect_contracts_resolves_inherited_alias_in_child_storage(self) -> None:
+        with tempfile.TemporaryDirectory() as tmpdir:
+            source = Path(tmpdir) / "Contracts.lean"
+            source.write_text(
+                textwrap.dedent(
+                    """
+                    verity_contract Base where
+                      types
+                        Amount : Uint256
+                      storage
+
+                    verity_contract Child is Base where
+                      storage
+                        left : Amount := slot 0
+                        right : Amount := slot 1
+
+                      function sum () : Amount := do
+                        let a ← getStorage left
+                        let b ← getStorage right
+                        return (add a b)
+                    """
+                ),
+                encoding="utf-8",
+            )
+            child = gen.collect_contracts([source])["Child"]
+            self.assertEqual(child.storage_types, {"left": "Uint256", "right": "Uint256"})
+            self.assertEqual(gen._sol_type(child.storage_types["left"]), "uint256")
+            self.assertEqual(gen._sol_type(child.storage_types["right"]), "uint256")
+
+    def test_collect_contracts_resolves_alias_in_inherited_parent_storage(self) -> None:
+        with tempfile.TemporaryDirectory() as tmpdir:
+            source = Path(tmpdir) / "Contracts.lean"
+            source.write_text(
+                textwrap.dedent(
+                    """
+                    verity_contract Base where
+                      types
+                        Amount : Uint256
+                      storage
+                        left : Amount := slot 0
+                        right : Amount := slot 1
+
+                    verity_contract Child is Base where
+                      storage
+
+                      function sum () : Amount := do
+                        let a ← getStorage left
+                        let b ← getStorage right
+                        return (add a b)
+                    """
+                ),
+                encoding="utf-8",
+            )
+            child = gen.collect_contracts([source])["Child"]
+            self.assertEqual(child.storage_types, {"left": "Uint256", "right": "Uint256"})
+            self.assertEqual(gen._sol_type(child.storage_types["left"]), "uint256")
+            self.assertEqual(gen._sol_type(child.storage_types["right"]), "uint256")
+
+    def test_parse_contracts_rejects_duplicate_unqualified_names(self) -> None:
+        src = textwrap.dedent(
+            """
+            namespace A
+            verity_contract Base where
+              storage
+            end A
+            namespace B
+            verity_contract Base where
+              storage
+            end B
+            """
+        )
+        with self.assertRaisesRegex(ValueError, "duplicate contract 'Base'"):
+            gen.parse_contracts(src, Path("dummy.lean"))
+
     def test_parse_two_contracts(self) -> None:
         src = textwrap.dedent(
             """
@@ -47,6 +186,23 @@ def test_parse_params(self) -> None:
         out = gen._split_params("to : Address, amount : Uint256")
         self.assertEqual([(p.name, p.lean_type) for p in out], [("to", "Address"), ("amount", "Uint256")])
 
+    def test_parse_function_post_parameter_clauses(self) -> None:
+        src = textwrap.dedent(
+            """
+            verity_contract Guarded where
+              storage
+                owner : Address := slot 0
+
+              function audit (value : Uint256) initializer(owner) with onlyOwner requires(owner) modifies(owner) local_obligations [safe := proved "ok"] : Uint256 := do
+                return value
+            """
+        )
+        parsed = gen.parse_contracts(src, Path("dummy.lean"))
+        fn = parsed["Guarded"].functions[0]
+        self.assertEqual(fn.name, "audit")
+        self.assertEqual(fn.return_type, "Uint256")
+        self.assertTrue(fn.requires_role)
+
     def test_parse_inline_struct_param_as_tuple(self) -> None:
         src = textwrap.dedent(
             """
@@ -271,6 +427,26 @@ def test_parse_contracts_skips_higher_order_helpers(self) -> None:
         rendered = gen.render_contract_test(parsed["FunctionPointerParamSmoke"])
         self.assertNotIn("apply(", rendered)
 
+    def test_role_negative_property_uses_distinct_unauthorized_caller(self) -> None:
+        src = textwrap.dedent(
+            """
+            verity_contract RoleConstructorSmoke where
+              storage
+                owner : Address := slot 0
+
+              constructor (initialOwner : Address) := do
+                setStorageAddr owner initialOwner
+
+              function guarded () requires(owner) : Unit := do
+                pure ()
+            """
+        )
+        contract = gen.parse_contracts(src, gen.ROOT / "Contracts/Smoke.lean")["RoleConstructorSmoke"]
+        rendered = gen.render_contract_test(contract)
+        self.assertIn("abi.encode(alice)", rendered)
+        self.assertIn("vm.prank(address(0x2222));", rendered)
+        self.assertNotIn("vm.prank(alice);\n        (bool ok,) = target.call", rendered)
+
 
 class RenderTests(unittest.TestCase):
     def test_render_unit_and_non_unit_tests(self) -> None: