diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml
index 9ad724008..1e579b269 100644
--- a/.github/workflows/verify.yml
+++ b/.github/workflows/verify.yml
@@ -738,6 +738,7 @@ jobs:
           set -euo pipefail
           smoke_modules=(
             Contracts.BytesEqSmoke
+            Contracts.Smoke.EnumFeatureTest
             Contracts.Smoke.ImmutableSmoke
             Contracts.Smoke.LowLevelTryCatchSmoke
             Contracts.Smoke.SelfBalanceSmoke
@@ -783,6 +784,7 @@ jobs:
           set -euo pipefail
           smoke_modules=(
             Contracts.BytesEqSmoke
+            Contracts.Smoke.EnumFeatureTest
             Contracts.Smoke.ImmutableSmoke
             Contracts.Smoke.LowLevelTryCatchSmoke
             Contracts.Smoke.SelfBalanceSmoke
diff --git a/Compiler/ABI.lean b/Compiler/ABI.lean
index d9e8e756d..465705196 100644
--- a/Compiler/ABI.lean
+++ b/Compiler/ABI.lean
@@ -27,6 +27,7 @@ private def abiTypeString : ParamType → String
   | .array t => abiTypeString t ++ "[]"
   | .fixedArray t n => abiTypeString t ++ "[" ++ toString n ++ "]"
   | .adt _ _ => "tuple"  -- ADTs are ABI-encoded as static tuples
+  | .newtypeOf "__verity_enum" _ => "uint8"
   | .newtypeOf _ baseType => abiTypeString baseType  -- Erased to base type
 
 -- Uses `fieldTypeToParamType` from CompilationModel (shared, not duplicated).
diff --git a/Compiler/CompilationModel/AbiHelpers.lean b/Compiler/CompilationModel/AbiHelpers.lean
index f53439dba..49e33fd2b 100644
--- a/Compiler/CompilationModel/AbiHelpers.lean
+++ b/Compiler/CompilationModel/AbiHelpers.lean
@@ -63,6 +63,7 @@ mutual
     | ParamType.adt _name maxFields =>
         -- ABI-encoded as static tuple: (uint8, uint256, ..., uint256)
         "(" ++ String.intercalate "," ("uint8" :: List.replicate maxFields "uint256") ++ ")"
+    | ParamType.newtypeOf "__verity_enum" _ => "uint8"
     | ParamType.newtypeOf _ baseType => paramTypeToSolidityString baseType  -- Erased to base type
 
   private def paramTypeListToSolidityStrings : List ParamType → List String
diff --git a/Compiler/CompilationModel/ValidationEvents.lean b/Compiler/CompilationModel/ValidationEvents.lean
index 514fc29c3..175ac2cb7 100644
--- a/Compiler/CompilationModel/ValidationEvents.lean
+++ b/Compiler/CompilationModel/ValidationEvents.lean
@@ -9,6 +9,12 @@ import Compiler.CompilationModel.ScopeValidation
 
 namespace Compiler.CompilationModel
 
+def eventParamTypeCompatible (actual expected : ParamType) : Bool :=
+  actual == expected ||
+    match actual, expected with
+    | .newtypeOf "__verity_enum" .uint256, .uint8 => true
+    | _, _ => false
+
 def customErrorRequiresDirectParamRef : ParamType → Bool
   | ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.uint16
   | ParamType.uintN _ | ParamType.intN _ | ParamType.bytesN _
@@ -104,7 +110,7 @@ def validateEventArgShapesNode (fnName : String) (params : List Param)
         | Expr.param name =>
             match findParamType params name with
             | some ty =>
-                if ty != eventParam.ty then
+                if !eventParamTypeCompatible ty eventParam.ty then
                   throw s!"Compilation error: function '{fnName}' event '{eventName}' param '{eventParam.name}' expects {repr eventParam.ty}, got parameter '{name}' of type {repr ty} ({issue586Ref})."
             | none =>
                 throw s!"Compilation error: function '{fnName}' event '{eventName}' references unknown parameter '{name}' ({issue586Ref})."
diff --git a/Contracts/Common.lean b/Contracts/Common.lean
index 4289def1f..8d8fb3673 100644
--- a/Contracts/Common.lean
+++ b/Contracts/Common.lean
@@ -168,7 +168,7 @@ macro_rules
           $(Lean.quote (toString errorName.getId))
           [ $[$encodedArgs],* ])
   | `(doElem| panic($code:term)) => do
-      let panicFn := Lean.mkIdentFrom code `_root_.Contracts.revertPanic
+      let panicFn := Lean.mkIdentFrom code `_root_.Contracts.revertPanicAs
       `(doElem| $panicFn:ident $code)
   | `(requireSomeUintError $optExpr:term $errorName:ident($args,*)) => do
       let requireFn := Lean.mkIdentFrom errorName `_root_.Contracts.requireSomeUintCustomError
@@ -317,6 +317,12 @@ decimal panic code; on-chain the compiled contract reverts with the ABI-encoded
 def revertPanic (code : Uint256) : Contract Unit :=
   revertCustomError "Panic" [CustomErrorArg.encode code]
 
+/-- Polymorphic executable counterpart used when a terminating panic appears in
+an expression-valued generated body. Keep `revertPanic`'s public signature
+source-compatible for direct callers. -/
+def revertPanicAs {α : Type} (code : Uint256) : Contract α :=
+  fun state => ContractResult.revert s!"Panic({code.val})" state
+
 private def wordToSigned (value : Uint256) : Int :=
   (toInt256 value : Int)
 
diff --git a/Contracts/Smoke/EnumFeatureTest.lean b/Contracts/Smoke/EnumFeatureTest.lean
new file mode 100644
index 000000000..eae5fd0bc
--- /dev/null
+++ b/Contracts/Smoke/EnumFeatureTest.lean
@@ -0,0 +1,242 @@
+import Contracts.Common
+
+namespace Contracts.Smoke.EnumFeatureTest
+
+open Compiler.CompilationModel
+open Verity hiding pure bind
+open Verity.EVM.Uint256
+
+verity_contract MacroEnumUsage where
+  enums
+    enum Status { Pending, Active, Closed }
+
+  storage
+    status : Status := slot 0
+    statuses : Uint256 → Status := slot 1
+
+  errors
+    error InvalidStatus(Status)
+
+  event_defs
+    event StatusChanged(@indexed previous : Status, current : Status)
+
+  function identity (value : Status) : Status := do
+    return value
+
+  function active () : Status := do
+    return Status.Active
+
+  function castStatus (value : Uint256) : Status := do
+    let casted ← Status(value)
+    return casted
+
+  function setStatus (value : Status) : Unit := do
+    setStorage status value
+
+  function announceStatus (value : Status) : Unit := do
+    emit "StatusChanged" [value, value]
+
+  function getStatus () : Status := do
+    let value ← getStorage status
+    return value
+
+  function setStatusAt (key : Uint256, value : Status) : Unit := do
+    setMappingUint statuses key value
+
+  function getStatusAt (key : Uint256) : Status := do
+    let value ← getMappingUint statuses key
+    return value
+
+def identityUsesUint8Abi : Bool :=
+  (match MacroEnumUsage.identity_model.params with
+   | [{ ty, .. }] => paramTypeToSolidityString ty == "uint8"
+   | _ => false) &&
+    MacroEnumUsage.identity_model.returns == [ParamType.uint8]
+
+example : identityUsesUint8Abi = true := by native_decide
+
+def eventAndErrorUseUint8Abi : Bool :=
+  MacroEnumUsage.spec.events.any (fun ev =>
+    match ev with
+    | { name := "StatusChanged", params :=
+        [{ name := "previous", ty := ParamType.uint8, kind := EventParamKind.indexed },
+         { name := "current", ty := ParamType.uint8, kind := EventParamKind.unindexed }] } => true
+    | _ => false) &&
+  MacroEnumUsage.spec.errors.any (fun err =>
+    match err with
+    | { name := "InvalidStatus", params := [ParamType.uint8] } => true
+    | _ => false)
+
+example : eventAndErrorUseUint8Abi = true := by native_decide
+
+def memberConstantIsOne : Bool := MacroEnumUsage.Status.Active == 1
+
+example : memberConstantIsOne = true := by native_decide
+
+def castAcceptsLastMember : Bool :=
+  match MacroEnumUsage.castStatus 2 defaultState with
+  | .success value _ => value == 2
+  | .revert _ _ => false
+
+example : castAcceptsLastMember = true := by native_decide
+
+def castRejectsOutOfRange : Bool :=
+  match MacroEnumUsage.castStatus 3 defaultState with
+  | .success _ _ => false
+  | .revert _ _ => true
+
+example : castRejectsOutOfRange = true := by native_decide
+
+def enumParamRejectsOutOfRange : Bool :=
+  match MacroEnumUsage.identity 3 defaultState with
+  | .success _ _ => false
+  | .revert _ _ => true
+
+example : enumParamRejectsOutOfRange = true := by native_decide
+
+/--
+error: ite requires matching branch types, got Verity.Macro.ValueType.enum "Status" 3 and Verity.Macro.ValueType.uint256
+-/
+#guard_msgs in
+verity_contract EnumIteRawWordRejected where
+  enums
+    enum Status { Pending, Active, Closed }
+
+  storage
+    status : Status := slot 0
+
+  function bad (cond : Bool) : Unit := do
+    setStorage status (ite cond Status.Active 999)
+
+/--
+error: typed interface call 'IStatus.current' uses an enum-valued return; checked enum decoding from untrusted external returndata is not implemented
+-/
+#guard_msgs in
+verity_contract TypedInterfaceEnumReturnRejected where
+  enums
+    enum Status { Pending, Active, Closed }
+
+  storage
+
+  interfaces
+    interface IStatus where
+      function current() view returns (Status)
+    end
+
+  function bad (source : IStatus) : Status := do
+    let value ← source.current
+    return value
+
+/-- -/
+#guard_msgs in
+verity_contract EnumOperatorsSupported where
+  enums
+    enum Status { Pending, Active }
+  storage
+  function isActive (value : Status) : Bool := do
+    return value == Status.Active
+  function nextOrdinal (value : Status) : Uint256 := do
+    return toUint256 value + 1
+
+/--
+error: event 'StatusChanged' parameter 'current' expects Verity.Macro.ValueType.enum "Status" 2, got Verity.Macro.ValueType.enum "Role" 3
+-/
+#guard_msgs in
+verity_contract CrossEnumEventRejected where
+  enums
+    enum Status { Pending, Active }
+    enum Role { Guest, Member, Admin }
+
+  storage
+
+  event_defs
+    event StatusChanged(current : Status)
+
+  function bad (role : Role) : Unit := do
+    emit "StatusChanged" [role]
+
+/--
+error: setStorage value expects Verity.Macro.ValueType.enum "Status" 3, got Verity.Macro.ValueType.uint256
+-/
+#guard_msgs in
+verity_contract RawEnumStorageLiteralRejected where
+  enums
+    enum Status { Pending, Active, Closed }
+  storage
+    status : Status := slot 0
+  function bad () : Unit := do
+    setStorage status 1
+
+/--
+error: return from 'bad' expects Verity.Macro.ValueType.enum "Status" 3, got Verity.Macro.ValueType.uint256
+-/
+#guard_msgs in
+verity_contract RawEnumReturnLiteralRejected where
+  enums
+    enum Status { Pending, Active, Closed }
+  storage
+  function bad () : Status := do
+    return 1
+
+/--
+error: assignment to 'value' expects Verity.Macro.ValueType.enum "Status" 3, got Verity.Macro.ValueType.uint256
+-/
+#guard_msgs in
+verity_contract RawEnumLocalAssignmentRejected where
+  enums
+    enum Status { Pending, Active, Closed }
+  storage
+  function bad () : Status := do
+    let mut value := Status.Pending
+    value := 1
+    return value
+
+/--
+error: equality is currently supported only for Bool, matching bytes/string params, and word-like values (Uint256, Int256, Uint8, Address, Bytes32); got Verity.Macro.ValueType.enum "Status" 2 and Verity.Macro.ValueType.enum "Role" 2
+-/
+#guard_msgs in
+verity_contract CrossEnumEqualityRejected where
+  enums
+    enum Status { Pending, Active }
+    enum Role { Guest, Admin }
+  storage
+  function bad () : Bool := do
+    return Status.Active == Role.Admin
+
+/--
+error: equality is currently supported only for Bool, matching bytes/string params, and word-like values (Uint256, Int256, Uint8, Address, Bytes32); got Verity.Macro.ValueType.enum "Status" 2 and Verity.Macro.ValueType.uint256
+-/
+#guard_msgs in
+verity_contract EnumWordEqualityRejected where
+  enums
+    enum Status { Pending, Active }
+  storage
+  function bad (word : Uint256) : Bool := do
+    return Status.Active == word
+
+/--
+error: word arithmetic requires `toUint256` before applying word operators to enum values; got Verity.Macro.ValueType.enum "Status" 2 and Verity.Macro.ValueType.uint256
+-/
+#guard_msgs in
+verity_contract EnumArithmeticRejected where
+  enums
+    enum Status { Pending, Active }
+  storage
+  function bad (status : Status) : Uint256 := do
+    return status + 1
+
+/--
+error: bitwise not requires `toUint256` before applying word operators to enum values; got Verity.Macro.ValueType.enum "Status" 2
+-/
+#guard_msgs in
+verity_contract EnumUnaryWordOperatorRejected where
+  enums
+    enum Status { Pending, Active }
+  storage
+  function bad (status : Status) : Uint256 := do
+    return bitNot status
+
+/-- Expose the contract model at the canonical module-level name used by the compiler CLI. -/
+def spec : CompilationModel := MacroEnumUsage.spec
+
+end Contracts.Smoke.EnumFeatureTest
diff --git a/Verity/Macro/Bridge.lean b/Verity/Macro/Bridge.lean
index 82e96c278..5dee992a2 100644
--- a/Verity/Macro/Bridge.lean
+++ b/Verity/Macro/Bridge.lean
@@ -247,12 +247,14 @@ private def mkFieldFrameConjunct (field : StorageFieldDecl) : CommandElabM Term
   | .dynamicArray _ =>
       -- storageArray slot is unchanged
       `(s'.storageArray $slotLit = s.storageArray $slotLit)
-  | .mappingAddressToUint256 | .mappingStruct .address _ =>
+  | .mappingAddressToUint256 | .mappingAddressToEnum _ _ | .mappingStruct .address _ =>
       -- ∀ k, s'.storageMap slot k = s.storageMap slot k
       `(∀ k, s'.storageMap $slotLit k = s.storageMap $slotLit k)
-  | .mappingUintToUint256 | .mappingStruct .uint256 _ =>
+  | .mappingUintToUint256 | .mappingUintToEnum _ _ | .mappingStruct .uint256 _ =>
       `(∀ k, s'.storageMapUint $slotLit k = s.storageMapUint $slotLit k)
-  | .mappingStruct .bytes32 _ | .mappingChain _ | .mapping2AddressToAddressToUint256 | .mappingStruct2 _ _ _ =>
+  | .mappingStruct .bytes32 _ | .mappingChain _ | .mappingChainEnum _ _ _
+    | .mapping2AddressToAddressToUint256 | .mapping2AddressToAddressToEnum _ _
+    | .mappingStruct2 _ _ _ =>
       -- These shapes compile to hashed `storage` slots rather than the legacy
       -- storageMap mirrors, so the conservative frame predicate must constrain
       -- the hashed storage surface.
diff --git a/Verity/Macro/Elaborate.lean b/Verity/Macro/Elaborate.lean
index f7e02efaf..716e9afa5 100644
--- a/Verity/Macro/Elaborate.lean
+++ b/Verity/Macro/Elaborate.lean
@@ -88,7 +88,7 @@ def elabVerityContract : CommandElab := fun stx => do
   validateConstantDeclsPublic constDecls
   validateImmutableDeclsPublic fields constDecls immutableDecls ctor
   validateExternalDeclsPublic externalDecls
-  validateFunctionDeclsPublic fields errorDecls constDecls immutableDecls externalDecls ctor modifiers functions
+  validateFunctionDeclsPublic fields errorDecls eventDecls constDecls immutableDecls externalDecls ctor modifiers functions
 
   elabCommand (← `(namespace $contractName))
   try
diff --git a/Verity/Macro/ExternalCalls.lean b/Verity/Macro/ExternalCalls.lean
index f3759cca5..8ddea7d91 100644
--- a/Verity/Macro/ExternalCalls.lean
+++ b/Verity/Macro/ExternalCalls.lean
@@ -59,6 +59,7 @@ def parseExternal
 private def externalExecutableWordType? : ValueType → Bool
   | .uint256 | .int256 | .uint8 | .uint16 | .uintN _ | .intN _ | .bytesN _
   | .address | .bytes32 | .bool => true
+  | .enum _ _ => true
   | .newtype _ baseType => externalExecutableWordType? baseType
   | _ => false
 
@@ -75,11 +76,21 @@ private partial def externalExecutableReturnType? : ValueType → Bool
   | .newtype _ baseType => externalExecutableReturnType? baseType
   | ty => externalExecutableWordType? ty
 
+private partial def containsEnumReturnType : ValueType → Bool
+  | .enum _ _ => true
+  | .tuple tys => tys.any containsEnumReturnType
+  | .fixedArray ty _ | .newtype _ ty => containsEnumReturnType ty
+  | .struct _ fields => fields.any (fun field => containsEnumReturnType field.snd)
+  | _ => false
+
 def validateExternalExecutableType
     (extIdent : Ident)
     (extName : String)
     (ty : ValueType)
     (role : String) : CommandElabM Unit := do
+  if containsEnumReturnType ty then
+    throwErrorAt extIdent
+      s!"linked external '{extName}' uses an enum-valued {role}; checked enum decoding from untrusted external returndata is not implemented"
   if !externalExecutableReturnType? ty then
     throwErrorAt extIdent
       s!"linked external '{extName}' uses unsupported {role} type; executable externalCall currently supports only word-like values and static ABI composites of word-like values"
diff --git a/Verity/Macro/Functions.lean b/Verity/Macro/Functions.lean
index 578faabdf..c61aec9a4 100644
--- a/Verity/Macro/Functions.lean
+++ b/Verity/Macro/Functions.lean
@@ -24,6 +24,7 @@ partial def valueTypeSignatureComponent : ValueType → String
   | .fixedArray ty size => "fixed_array_" ++ toString size ++ "_" ++ valueTypeSignatureComponent ty
   | .tuple tys => "tuple" ++ toString tys.length ++ "_" ++ String.intercalate "__" (tys.map valueTypeSignatureComponent)
   | .newtype name baseType => "newtype_" ++ name ++ "_" ++ valueTypeSignatureComponent baseType
+  | .enum name _ => "enum_" ++ name
   | .struct name fields =>
       "struct_" ++ name ++ "_" ++
         String.intercalate "__" (fields.map (fun field => field.fst ++ "_" ++ valueTypeSignatureComponent field.snd))
@@ -34,6 +35,7 @@ def functionSignatureKey (fn : FunctionDecl) : String :=
 
 partial def valueTypeAbiSignatureComponent : ValueType → String
   | .newtype _ baseType => valueTypeAbiSignatureComponent baseType
+  | .enum _ _ => "scalar_uint8"
   | .array ty => "array_" ++ valueTypeAbiSignatureComponent ty
   | .fixedArray ty size => "fixed_array_" ++ toString size ++ "_" ++ valueTypeAbiSignatureComponent ty
   | .tuple tys => "tuple" ++ toString tys.length ++ "_" ++ String.intercalate "__" (tys.map valueTypeAbiSignatureComponent)
diff --git a/Verity/Macro/Interfaces.lean b/Verity/Macro/Interfaces.lean
index be1205f32..78c5cf5ae 100644
--- a/Verity/Macro/Interfaces.lean
+++ b/Verity/Macro/Interfaces.lean
@@ -27,6 +27,7 @@ partial def valueTypeToSolidityString : ValueType → String
   | .struct _ fields =>
       "(" ++ String.intercalate "," (fields.map (fun field => valueTypeToSolidityString field.snd)) ++ ")"
   | .newtype _ baseType => valueTypeToSolidityString baseType
+  | .enum _ _ => "uint8"
   | .adt name _ => name
   | .unit => "()"
 
diff --git a/Verity/Macro/Internal.lean b/Verity/Macro/Internal.lean
index 6915cb257..728178cf9 100644
--- a/Verity/Macro/Internal.lean
+++ b/Verity/Macro/Internal.lean
@@ -1,6 +1,7 @@
 import Lean
 import Compiler.CompilationModel.InternalNaming
 import Verity.Macro.Types
+import Verity.Macro.Syntax
 
 namespace Verity.Macro
 
@@ -10,7 +11,10 @@ open Lean.Elab.Command
 def localFunctionAppSyntax?
     (stx : Term) : Option (String × Array Term) :=
   let stx := stripParens stx
-  match stx.raw with
+  match stx with
+  | `(term| $fn:ident($[$args:term],*)) =>
+      some (toString fn.getId, args)
+  | _ => match stx.raw with
   | .node _ `Lean.Parser.Term.app args =>
       match args.getD 0 Syntax.missing with
       | .ident _ raw _ _ =>
diff --git a/Verity/Macro/Storage.lean b/Verity/Macro/Storage.lean
index dfeb69e29..b08bbcf35 100644
--- a/Verity/Macro/Storage.lean
+++ b/Verity/Macro/Storage.lean
@@ -52,6 +52,7 @@ def storageTypeFromSyntax
   let rec storageStructMemberElementWords (memberName : String) : ValueType → CommandElabM Nat
     | .uint256 | .int256 | .uint16 | .address | .bool | .bytes32 => pure 1
     | .newtype _ baseType => storageStructMemberElementWords memberName baseType
+    | .enum _ _ => pure 1
     | .fixedArray elemTy size => do
         let elemWords ← storageStructMemberElementWords memberName elemTy
         pure (elemWords * size)
@@ -64,6 +65,8 @@ def storageTypeFromSyntax
     match memberTy with
     | .newtype _ baseType =>
         expandStructMemberDecl memberPrefix baseOffset baseType packed
+    | .enum _ _ =>
+        pure [{ name := memberPrefix, ty := memberTy, wordOffset := baseOffset, packed := packed }]
     | .fixedArray elemTy size => do
         if packed.isSome then
           throwErrorAt ty s!"mapping struct fixed-array member '{memberPrefix}' cannot be packed"
@@ -94,16 +97,23 @@ def storageTypeFromSyntax
 
   let (arrowArgs, arrowResult) ← collectArrowChainTypes ty
   if !arrowArgs.isEmpty then
-    match arrowResult with
-    | `(term| Uint256) =>
+    match (← valueTypeFromSyntax newtypes structDecls adtDecls arrowResult) with
+    | .uint256 =>
         let keyTypes ← arrowArgs.mapM keyTypeFromSyntax
         match keyTypes with
         | [.address] => pure .mappingAddressToUint256
         | [.uint256] => pure .mappingUintToUint256
         | [.address, .address] => pure .mapping2AddressToAddressToUint256
         | _ => pure (.mappingChain keyTypes)
+    | .enum name memberCount =>
+        let keyTypes ← arrowArgs.mapM keyTypeFromSyntax
+        match keyTypes with
+        | [.address] => pure (.mappingAddressToEnum name memberCount)
+        | [.uint256] => pure (.mappingUintToEnum name memberCount)
+        | [.address, .address] => pure (.mapping2AddressToAddressToEnum name memberCount)
+        | _ => pure (.mappingChainEnum keyTypes name memberCount)
     | _ =>
-        throwErrorAt ty "unsupported mapping value type; expected Uint256"
+        throwErrorAt ty "unsupported mapping value type; expected Uint256 or an enum"
   else
     match ty with
   | `(term| MappingStruct($keyTy:term,[ $[$members:verityStructMember],* ])) =>
@@ -132,14 +142,24 @@ def modelMappingKeyTypeTerm : MappingKeyType → CommandElabM Term
 
 def storageTypeMappingKeyTypes? : StorageType → Option (List MappingKeyType)
   | .mappingAddressToUint256 => some [.address]
+  | .mappingAddressToEnum _ _ => some [.address]
   | .mapping2AddressToAddressToUint256 => some [.address, .address]
+  | .mapping2AddressToAddressToEnum _ _ => some [.address, .address]
   | .mappingUintToUint256 => some [.uint256]
+  | .mappingUintToEnum _ _ => some [.uint256]
   | .mappingChain keyTypes => some keyTypes
+  | .mappingChainEnum keyTypes _ _ => some keyTypes
   | _ => none
 
 def storageTypeMappingDepth? (ty : StorageType) : Option Nat :=
   storageTypeMappingKeyTypes? ty |>.map List.length
 
+def storageTypeMappingValueType? : StorageType → Option ValueType
+  | .mappingAddressToEnum name memberCount | .mapping2AddressToAddressToEnum name memberCount
+    | .mappingUintToEnum name memberCount | .mappingChainEnum _ name memberCount =>
+      some (.enum name memberCount)
+  | _ => none
+
 def storageKeyTypeContractTerm : MappingKeyType → CommandElabM Term
   | .address => `(Address)
   | .uint256 => `(Uint256)
@@ -153,7 +173,7 @@ def modelStructMemberTerm (member : StructMemberDecl) : CommandElabM Term := do
         `(some { offset := $(natTerm offset), width := $(natTerm width) })
   let memberTypeTerm ←
     match member.ty with
-    | .uint256 | .int256 | .uint8 =>
+    | .uint256 | .int256 | .uint8 | .enum _ _ =>
         `(Compiler.CompilationModel.StructMemberType.uint256)
     | .uint16 =>
         `(Compiler.CompilationModel.StructMemberType.uint16)
@@ -193,6 +213,7 @@ def modelFieldTypeTerm (ty : StorageType) : CommandElabM Term :=
         "top-level named struct storage fields are not supported yet (#1758); flatten the struct into explicit scalar storage fields with fixed slots, or use MappingStruct/MappingStruct2 for struct-valued mappings"
   | .scalar .unit => throwError "storage fields cannot be Unit"
   | .scalar (.newtype _ baseType) => modelFieldTypeTerm (.scalar baseType)  -- Erased to base type
+  | .scalar (.enum _ _) => `(Compiler.CompilationModel.FieldType.uint256)
   | .scalar (.adt name maxFields) =>
       `(Compiler.CompilationModel.FieldType.adt $(Lean.quote name) $(Lean.quote maxFields))
   | .dynamicArray .uint256 => `(Compiler.CompilationModel.FieldType.dynamicArray Compiler.CompilationModel.StorageArrayElemType.uint256)
@@ -203,18 +224,33 @@ def modelFieldTypeTerm (ty : StorageType) : CommandElabM Term :=
   | .mappingAddressToUint256 =>
       `(Compiler.CompilationModel.FieldType.mappingTyped
           (Compiler.CompilationModel.MappingType.simple Compiler.CompilationModel.MappingKeyType.address))
+  | .mappingAddressToEnum _ _ =>
+      `(Compiler.CompilationModel.FieldType.mappingTyped
+          (Compiler.CompilationModel.MappingType.simple Compiler.CompilationModel.MappingKeyType.address))
   | .mapping2AddressToAddressToUint256 =>
       `(Compiler.CompilationModel.FieldType.mappingTyped
           (Compiler.CompilationModel.MappingType.nested
             Compiler.CompilationModel.MappingKeyType.address
             Compiler.CompilationModel.MappingKeyType.address))
+  | .mapping2AddressToAddressToEnum _ _ =>
+      `(Compiler.CompilationModel.FieldType.mappingTyped
+          (Compiler.CompilationModel.MappingType.nested
+            Compiler.CompilationModel.MappingKeyType.address
+            Compiler.CompilationModel.MappingKeyType.address))
   | .mappingUintToUint256 =>
       `(Compiler.CompilationModel.FieldType.mappingTyped
           (Compiler.CompilationModel.MappingType.simple Compiler.CompilationModel.MappingKeyType.uint256))
+  | .mappingUintToEnum _ _ =>
+      `(Compiler.CompilationModel.FieldType.mappingTyped
+          (Compiler.CompilationModel.MappingType.simple Compiler.CompilationModel.MappingKeyType.uint256))
   | .mappingChain keyTypes => do
       let keyTypeTerms := (← keyTypes.mapM modelMappingKeyTypeTerm).toArray
       `(Compiler.CompilationModel.FieldType.mappingTyped
           (Compiler.CompilationModel.MappingType.chain [ $[$keyTypeTerms],* ]))
+  | .mappingChainEnum keyTypes _ _ => do
+      let keyTypeTerms := (← keyTypes.mapM modelMappingKeyTypeTerm).toArray
+      `(Compiler.CompilationModel.FieldType.mappingTyped
+          (Compiler.CompilationModel.MappingType.chain [ $[$keyTypeTerms],* ]))
   | .mappingStruct keyType members => do
       let keyTypeTerm ← modelMappingKeyTypeTerm keyType
       let memberTerms := (← members.mapM modelStructMemberTerm).toArray
diff --git a/Verity/Macro/Syntax.lean b/Verity/Macro/Syntax.lean
index 5937fdfe9..d06e273e1 100644
--- a/Verity/Macro/Syntax.lean
+++ b/Verity/Macro/Syntax.lean
@@ -4,6 +4,10 @@ namespace Verity.Macro
 
 open Lean
 
+syntax:max ident noWs "(" sepBy(term, ",") ")" : term
+macro_rules
+  | `($fn:ident($[$args:term],*)) => `($fn $args*)
+
 declare_syntax_cat verityStorageField
 declare_syntax_cat verityStorageItem
 declare_syntax_cat verityStorageStructMember
@@ -27,6 +31,7 @@ declare_syntax_cat verityInitGuard
 declare_syntax_cat verityModifies
 declare_syntax_cat verityRequiresRole
 declare_syntax_cat verityNewtype
+declare_syntax_cat verityEnumDecl
 declare_syntax_cat verityStructDecl
 declare_syntax_cat verityAdtVariant
 declare_syntax_cat verityAdtDecl
@@ -99,6 +104,7 @@ syntax "reentrancy_trusted" : verityMutability
 syntax "modifies(" sepBy1(ident, ",") ")" : verityModifies
 syntax "requires(" ident ")" : verityRequiresRole
 syntax ident " : " term:max : verityNewtype
+syntax "enum " ident " {" sepBy1(ident, ",") "}" : verityEnumDecl
 syntax "struct " ident " where " sepBy1(verityParam, ",") : verityStructDecl
 syntax "| " ident "(" sepBy(verityParam, ",") ")" : verityAdtVariant
 syntax "| " ident : verityAdtVariant
@@ -192,6 +198,7 @@ syntax (name := verityIntrinsicCmd)
 syntax (name := verityContractCmd)
   "verity_contract " ident " where "
   ("types " verityNewtype+)?
+  ("enums " verityEnumDecl+)?
   ("inductive " verityAdtDecl+)?
   (verityNamespaceSpec)?
   "storage " verityStorageItem*
diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index f73062dab..4aa544978 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -48,46 +48,59 @@ private def translateCustomErrorArgExprs
     normalizeTranslatedExprForType expectedTy arg raw
 
 mutual
+private partial def returnTypeContainsEnum : ValueType → Bool
+  | .enum _ _ => true
+  | .array ty | .fixedArray ty _ | .newtype _ ty => returnTypeContainsEnum ty
+  | .tuple tys => tys.any returnTypeContainsEnum
+  | .struct _ fields => fields.any (fun field => returnTypeContainsEnum field.snd)
+  | _ => false
+
 private partial def validateDoSeqExprTypes
     (ownerName : String)
+    (returnTy : ValueType)
     (fields : Array StorageFieldDecl)
     (constDecls : Array ConstantDecl)
     (immutableDecls : Array ImmutableDecl)
     (externalDecls : Array ExternalDecl)
     (errorDecls : Array ErrorDecl)
+    (eventDecls : Array EventDecl)
     (functions : Array FunctionDecl)
     (params : Array ParamDecl)
     (locals : Array TypedLocal)
     (doSeq : DoSeq) : CommandElabM Unit := do
   match doSeq with
   | `(doSeq| $[$elems:doElem]*) =>
-      let _ ← validateDoElemsExprTypes ownerName fields constDecls immutableDecls externalDecls errorDecls functions params locals elems
+      let _ ← validateDoElemsExprTypes ownerName returnTy fields constDecls immutableDecls externalDecls errorDecls eventDecls functions params locals elems
       pure ()
   | _ => throwErrorAt doSeq "unsupported branch body; expected do-sequence"
 
 private partial def validateDoElemsExprTypes
     (ownerName : String)
+    (returnTy : ValueType)
     (fields : Array StorageFieldDecl)
     (constDecls : Array ConstantDecl)
     (immutableDecls : Array ImmutableDecl)
     (externalDecls : Array ExternalDecl)
     (errorDecls : Array ErrorDecl)
+    (eventDecls : Array EventDecl)
     (functions : Array FunctionDecl)
     (params : Array ParamDecl)
     (locals : Array TypedLocal)
     (elems : Array (TSyntax `doElem)) : CommandElabM (Array TypedLocal) := do
   let mut branchLocals := locals
   for elem in elems do
-    branchLocals ← validateDoElemExprTypes ownerName fields constDecls immutableDecls externalDecls errorDecls functions params branchLocals elem
+    branchLocals ← validateDoElemExprTypes ownerName returnTy fields constDecls immutableDecls externalDecls errorDecls eventDecls functions params branchLocals elem
   pure branchLocals
 
 private partial def validateDoElemExprTypes
     (ownerName : String)
+    (returnTy : ValueType)
     (fields : Array StorageFieldDecl)
     (constDecls : Array ConstantDecl)
     (immutableDecls : Array ImmutableDecl)
     (externalDecls : Array ExternalDecl)
     (errorDecls : Array ErrorDecl)
+    (eventDecls : Array EventDecl)
     (functions : Array FunctionDecl)
     (params : Array ParamDecl)
     (locals : Array TypedLocal)
@@ -151,18 +164,18 @@ private partial def validateDoElemExprTypes
   | some typedLocals => pure typedLocals
   | none => match elem with
       | `(doElem| let _ := ($rhs:term : $_ty:term)) =>
-          validateDoElemExprTypes ownerName fields constDecls immutableDecls externalDecls
-            errorDecls functions params locals (← `(doElem| let _ := $rhs:term))
+          validateDoElemExprTypes ownerName returnTy fields constDecls immutableDecls externalDecls
+            errorDecls eventDecls functions params locals (← `(doElem| let _ := $rhs:term))
       | `(doElem| let _ := $rhs:term) =>
           let discardName := freshSyntheticLocalName "discard" params locals #[]
           let discardIdent := mkIdent (Name.mkSimple discardName)
-          validateDoElemExprTypes ownerName fields constDecls immutableDecls externalDecls
-            errorDecls functions params locals (← `(doElem| let $discardIdent:ident := $rhs:term))
+          validateDoElemExprTypes ownerName returnTy fields constDecls immutableDecls externalDecls
+            errorDecls eventDecls functions params locals (← `(doElem| let $discardIdent:ident := $rhs:term))
       | `(doElem| let _ ← $rhs:term) =>
           let discardName := freshSyntheticLocalName "__discard" params locals #[]
           let discardIdent := mkIdent (Name.mkSimple discardName)
-          validateDoElemExprTypes ownerName fields constDecls immutableDecls externalDecls
-            errorDecls functions params locals (← `(doElem| let $discardIdent:ident ← $rhs:term))
+          validateDoElemExprTypes ownerName returnTy fields constDecls immutableDecls externalDecls
+            errorDecls eventDecls functions params locals (← `(doElem| let $discardIdent:ident ← $rhs:term))
       | `(doElem| let mut $name:ident := $rhs:term) =>
           let ty ← inferPureExprType fields constDecls immutableDecls externalDecls params locals rhs
           requireSupportedLocalBindingType name s!"local binding '{toString name.getId}'" ty
@@ -226,27 +239,32 @@ private partial def validateDoElemExprTypes
                           requireSupportedLocalBindingType name s!"local binding '{toString name.getId}'" ty
                           pure <| locals.push (mkTypedLocal (toString name.getId) ty)
       | `(doElem| $name:ident := $rhs:term) =>
-          let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals rhs
+          let actualTy ← inferPureExprType fields constDecls immutableDecls externalDecls params locals rhs
+          let some localInfo := locals.find? (fun entry => entry.name == toString name.getId)
+            | throwErrorAt name s!"cannot resolve type of variable '{toString name.getId}'"
+          requireDeclaredValueType rhs s!"assignment to '{localInfo.name}'" localInfo.ty actualTy
           pure locals
       | `(doElem| return $value:term) =>
-          let _ ←
+          let actualTy ←
             match (← inferTupleSourceTypes? fields constDecls immutableDecls externalDecls functions params locals value) with
-            | some _ => pure .unit
+            | some valueTys => pure (.tuple valueTys.toList)
             | none => inferPureExprType fields constDecls immutableDecls externalDecls params locals value
+          if returnTypeContainsEnum returnTy then
+            requireDeclaredValueType value s!"return from '{ownerName}'" returnTy actualTy
           pure locals
       | `(doElem| pure ()) =>
           pure locals
       | `(doElem| if $cond:term then $thenBranch:doSeq else $elseBranch:doSeq) =>
           requireBoolType cond "if condition" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals cond)
-          validateDoSeqExprTypes ownerName fields constDecls immutableDecls externalDecls errorDecls functions params locals thenBranch
-          validateDoSeqExprTypes ownerName fields constDecls immutableDecls externalDecls errorDecls functions params locals elseBranch
+          validateDoSeqExprTypes ownerName returnTy fields constDecls immutableDecls externalDecls errorDecls eventDecls functions params locals thenBranch
+          validateDoSeqExprTypes ownerName returnTy fields constDecls immutableDecls externalDecls errorDecls eventDecls functions params locals elseBranch
           pure locals
       | `(doElem| forEach $name:term $count:term $body:term) =>
           requireWordLikeType count "forEach count" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals count)
           match stripParens body with
           | `(term| do $[$inner:doElem]*) =>
               let _ ← validateDoElemsExprTypes
-                ownerName fields constDecls immutableDecls externalDecls errorDecls functions params
+                ownerName returnTy fields constDecls immutableDecls externalDecls errorDecls eventDecls functions params
                 (locals.push (mkTypedLocal (← expectStringOrIdent name) .uint256))
                 inner
               pure locals
@@ -256,7 +274,7 @@ private partial def validateDoElemExprTypes
           match stripParens body with
           | `(term| do $[$inner:doElem]*) =>
               let _ ← validateDoElemsExprTypes
-                ownerName fields constDecls immutableDecls externalDecls errorDecls functions params
+                ownerName returnTy fields constDecls immutableDecls externalDecls errorDecls eventDecls functions params
                 (locals.push (mkTypedLocal (← expectStringOrIdent name) .uint256))
                 inner
               pure locals
@@ -289,10 +307,10 @@ private partial def validateDoElemExprTypes
             (← inferPureExprType fields constDecls immutableDecls externalDecls params locals attempt)
           let (payloadName?, catchElems) ← parseTryCatchHandler handler
           validateTryCatchHandlerDoesNotUsePayload handler payloadName? catchElems
-          let _ ← validateDoElemsExprTypes ownerName fields constDecls immutableDecls externalDecls errorDecls functions params locals catchElems
+          let _ ← validateDoElemsExprTypes ownerName returnTy fields constDecls immutableDecls externalDecls errorDecls eventDecls functions params locals catchElems
           pure locals
       | `(doElem| unsafe $_reason:str do $body:doSeq) =>
-          validateDoSeqExprTypes ownerName fields constDecls immutableDecls externalDecls errorDecls functions params locals body
+          validateDoSeqExprTypes ownerName returnTy fields constDecls immutableDecls externalDecls errorDecls eventDecls functions params locals body
           pure locals
       | `(doElem| ecmBind $names:term $module:term $args:term) =>
           let resultVars ← expectStringList names
@@ -301,11 +319,17 @@ private partial def validateDoElemExprTypes
             args "ECM argument"
           validateResultEcmModuleTerm module resultVars
           pure <| locals ++ resultVars.map (fun name => mkTypedLocal name .uint256)
-      | `(doElem| emit $_eventName:term $values:term) =>
+      | `(doElem| emit $eventName:term $values:term) =>
           match stripParens values with
           | `(term| [ $[$args],* ]) =>
+              let eventNameString ← expectStringOrIdent eventName
+              let some eventDecl := eventDecls.find? (fun ev => ev.name == eventNameString)
+                | throwErrorAt eventName s!"unknown event '{eventNameString}'"
+              if eventDecl.params.size != args.size then
+                throwErrorAt values
+                  s!"event '{eventNameString}' expects {eventDecl.params.size} args, got {args.size}"
               let mut branchLocals := locals
-              for arg in args do
+              for (arg, eventParam) in args.zip eventDecl.params do
                 match ← localInternalArrayReturnBind? fields constDecls immutableDecls externalDecls functions params branchLocals arg with
                 | some (_, _, elemTy) =>
                     let tempName := freshSyntheticLocalName "emit_array" params branchLocals #[]
@@ -314,8 +338,11 @@ private partial def validateDoElemExprTypes
                         ty := .array elemTy
                         source := .memoryArray }
                 | none =>
-                    let _ ← inferEmitArgExprType fields constDecls immutableDecls externalDecls params branchLocals arg
-                    pure ()
+                    let actualTy ← inferEmitArgExprType fields constDecls immutableDecls externalDecls params branchLocals arg
+                    if let expectedTy@(.enum _ _) := eventParam.ty then
+                      requireDeclaredValueType arg
+                        s!"event '{eventNameString}' parameter '{eventParam.name}'"
+                        expectedTy actualTy
               pure locals
           | _ => throwErrorAt values "expected list literal [..]"
       | `(doElem| $stmt:term) =>
@@ -354,6 +381,9 @@ private partial def validateEffectStmtExprTypes
       match f.adtInfo?, f.ty with
       | some _, _ => pure ()
       | none, .scalar (.adt _ _) => pure ()
+      | _, .scalar (expectedTy@(.enum _ _)) =>
+          requireDeclaredValueType value "setStorage value" expectedTy
+            (← inferPureExprType fields constDecls immutableDecls externalDecls params locals value)
       | _, _ =>
           let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals value
           pure ()
@@ -373,21 +403,43 @@ private partial def validateEffectStmtExprTypes
       let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals index
       let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals value
       pure ()
-  | `(term| setMapping $_field:ident $key:term $value:term) | `(term| setMappingAddr $_field:ident $key:term $value:term)
-    | `(term| setMappingUint $_field:ident $key:term $value:term) | `(term| setMappingUintAddr $_field:ident $key:term $value:term)
-    | `(term| setMappingWord $_field:ident $key:term $_wordOffset:num $value:term)
-    | `(term| setStructMember $_field:term $key:term $_member:term $value:term) => do
+  | `(term| setMapping $field:ident $key:term $value:term) | `(term| setMappingAddr $field:ident $key:term $value:term)
+    | `(term| setMappingUint $field:ident $key:term $value:term) | `(term| setMappingUintAddr $field:ident $key:term $value:term)
+    | `(term| setMappingWord $field:ident $key:term $_wordOffset:num $value:term) => do
       let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals key
-      let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals value
-  | `(term| setMapping2 $_field:ident $key1:term $key2:term $value:term)
-    | `(term| setStructMember2 $_field:term $key1:term $key2:term $_member:term $value:term) => do
+      let actualTy ← inferPureExprType fields constDecls immutableDecls externalDecls params locals value
+      if let some f := fields.find? (fun f => f.name == toString field.getId) then
+        if let some expectedTy := storageTypeMappingValueType? f.ty then
+          requireDeclaredValueType value "mapping value" expectedTy actualTy
+  | `(term| setStructMember $field:term $key:term $member:term $value:term) => do
+      let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals key
+      let memberDecl ← lookupStructMemberDecl fields (← expectStringOrIdent field) (← expectStringOrIdent member) false
+      let actualTy ← inferPureExprType fields constDecls immutableDecls externalDecls params locals value
+      match memberDecl.ty with
+      | expectedTy@(.enum _ _) => requireDeclaredValueType value "struct mapping value" expectedTy actualTy
+      | _ => pure ()
+  | `(term| setMapping2 $field:ident $key1:term $key2:term $value:term) => do
       let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals key1
       let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals key2
-      let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals value
-  | `(term| setMappingN $_field:ident $keys:term $value:term) => do
+      let actualTy ← inferPureExprType fields constDecls immutableDecls externalDecls params locals value
+      if let some f := fields.find? (fun f => f.name == toString field.getId) then
+        if let some expectedTy := storageTypeMappingValueType? f.ty then
+          requireDeclaredValueType value "mapping value" expectedTy actualTy
+  | `(term| setStructMember2 $field:term $key1:term $key2:term $member:term $value:term) => do
+      let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals key1
+      let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals key2
+      let memberDecl ← lookupStructMemberDecl fields (← expectStringOrIdent field) (← expectStringOrIdent member) true
+      let actualTy ← inferPureExprType fields constDecls immutableDecls externalDecls params locals value
+      match memberDecl.ty with
+      | expectedTy@(.enum _ _) => requireDeclaredValueType value "struct mapping value" expectedTy actualTy
+      | _ => pure ()
+  | `(term| setMappingN $field:ident $keys:term $value:term) => do
       for key in (← expectMappingKeyTerms keys) do
         let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals key
-      let _ ← inferPureExprType fields constDecls immutableDecls externalDecls params locals value
+      let actualTy ← inferPureExprType fields constDecls immutableDecls externalDecls params locals value
+      if let some f := fields.find? (fun f => f.name == toString field.getId) then
+        if let some expectedTy := storageTypeMappingValueType? f.ty then
+          requireDeclaredValueType value "mapping value" expectedTy actualTy
   | `(term| setMemoryArrayElement $name:term $index:term $value:term) => do
       let (_, elemTy) ← requireSupportedMemoryArrayLocal name "setMemoryArrayElement" locals
       unless isSingleWordStaticValueType elemTy do
@@ -485,6 +537,7 @@ end
 private def validateFunctionBodyExprTypes
     (fields : Array StorageFieldDecl)
     (errorDecls : Array ErrorDecl)
+    (eventDecls : Array EventDecl)
     (constDecls : Array ConstantDecl)
     (immutableDecls : Array ImmutableDecl)
     (externalDecls : Array ExternalDecl)
@@ -492,7 +545,19 @@ private def validateFunctionBodyExprTypes
     (fn : FunctionDecl) : CommandElabM Unit := do
   match fn.body with
   | `(term| do $[$elems:doElem]*) =>
-      let _ ← validateDoElemsExprTypes fn.name fields constDecls immutableDecls externalDecls errorDecls functions fn.params #[] elems
+      -- Generated enum casts accept a raw Uint256, guard it against the member
+      -- count, and only then return it as the enum. Type the guarded parameter
+      -- as that enum while validating this compiler-generated body so the
+      -- exact enum-return rule does not reject the proven refinement.
+      let validationParams :=
+        match fn.isInternal, fn.returnTy, fn.params with
+        | true, enumTy@(.enum enumName _), #[param] =>
+            if fn.name == enumName && param.ty == .uint256 then
+              #[{ param with ty := enumTy }]
+            else
+              fn.params
+        | _, _, _ => fn.params
+      let _ ← validateDoElemsExprTypes fn.name fn.returnTy fields constDecls immutableDecls externalDecls errorDecls eventDecls functions validationParams #[] elems
       pure ()
   | _ => throwErrorAt fn.body "function body must be a do block"
 
@@ -500,11 +565,20 @@ private def validateConstantExprTypes
     (constDecls : Array ConstantDecl) : CommandElabM Unit := do
   for constant in constDecls do
     let inferredTy ← inferPureExprType #[] constDecls #[] #[] #[] #[] constant.body
-    requireDeclaredValueType constant.body s!"constant '{constant.name}'" constant.ty inferredTy
+    -- Enum members are the only compiler-generated enum literals. Their
+    -- qualified name and in-range ordinal make the exception unforgeable by
+    -- ordinary user constants; every other enum value remains exact-typed.
+    let generatedEnumMember := match constant.ty, inferredTy, constant.body.raw.isNatLit? with
+      | .enum enumName memberCount, .uint256, some value =>
+          constant.name.startsWith s!"{enumName}." && value < memberCount
+      | _, _, _ => false
+    unless generatedEnumMember do
+      requireDeclaredValueType constant.body s!"constant '{constant.name}'" constant.ty inferredTy
 
 private def validateConstructorBodyExprTypes
     (fields : Array StorageFieldDecl)
     (errorDecls : Array ErrorDecl)
+    (eventDecls : Array EventDecl)
     (constDecls : Array ConstantDecl)
     (immutableDecls : Array ImmutableDecl)
     (externalDecls : Array ExternalDecl)
@@ -512,7 +586,7 @@ private def validateConstructorBodyExprTypes
     (ctor : ConstructorDecl) : CommandElabM Unit := do
   match ctor.body with
   | `(term| do $[$elems:doElem]*) =>
-      let _ ← validateDoElemsExprTypes "constructor" fields constDecls immutableDecls externalDecls errorDecls functions ctor.params #[] elems
+      let _ ← validateDoElemsExprTypes "constructor" .unit fields constDecls immutableDecls externalDecls errorDecls eventDecls functions ctor.params #[] elems
       pure ()
   | _ => throwErrorAt ctor.body "constructor body must be a do block"
 
@@ -710,7 +784,7 @@ private def translateEffectStmt
               $(← translateAdtConstructForStorage fields constDecls immutableDecls params locals adtName value))
       | none =>
           match f.ty with
-          | .scalar .uint256 | .scalar .int256 | .scalar (.newtype _ .uint256) =>
+          | .scalar .uint256 | .scalar .int256 | .scalar (.newtype _ .uint256) | .scalar (.enum _ _) =>
               `(Compiler.CompilationModel.Stmt.setStorage $(strTerm f.name) $(← translatePureExprWithTypes fields constDecls immutableDecls params locals value))
           | .scalar (.adt adtName _) =>
               `(Compiler.CompilationModel.Stmt.setStorage
@@ -727,7 +801,7 @@ private def translateEffectStmt
       match f.ty with
       | .scalar .address | .scalar (.newtype _ .address) =>
           `(Compiler.CompilationModel.Stmt.setStorageAddr $(strTerm f.name) $(← translatePureExprWithTypes fields constDecls immutableDecls params locals value))
-      | .scalar .uint256 | .scalar (.newtype _ .uint256) =>
+      | .scalar .uint256 | .scalar (.newtype _ .uint256) | .scalar (.enum _ _) =>
           throwErrorAt stx s!"field '{f.name}' is Uint256-valued; use setStorage"
       | .dynamicArray _ =>
           throwErrorAt stx s!"field '{f.name}' is a storage dynamic array; use pushStorageArray/popStorageArray/setStorageArrayElement"
@@ -744,24 +818,25 @@ private def translateEffectStmt
       | .dynamicArray _ =>
           throwErrorAt stx s!"field '{f.name}' is a storage dynamic array; setPackedStorage requires a scalar root slot"
       | .mappingAddressToUint256 | .mappingUintToUint256 | .mapping2AddressToAddressToUint256
-      | .mappingChain _ | .mappingStruct _ _ | .mappingStruct2 _ _ _ =>
+      | .mappingAddressToEnum _ _ | .mappingUintToEnum _ _ | .mapping2AddressToAddressToEnum _ _
+      | .mappingChain _ | .mappingChainEnum _ _ _ | .mappingStruct _ _ | .mappingStruct2 _ _ _ =>
           throwErrorAt stx s!"field '{f.name}' is a mapping; setPackedStorage requires a scalar root slot"
   | `(term| setMapping $field:ident $key:term $value:term) =>
       let f ← lookupStorageField fields (toString field.getId)
       match f.ty with
-      | .mappingAddressToUint256 =>
+      | .mappingAddressToUint256 | .mappingAddressToEnum _ _ =>
           `(Compiler.CompilationModel.Stmt.setMapping
               $(strTerm f.name)
               $(← translatePureExprWithTypes fields constDecls immutableDecls params locals key)
               $(← translatePureExprWithTypes fields constDecls immutableDecls params locals value))
-      | .mappingUintToUint256 =>
+      | .mappingUintToUint256 | .mappingUintToEnum _ _ =>
           `(Compiler.CompilationModel.Stmt.setMappingUint
               $(strTerm f.name)
               $(← translatePureExprWithTypes fields constDecls immutableDecls params locals key)
               $(← translatePureExprWithTypes fields constDecls immutableDecls params locals value))
-      | .mapping2AddressToAddressToUint256 =>
+      | .mapping2AddressToAddressToUint256 | .mapping2AddressToAddressToEnum _ _ =>
           throwErrorAt stx s!"field '{f.name}' is a double mapping; use setMapping2"
-      | .mappingChain _ =>
+      | .mappingChain _ | .mappingChainEnum _ _ _ =>
           throwErrorAt stx s!"field '{f.name}' uses {storageTypeMappingDepth? f.ty |>.getD 0} mapping keys; use setMappingN"
       | .dynamicArray _ =>
           throwErrorAt stx s!"field '{f.name}' is a storage dynamic array; use pushStorageArray/popStorageArray/setStorageArrayElement"
@@ -778,9 +853,11 @@ private def translateEffectStmt
               $(← translatePureExprWithTypes fields constDecls immutableDecls params locals value))
       | .mappingUintToUint256 =>
           throwErrorAt stx s!"field '{f.name}' is Uint256-keyed; use setMappingUintAddr"
-      | .mapping2AddressToAddressToUint256 =>
+      | .mappingAddressToEnum _ _ | .mappingUintToEnum _ _ =>
+          throwErrorAt stx s!"field '{f.name}' is enum-valued; use setMapping/setMappingUint"
+      | .mapping2AddressToAddressToUint256 | .mapping2AddressToAddressToEnum _ _ =>
           throwErrorAt stx s!"field '{f.name}' is a double mapping; use setMapping2"
-      | .mappingChain _ =>
+      | .mappingChain _ | .mappingChainEnum _ _ _ =>
           throwErrorAt stx s!"field '{f.name}' uses {storageTypeMappingDepth? f.ty |>.getD 0} mapping keys; use setMappingN"
       | .dynamicArray _ =>
           throwErrorAt stx s!"field '{f.name}' is a storage dynamic array; use pushStorageArray/popStorageArray/setStorageArrayElement"
@@ -790,16 +867,16 @@ private def translateEffectStmt
   | `(term| setMappingUint $field:ident $key:term $value:term) =>
       let f ← lookupStorageField fields (toString field.getId)
       match f.ty with
-      | .mappingUintToUint256 =>
+      | .mappingUintToUint256 | .mappingUintToEnum _ _ =>
           `(Compiler.CompilationModel.Stmt.setMappingUint
               $(strTerm f.name)
               $(← translatePureExprWithTypes fields constDecls immutableDecls params locals key)
               $(← translatePureExprWithTypes fields constDecls immutableDecls params locals value))
-      | .mappingAddressToUint256 =>
+      | .mappingAddressToUint256 | .mappingAddressToEnum _ _ =>
           throwErrorAt stx s!"field '{f.name}' is Address-keyed; use setMapping"
-      | .mapping2AddressToAddressToUint256 =>
+      | .mapping2AddressToAddressToUint256 | .mapping2AddressToAddressToEnum _ _ =>
           throwErrorAt stx s!"field '{f.name}' is a double mapping; use setMapping2"
-      | .mappingChain _ =>
+      | .mappingChain _ | .mappingChainEnum _ _ _ =>
           throwErrorAt stx s!"field '{f.name}' uses {storageTypeMappingDepth? f.ty |>.getD 0} mapping keys; use setMappingN"
       | .dynamicArray _ =>
           throwErrorAt stx s!"field '{f.name}' is a storage dynamic array; use pushStorageArray/popStorageArray/setStorageArrayElement"
@@ -816,9 +893,11 @@ private def translateEffectStmt
               $(← translatePureExprWithTypes fields constDecls immutableDecls params locals value))
       | .mappingAddressToUint256 =>
           throwErrorAt stx s!"field '{f.name}' is Address-keyed; use setMappingAddr"
-      | .mapping2AddressToAddressToUint256 =>
+      | .mappingAddressToEnum _ _ | .mappingUintToEnum _ _ =>
+          throwErrorAt stx s!"field '{f.name}' is enum-valued; use setMapping/setMappingUint"
+      | .mapping2AddressToAddressToUint256 | .mapping2AddressToAddressToEnum _ _ =>
           throwErrorAt stx s!"field '{f.name}' is a double mapping; use setMapping2"
-      | .mappingChain _ =>
+      | .mappingChain _ | .mappingChainEnum _ _ _ =>
           throwErrorAt stx s!"field '{f.name}' uses {storageTypeMappingDepth? f.ty |>.getD 0} mapping keys; use setMappingN"
       | .dynamicArray _ =>
           throwErrorAt stx s!"field '{f.name}' is a storage dynamic array; use pushStorageArray/popStorageArray/setStorageArrayElement"
@@ -828,13 +907,14 @@ private def translateEffectStmt
   | `(term| setMappingWord $field:ident $key:term $wordOffset:num $value:term) =>
       let f ← lookupStorageField fields (toString field.getId)
       match f.ty with
-      | .mappingAddressToUint256 | .mappingUintToUint256 =>
+      | .mappingAddressToUint256 | .mappingUintToUint256
+        | .mappingAddressToEnum _ _ | .mappingUintToEnum _ _ =>
           `(Compiler.CompilationModel.Stmt.setMappingWord
               $(strTerm f.name)
               $(← translatePureExprWithTypes fields constDecls immutableDecls params locals key)
               $wordOffset
               $(← translatePureExprWithTypes fields constDecls immutableDecls params locals value))
-      | .mapping2AddressToAddressToUint256 =>
+      | .mapping2AddressToAddressToUint256 | .mapping2AddressToAddressToEnum _ _ =>
           throwErrorAt stx s!"field '{f.name}' is a double mapping; use setMapping2Word"
       | .mappingStruct _ _ =>
           throwErrorAt stx s!"field '{f.name}' is a struct-valued mapping; use setStructMember"
@@ -843,12 +923,12 @@ private def translateEffectStmt
       | .dynamicArray _ =>
           throwErrorAt stx s!"field '{f.name}' is a storage dynamic array; use pushStorageArray/popStorageArray/setStorageArrayElement"
       | .scalar _ => throwErrorAt stx s!"field '{f.name}' is not a mapping"
-      | .mappingChain _ =>
+      | .mappingChain _ | .mappingChainEnum _ _ _ =>
           throwErrorAt stx s!"field '{f.name}' uses {storageTypeMappingDepth? f.ty |>.getD 0} mapping keys; use setMappingN"
   | `(term| setMapping2 $field:ident $key1:term $key2:term $value:term) =>
       let f ← lookupStorageField fields (toString field.getId)
       match f.ty with
-      | .mapping2AddressToAddressToUint256 =>
+      | .mapping2AddressToAddressToUint256 | .mapping2AddressToAddressToEnum _ _ =>
           `(Compiler.CompilationModel.Stmt.setMapping2
               $(strTerm f.name)
               $(← translatePureExprWithTypes fields constDecls immutableDecls params locals key1)
@@ -1626,6 +1706,47 @@ private partial def translateDoElem
       | _ => throwErrorAt elem "unsupported do element"
 end
 
+private partial def containsEnumValueType : ValueType → Bool
+  | .enum _ _ => true
+  | .array elemTy | .fixedArray elemTy _ => containsEnumValueType elemTy
+  | .tuple elemTys => elemTys.any containsEnumValueType
+  | .struct _ fields => fields.any (fun field => containsEnumValueType field.snd)
+  | .newtype _ baseTy => containsEnumValueType baseTy
+  | _ => false
+
+private def enumParamGuards (params : Array ParamDecl) : CommandElabM (Array (TSyntax `doElem)) :=
+  params.filterMapM fun param => do
+    match param.ty with
+    | .enum _ memberCount =>
+        let bound := natTerm memberCount
+        pure (some (← `(doElem|
+          if toUint256 $(param.ident) < $bound then
+            pure ()
+          else
+            panic(0x21))))
+    | ty =>
+        if containsEnumValueType ty then
+          throwErrorAt param.ident
+            "enum values nested in Array, FixedArray, Tuple, Struct, or newtype parameters are not yet supported; pass enum values as direct parameters so range validation remains explicit"
+        pure none
+
+private def prependEnumGuards
+    (params : Array ParamDecl) (body : Term) : CommandElabM Term := do
+  let guards ← enumParamGuards params
+  if guards.isEmpty then
+    pure body
+  else
+    match body with
+    | `(term| do $[$elems:doElem]*) =>
+        `(term| do $[$guards:doElem]* $[$elems:doElem]*)
+    | _ => throwErrorAt body "function or constructor body must be a do block"
+
+private def guardEnumParams (fn : FunctionDecl) : CommandElabM FunctionDecl := do
+  pure { fn with body := ← prependEnumGuards fn.params fn.body }
+
+private def guardEnumConstructor (ctor : ConstructorDecl) : CommandElabM ConstructorDecl := do
+  pure { ctor with body := ← prependEnumGuards ctor.params ctor.body }
+
 private def translateBodyToStmtTerms
     (fields : Array StorageFieldDecl)
     (roleDecls : Array RoleDecl)
@@ -1637,11 +1758,16 @@ private def translateBodyToStmtTerms
     (fn : FunctionDecl) : CommandElabM (Array Term) := do
   match fn.body with
   | `(term| do $[$elems:doElem]*) =>
+      let enumGuardCount := (← enumParamGuards fn.params).size
       let guardPrelude ← initGuardPreludeStmtTerms fields fn
       let rolePrelude ← roleGuardPreludeStmtTerms fields roleDecls fn
       let modifierPrelude ← fn.modifiers.mapM fun modIdent =>
         `(Compiler.CompilationModel.Stmt.internalCall $(strTerm (modifierInternalName (toString modIdent.getId))) [])
-      let stmts := guardPrelude ++ rolePrelude ++ modifierPrelude ++ (← translateDoElems fields constDecls immutableDecls externalDecls errorDecls functions fn.returnTy fn.params #[] #[] elems).1
+      let bodyStmts := (← translateDoElems fields constDecls immutableDecls externalDecls errorDecls functions fn.returnTy fn.params #[] #[] elems).1
+      -- ABI decoding (including enum validity) precedes every function-level
+      -- prelude in Solidity. Keep those guards first on the model path too.
+      let stmts := bodyStmts.take enumGuardCount ++ guardPrelude ++ rolePrelude ++
+        modifierPrelude ++ bodyStmts.drop enumGuardCount
       let mut stmts := stmts
       if fn.returnTy == .unit then
         stmts := stmts.push (← `(Compiler.CompilationModel.Stmt.stop))
@@ -1925,7 +2051,13 @@ private def mkContractFnValue (params : Array ParamDecl) (body : Term) : Command
 
 private def mkModelParamsTerm (params : Array ParamDecl) : CommandElabM Term := do
   let xs ← params.mapM fun p => do
-    `(Compiler.CompilationModel.Param.mk $(strTerm p.name) $(← modelParamTypeTerm p.ty))
+    let tyTerm ← match p.ty with
+      -- Function/constructor enum inputs keep the uint8 ABI spelling but load
+      -- the full word so the injected enum guard observes non-canonical data.
+      | .enum _ _ =>
+          `(Compiler.CompilationModel.ParamType.newtypeOf "__verity_enum" Compiler.CompilationModel.ParamType.uint256)
+      | ty => modelParamTypeTerm ty
+    `(Compiler.CompilationModel.Param.mk $(strTerm p.name) $tyTerm)
   `([ $[$xs],* ])
 
 private def storageSlotInnerTypeTerm (ty : StorageType) : CommandElabM Term := do
@@ -1958,6 +2090,7 @@ private def storageSlotInnerTypeTerm (ty : StorageType) : CommandElabM Term := d
         | .uint256 => `(Uint256)
         | .address => `(Address)
         | _ => throwError "storage field with newtype base type not supported; use Uint256 or Address"
+    | .scalar (.enum _ _) => `(Uint256)
     | .scalar (.adt _ _) => `(Uint256)  -- ADTs stored as tag value in storage (#1727 Step 5b)
     | .dynamicArray .uint256 => `(List Uint256)
     | .dynamicArray .address => `(List Address)
@@ -1965,9 +2098,13 @@ private def storageSlotInnerTypeTerm (ty : StorageType) : CommandElabM Term := d
     | .dynamicArray .uint8 => throwError "storage dynamic arrays currently support only Uint256 elements on the macro path"
     | .dynamicArray .bytes32 => `(List Uint256)
     | .mappingAddressToUint256 => `(Address → Uint256)
+    | .mappingAddressToEnum _ _ => `(Address → Uint256)
     | .mapping2AddressToAddressToUint256 => `(Address → Address → Uint256)
+    | .mapping2AddressToAddressToEnum _ _ => `(Address → Address → Uint256)
     | .mappingUintToUint256 => `(Uint256 → Uint256)
+    | .mappingUintToEnum _ _ => `(Uint256 → Uint256)
     | .mappingChain keyTypes => mkStorageMappingTy keyTypes
+    | .mappingChainEnum keyTypes _ _ => mkStorageMappingTy keyTypes
     | .mappingStruct keyType _ => `(($(← storageKeyTypeContractTerm keyType) → Uint256))
     | .mappingStruct2 outerKey innerKey _ =>
         `(($(← storageKeyTypeContractTerm outerKey) → $(← storageKeyTypeContractTerm innerKey) → Uint256))
@@ -2396,7 +2533,9 @@ private def mkSpecCommand
           (constructorLocalObligationsWithArithmetic ctor immutableDecls).mapM mkModelLocalObligationTerm
         let immutableInitTerms ← immutableInitStmtTerms fields constDecls immutableDecls ctor.params
         let ctorBodyTerms ← translateConstructorBodyToStmtTerms fields errorDecls constDecls immutableDecls externalDecls functions ctor
-        let ctorAllTerms := immutableInitTerms ++ ctorBodyTerms
+        let enumGuardCount := (← enumParamGuards ctor.params).size
+        let ctorAllTerms := ctorBodyTerms.take enumGuardCount ++ immutableInitTerms ++
+          ctorBodyTerms.drop enumGuardCount
         `(some {
           params := $ctorParams
           isPayable := $ctorPayable
@@ -2703,6 +2842,7 @@ private partial def offsetStorageAccessorTree (offset : Nat) : StorageAccessorTr
 structure ParsedContractSyntax where
   contractName : Ident
   newtypeDecls : Array NewtypeDecl
+  enumDecls : Array EnumDecl
   structDecls : Array StructDecl
   adtDecls : Array AdtDecl
   fields : Array StorageFieldDecl
@@ -2751,12 +2891,18 @@ 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 where $[types $[$newtypeDecls:verityNewtype]*]? $[enums $[$enumDecls:verityEnumDecl]*]? $[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]*) =>
       -- Parse newtypes first — they are needed by all downstream type resolution
       let parsedNewtypes ←
         match newtypeDecls with
         | some decls => decls.mapM parseNewtype
         | none => pure #[]
+      let parsedEnums ←
+        match enumDecls with
+        | some decls => decls.mapM parseEnumDecl
+        | none => pure #[]
+      let parsedNewtypes := parsedNewtypes ++ parsedEnums.map (fun e => {
+        ident := e.ident, name := e.name, baseType := .uint8, enumMembers := e.members })
       -- Validate: no duplicate type names
       let mut seenNames : Array String := #[]
       for nt in parsedNewtypes do
@@ -2826,6 +2972,16 @@ def parseContractSyntax
         match constantDecls with
         | some decls => decls.mapM (parseConstant parsedNewtypes)
         | none => pure #[]
+      let mut parsedConstants := parsedConstants
+      for enumDecl in parsedEnums do
+        for (member, idx) in enumDecl.members.zipIdx do
+          let qualified := Name.str enumDecl.ident.getId (toString member.getId)
+          parsedConstants := parsedConstants.push {
+            ident := mkIdentFrom member qualified
+            name := toString qualified
+            ty := .enum enumDecl.name enumDecl.members.size
+            body := natTerm idx
+          }
       let parsedImmutables ←
         match immutableDecls with
         | some decls => decls.mapM (parseImmutable parsedNewtypes)
@@ -2905,9 +3061,35 @@ def parseContractSyntax
         if seenRoleNames.contains role.name then
           throwErrorAt role.ident s!"duplicate role declaration '{role.name}'"
         seenRoleNames := seenRoleNames.push role.name
+      let parsedUserFunctions ←
+        (assignOverloadInternalIdents
+          (← monomorphizeHigherOrderHelpers
+            ((← entrypoints.mapM parseSpecialEntrypoint) ++
+              (← functions.mapM (parseFunction parsedNewtypes parsedStructs parsedAdts interfaceNames))))).mapM
+          guardEnumParams
+      let mut enumCastFunctions : Array FunctionDecl := #[]
+      for enumDecl in parsedEnums do
+        let argId := mkIdentFrom enumDecl.ident (Name.mkSimple "x")
+        let bound := natTerm enumDecl.members.size
+        let body ← `(term| do
+          if toUint256 $argId < $bound then
+            return $argId
+          else
+            panic(0x21))
+        enumCastFunctions := enumCastFunctions.push {
+          ident := enumDecl.ident
+          name := enumDecl.name
+          params := #[{ ident := argId, name := "x", ty := .uint256 }]
+          returnTy := .enum enumDecl.name enumDecl.members.size
+          isPure := true
+          isInternal := true
+          body := body
+        }
+      let parsedFunctions := enumCastFunctions ++ parsedUserFunctions
       pure {
         contractName := contractName
         newtypeDecls := parsedNewtypes
+        enumDecls := parsedEnums
         structDecls := parsedStructs
         adtDecls := parsedAdts
         fields := parsedFields
@@ -2918,13 +3100,10 @@ def parseContractSyntax
         constDecls := parsedConstants
         immutableDecls := parsedImmutables
         externalDecls := parsedExternals
-        ctor := (← ctor.mapM (parseConstructor parsedNewtypes parsedStructs parsedAdts))
+        ctor := (← ctor.mapM fun ctorStx => do
+          guardEnumConstructor (← parseConstructor parsedNewtypes parsedStructs parsedAdts ctorStx))
         modifiers := (← modifierDecls.mapM parseModifier)
-        functions :=
-          assignOverloadInternalIdents
-            (← monomorphizeHigherOrderHelpers
-              ((← entrypoints.mapM parseSpecialEntrypoint) ++
-                (← functions.mapM (parseFunction parsedNewtypes parsedStructs parsedAdts interfaceNames))))
+        functions := parsedFunctions
         storageNamespace := firstNamespaceOpt
       }
   | _ => throwErrorAt stx "invalid verity_contract declaration"
@@ -3150,6 +3329,7 @@ private def validateLocalObligationDecls
 def validateFunctionDeclsPublic
     (fields : Array StorageFieldDecl)
     (errorDecls : Array ErrorDecl)
+    (eventDecls : Array EventDecl)
     (constDecls : Array ConstantDecl)
     (immutableDecls : Array ImmutableDecl)
     (externalDecls : Array ExternalDecl)
@@ -3161,13 +3341,13 @@ def validateFunctionDeclsPublic
       for param in ctor.params do
         rejectExecutableBoundaryAdt param.ident s!"constructor parameter '{param.name}'" param.ty
       validateLocalObligationDecls "constructor" ctor.localObligations
-      validateConstructorBodyExprTypes fields errorDecls constDecls immutableDecls externalDecls functions ctor
+      validateConstructorBodyExprTypes fields errorDecls eventDecls constDecls immutableDecls externalDecls functions ctor
   | none => pure ()
   let modifierNames := modifiers.map (·.name)
   for modDecl in modifiers do
     match modDecl.body with
     | `(term| do $[$elems:doElem]*) =>
-        let _ ← validateDoElemsExprTypes modDecl.name fields constDecls immutableDecls externalDecls errorDecls functions #[] #[] elems
+        let _ ← validateDoElemsExprTypes modDecl.name .unit fields constDecls immutableDecls externalDecls errorDecls eventDecls functions #[] #[] elems
         pure ()
     | _ => throwErrorAt modDecl.body "modifier body must be a do block"
   for fn in functions do
@@ -3221,7 +3401,7 @@ def validateFunctionDeclsPublic
       throwErrorAt fn.ident s!"function '{fn.name}': nonreentrant and allow_post_interaction_writes are mutually exclusive"
     if fn.nonReentrantLock.isSome && fn.ceiSafe then
       throwErrorAt fn.ident s!"function '{fn.name}': nonreentrant and cei_safe are mutually exclusive"
-    validateFunctionBodyExprTypes fields errorDecls constDecls immutableDecls externalDecls functions fn
+    validateFunctionBodyExprTypes fields errorDecls eventDecls constDecls immutableDecls externalDecls functions fn
 
 def mkFunctionCommandsPublic
     (fields : Array StorageFieldDecl)
@@ -3238,6 +3418,10 @@ def mkFunctionCommandsPublic
   let fnGuardedBody ← mkInitGuardedBody fields fnDecl
   let fnBody ← mkImmutableBoundBody fields immutableDecls fn fnGuardedBody
   let fnExecutableBody ← rewriteForEachExecutableBody externalDecls fn.params fnBody
+  -- The parsed body already contains guards for the model path. Re-applying
+  -- them outside all executable wrappers makes ABI validation happen before
+  -- initializer, role, and modifier effects (the inner copy is harmless).
+  let fnExecutableBody ← prependEnumGuards fn.params fnExecutableBody
   let fnValue ← mkContractFnValue fn.params fnExecutableBody
   let modelBodyName ← mkSuffixedIdent fn.ident "_modelBody"
   let modelName ← mkSuffixedIdent fn.ident "_model"
diff --git a/Verity/Macro/Translate/Expr.lean b/Verity/Macro/Translate/Expr.lean
index 3fb4f68df..beea95feb 100644
--- a/Verity/Macro/Translate/Expr.lean
+++ b/Verity/Macro/Translate/Expr.lean
@@ -52,6 +52,7 @@ partial def modelParamTypeTerm (ty : ValueType) : CommandElabM Term :=
   | .newtype name baseType => do
       let baseTerm ← modelParamTypeTerm baseType
       `(Compiler.CompilationModel.ParamType.newtypeOf $(Lean.quote name) $baseTerm)
+  | .enum _ _ => `(Compiler.CompilationModel.ParamType.uint8)
   | .adt name maxFields => do
       `(Compiler.CompilationModel.ParamType.adt $(Lean.quote name) $(Lean.quote maxFields))
 
@@ -73,6 +74,7 @@ def modelReturnTypeTerm (ty : ValueType) : CommandElabM Term :=
   | .tuple _ => `(none)
   | .struct _ _ => `(none)
   | .newtype _ baseType => modelReturnTypeTerm baseType
+  | .enum _ _ => `(none)
   | .adt _ _ => `(none)  -- ADTs are not directly returnable as single FieldType
 
 partial def modelReturnsTerm (ty : ValueType) : CommandElabM Term :=
@@ -103,6 +105,7 @@ partial def modelReturnsTerm (ty : ValueType) : CommandElabM Term :=
   | .newtype name baseType => do
       let baseTerm ← modelParamTypeTerm baseType
       `([Compiler.CompilationModel.ParamType.newtypeOf $(Lean.quote name) $baseTerm])
+  | .enum _ _ => `([Compiler.CompilationModel.ParamType.uint8])
   | .adt name maxFields => do
       `([Compiler.CompilationModel.ParamType.adt $(Lean.quote name) $(Lean.quote maxFields)])
 
@@ -189,6 +192,7 @@ partial def contractValueTypeTerm (ty : ValueType) : CommandElabM Term :=
   | .tuple elemTys => mkTupleContractType elemTys
   | .unit => `(Unit)
   | .newtype _ baseType => contractValueTypeTerm baseType  -- Erased to base type at contract level
+  | .enum _ _ => `(Uint256)
   | .struct name _ => pure (mkIdent (Name.mkSimple name))
   | .adt _ _ => `(Uint256)  -- ADTs represented as tag value at contract level
 end
@@ -213,6 +217,7 @@ def normalizeTranslatedExprForType
           `(Compiler.CompilationModel.Expr.bitAnd $expr
               (Compiler.CompilationModel.Expr.literal $(natTerm mask)))
   | .newtype _ baseType => normalizeTranslatedExprForType baseType source expr
+  | .enum _ _ => `(Compiler.CompilationModel.Expr.bitAnd $expr (Compiler.CompilationModel.Expr.literal 255))
   | _ => pure expr
 
 def immutableHiddenName (imm : ImmutableDecl) : String :=
@@ -691,6 +696,7 @@ def isWordLikeValueType : ValueType → Bool
   | .uint256 | .int256 | .uint8 | .uint16 | .uintN _ | .intN _ | .bytesN _
   | .address | .bytes32 => true
   | .newtype _ baseType => isWordLikeValueType baseType
+  | .enum _ _ => true
   | _ => false
 
 def isSingleWordStaticValueType : ValueType → Bool
@@ -725,6 +731,7 @@ partial def staticAbiWordCount? : ValueType → Option Nat
           | _, _ => none)
         (some 0)
   | .newtype _ baseType => staticAbiWordCount? baseType
+  | .enum _ _ => some 1
   | _ => none
 
 partial def staticAbiLeafNames? : ValueType → Option (List String)
@@ -752,6 +759,7 @@ partial def staticAbiLeafNames? : ValueType → Option (List String)
           out := out ++ [if suffix == "" then fieldName else s!"{fieldName}_{suffix}"]
       some out
   | .newtype _ baseType => staticAbiLeafNames? baseType
+  | .enum _ _ => some [""]
   | _ => none
 
 partial def staticStructDirectFieldLocals?
@@ -795,6 +803,7 @@ partial def abiLocalHeadWordCount? : ValueType → Option Nat
           | _, _ => none)
         (some 0)
   | .newtype _ baseType => abiLocalHeadWordCount? baseType
+  | .enum _ _ => some 1
   | .adt _ _ | .unit => none
 
 partial def valueTypeUsesDynamicData : ValueType → Bool
@@ -803,6 +812,7 @@ partial def valueTypeUsesDynamicData : ValueType → Bool
   | .tuple elemTys => elemTys.any valueTypeUsesDynamicData
   | .struct _ fields => fields.any (fun field => valueTypeUsesDynamicData field.snd)
   | .newtype _ baseType => valueTypeUsesDynamicData baseType
+  | .enum _ _ => false
   | .adt _ _ => false  -- ADTs are stored as tag + fixed-width slots, not dynamic
   | .uint256 | .int256 | .uint8 | .uint16 | .uintN _ | .intN _ | .bytesN _
   | .address | .bytes32 | .bool | .unit => false
@@ -821,6 +831,7 @@ partial def abiParentHeadWordCount? (ty : ValueType) : Option Nat :=
       else
         abiLocalHeadWordCount? ty
   | .newtype _ baseType => abiParentHeadWordCount? baseType
+  | .enum _ _ => some 1
   | .uint256 | .int256 | .uint8 | .uint16 | .uintN _ | .intN _ | .bytesN _
   | .address | .bytes32 | .bool => some 1
   | .adt _ _ | .unit => none
@@ -829,6 +840,10 @@ def classifyWordArithmeticResultType
     (stx : Syntax)
     (context : String)
     (lhsTy rhsTy : ValueType) : CommandElabM ValueType := do
+  if (match lhsTy with | .enum _ _ => true | _ => false) ||
+      (match rhsTy with | .enum _ _ => true | _ => false) then
+    throwErrorAt stx
+      s!"{context} requires `toUint256` before applying word operators to enum values; got {reprStr lhsTy} and {reprStr rhsTy}"
   unless isWordLikeValueType lhsTy do
     throwErrorAt stx s!"{context} requires a word-like value (Uint256, Int256, Uint8, Address, or Bytes32), got {reprStr lhsTy}"
   unless isWordLikeValueType rhsTy do
@@ -850,6 +865,10 @@ def classifyUnsignedWordArithmeticResultType
     (stx : Syntax)
     (context : String)
     (lhsTy rhsTy : ValueType) : CommandElabM ValueType := do
+  if (match lhsTy with | .enum _ _ => true | _ => false) ||
+      (match rhsTy with | .enum _ _ => true | _ => false) then
+    throwErrorAt stx
+      s!"{context} requires `toUint256` before applying word operators to enum values; got {reprStr lhsTy} and {reprStr rhsTy}"
   unless isWordLikeValueType lhsTy do
     throwErrorAt stx s!"{context} requires a word-like value (Uint256, Int256, Uint8, Address, or Bytes32), got {reprStr lhsTy}"
   unless isWordLikeValueType rhsTy do
@@ -864,6 +883,7 @@ def isNatLiteralTerm (stx : Term) : Bool :=
 def numericLiteralCompatibleValueType : ValueType → Bool
   | .uint256 | .int256 | .uint8 | .uint16 | .uintN _ | .intN _ | .bytesN _ => true
   | .newtype _ baseType => numericLiteralCompatibleValueType baseType
+  | .enum _ _ => false
   | _ => false
 
 def argumentTypeMatchesParam (arg : Term) (argTy paramTy : ValueType) : Bool :=
@@ -1372,10 +1392,20 @@ def requireTypedInterfaceStaticParams
     True dynamic returns (bytes/string, arrays with dynamic elements) are
     still rejected here with the #1982 error until full ABI-frame
     typed-interface lowering exists. -/
+partial def containsEnumInterfaceReturn : ValueType → Bool
+  | .enum _ _ => true
+  | .array ty | .fixedArray ty _ | .newtype _ ty => containsEnumInterfaceReturn ty
+  | .tuple tys => tys.any containsEnumInterfaceReturn
+  | .struct _ fields => fields.any (fun field => containsEnumInterfaceReturn field.snd)
+  | _ => false
+
 def requireTypedInterfaceStaticReturns
     (stx : Syntax) (externalName : String) (returnTys : Array ValueType) : CommandElabM Unit := do
   for h : i in [:returnTys.size] do
     let ty := returnTys[i]
+    if containsEnumInterfaceReturn ty then
+      throwErrorAt stx
+        s!"typed interface call '{externalName}' uses an enum-valued return; checked enum decoding from untrusted external returndata is not implemented"
     if staticAbiWordCount? ty |>.isNone then
       throwErrorAt stx
         s!"typed interface call '{externalName}' currently supports only static (single-word or composite) returns; return {i + 1} has {renderValueType ty}. Dynamic and composite ABI returns require ABI-frame typed-interface lowering, which is not implemented yet (#1982)."
@@ -1407,6 +1437,13 @@ def requireWordLikeType (stx : Syntax) (context : String) (ty : ValueType) : Com
   unless isWordLikeValueType ty do
     throwErrorAt stx s!"{context} requires a word-like value (Uint256, Int256, Uint8, Address, or Bytes32), got {renderValueType ty}"
 
+def requireWordOperatorType (stx : Syntax) (context : String) (ty : ValueType) : CommandElabM Unit := do
+  match ty with
+  | .enum _ _ =>
+      throwErrorAt stx
+        s!"{context} requires `toUint256` before applying word operators to enum values; got {renderValueType ty}"
+  | _ => requireWordLikeType stx context ty
+
 def requireBoolType (stx : Syntax) (context : String) (ty : ValueType) : CommandElabM Unit := do
   unless ty == .bool do
     throwErrorAt stx s!"{context} requires Bool, got {renderValueType ty}"
@@ -1504,10 +1541,14 @@ def requireSupportedReturnStorageWordsType
         s!"{context} requires an Array parameter on the compilation-model path, got {renderValueType ty}"
 
 def requireEqComparableTypes (stx : Syntax) (lhsTy rhsTy : ValueType) : CommandElabM Unit := do
-  let bothWordLike := isWordLikeValueType lhsTy && isWordLikeValueType rhsTy
+  let involvesEnum := match lhsTy, rhsTy with
+    | .enum _ _, _ | _, .enum _ _ => true
+    | _, _ => false
+  let bothWordLike := !involvesEnum && isWordLikeValueType lhsTy && isWordLikeValueType rhsTy
+  let sameEnum := involvesEnum && lhsTy == rhsTy
   let bothBool := lhsTy == .bool && rhsTy == .bool
   let bothDynamicBytes := (lhsTy == .string && rhsTy == .string) || (lhsTy == .bytes && rhsTy == .bytes)
-  unless bothWordLike || bothBool || bothDynamicBytes do
+  unless sameEnum || bothWordLike || bothBool || bothDynamicBytes do
     throwErrorAt stx
       s!"equality is currently supported only for Bool, matching bytes/string params, and word-like values (Uint256, Int256, Uint8, Address, Bytes32); got {renderValueType lhsTy} and {renderValueType rhsTy}"
 
@@ -1541,7 +1582,10 @@ def dynamicEqParamNames
         "bytes/string equality currently requires direct parameter references on the compilation-model path"
 
 def requireSameOrWordLikeTypes (stx : Syntax) (context : String) (lhsTy rhsTy : ValueType) : CommandElabM Unit := do
-  unless lhsTy == rhsTy || (isWordLikeValueType lhsTy && isWordLikeValueType rhsTy) do
+  let involvesEnum := match lhsTy, rhsTy with
+    | .enum _ _, _ | _, .enum _ _ => true
+    | _, _ => false
+  unless lhsTy == rhsTy || (!involvesEnum && isWordLikeValueType lhsTy && isWordLikeValueType rhsTy) do
     throwErrorAt stx
       s!"{context} requires matching branch types, got {renderValueType lhsTy} and {renderValueType rhsTy}"
 
@@ -1549,7 +1593,11 @@ def requireDeclaredValueType
     (stx : Syntax)
     (context : String)
     (expectedTy actualTy : ValueType) : CommandElabM Unit := do
-  unless actualTy == expectedTy || (isWordLikeValueType actualTy && isWordLikeValueType expectedTy) do
+  let involvesEnum := match expectedTy, actualTy with
+    | .enum _ _, _ | _, .enum _ _ => true
+    | _, _ => false
+  unless actualTy == expectedTy ||
+      (!involvesEnum && isWordLikeValueType actualTy && isWordLikeValueType expectedTy) do
     throwErrorAt stx
       s!"{context} expects {renderValueType expectedTy}, got {renderValueType actualTy}"
 
@@ -1596,6 +1644,7 @@ def customErrorRequiresDirectParamRef : ValueType → Bool
   | .uint256 | .int256 | .uint8 | .uint16 | .uintN _ | .intN _ | .bytesN _
   | .address | .bool | .bytes32 => false
   | .newtype _ baseType => customErrorRequiresDirectParamRef baseType
+  | .enum _ _ => false
   | _ => true
 
 def directParamRefName? (stx : Term) : Option String :=
@@ -1991,22 +2040,22 @@ partial def inferPureExprType
       classifyUnsignedWordArithmeticResultType stx "signed builtin arithmetic" lhsTy rhsTy
   | `(term| bitNot $a) | `(term| not $a) => do
       let ty ← inferPureExprType fields constDecls immutableDecls externalDecls params locals a visitingConstants
-      requireWordLikeType a "bitwise not" ty
+      requireWordOperatorType a "bitwise not" ty
       pure .uint256
   | `(term| shl $shift $value) | `(term| shr $shift $value) | `(term| sar $shift $value)
     | `(term| signextend $shift $value) => do
-      requireWordLikeType shift "shift" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals shift visitingConstants)
+      requireWordOperatorType shift "shift" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals shift visitingConstants)
       let valueTy ← inferPureExprType fields constDecls immutableDecls externalDecls params locals value visitingConstants
-      requireWordLikeType value "shift" valueTy
+      requireWordOperatorType value "shift" valueTy
       pure .uint256
   | `(term| byte $index $value) => do
-      requireWordLikeType index "byte index" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals index visitingConstants)
+      requireWordOperatorType index "byte index" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals index visitingConstants)
       let valueTy ← inferPureExprType fields constDecls immutableDecls externalDecls params locals value visitingConstants
-      requireWordLikeType value "byte value" valueTy
+      requireWordOperatorType value "byte value" valueTy
       pure .uint256
   | `(term| slt $a $b) | `(term| sgt $a $b) => do
-      requireWordLikeType a "signed ordering comparison" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals a visitingConstants)
-      requireWordLikeType b "signed ordering comparison" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals b visitingConstants)
+      requireWordOperatorType a "signed ordering comparison" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals a visitingConstants)
+      requireWordOperatorType b "signed ordering comparison" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals b visitingConstants)
       pure .bool
   | `(term| $a == $b) | `(term| $a != $b) => do
       let lhsTy ← inferPureExprType fields constDecls immutableDecls externalDecls params locals a visitingConstants
@@ -2024,11 +2073,11 @@ partial def inferPureExprType
       requireBoolType b "logical operator" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals b visitingConstants)
       pure .bool
   | `(term| logicalAnd $a $b) | `(term| logicalOr $a $b) => do
-      requireWordLikeType a "logical word operator" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals a visitingConstants)
-      requireWordLikeType b "logical word operator" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals b visitingConstants)
+      requireWordOperatorType a "logical word operator" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals a visitingConstants)
+      requireWordOperatorType b "logical word operator" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals b visitingConstants)
       pure .uint256
   | `(term| logicalNot $a) => do
-      requireWordLikeType a "logical word operator" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals a visitingConstants)
+      requireWordOperatorType a "logical word operator" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals a visitingConstants)
       pure .uint256
   | `(term| ! $a) => do
       requireBoolType a "logical not" (← inferPureExprType fields constDecls immutableDecls externalDecls params locals a visitingConstants)
@@ -2260,6 +2309,7 @@ partial def inferBindSourceType
       | .scalar .uint256 => pure .uint256
       | .scalar .int256 => pure .int256
       | .scalar (.newtype ntName (.uint256)) => pure (.newtype ntName .uint256)
+      | .scalar (.enum name memberCount) => pure (.enum name memberCount)
       | .scalar (.adt name maxFields) => pure (.adt name maxFields)
       | .scalar (.newtype _ (.address)) => throwErrorAt rhs s!"field '{f.name}' is Address-based newtype; use getStorageAddr"
       | .scalar .address => throwErrorAt rhs s!"field '{f.name}' is Address; use getStorageAddr"
@@ -2301,13 +2351,15 @@ partial def inferBindSourceType
       let f ← lookupStorageField fields (toString field.getId)
       match f.ty with
       | .mappingAddressToUint256 | .mappingUintToUint256 => pure .uint256
+      | .mappingAddressToEnum name memberCount | .mappingUintToEnum name memberCount =>
+          pure (.enum name memberCount)
       | .mappingStruct _ _ =>
           throwErrorAt rhs s!"field '{f.name}' is a struct-valued mapping; use structMember"
       | .mappingStruct2 _ _ _ =>
           throwErrorAt rhs s!"field '{f.name}' is a nested struct mapping; use structMember2"
-      | .mapping2AddressToAddressToUint256 =>
+      | .mapping2AddressToAddressToUint256 | .mapping2AddressToAddressToEnum _ _ =>
           throwErrorAt rhs s!"field '{f.name}' is a double mapping; use getMapping2"
-      | .mappingChain _ =>
+      | .mappingChain _ | .mappingChainEnum _ _ _ =>
           throwErrorAt rhs s!"field '{f.name}' uses {storageTypeMappingDepth? f.ty |>.getD 0} mapping keys; use getMappingN"
       | .dynamicArray _ =>
           throwErrorAt rhs s!"field '{f.name}' is a storage dynamic array; use getStorageArrayLength/getStorageArrayElement"
@@ -2317,13 +2369,15 @@ partial def inferBindSourceType
       let f ← lookupStorageField fields (toString field.getId)
       match f.ty with
       | .mappingAddressToUint256 | .mappingUintToUint256 => pure .address
+      | .mappingAddressToEnum _ _ | .mappingUintToEnum _ _ =>
+          throwErrorAt rhs s!"field '{f.name}' is enum-valued; use getMapping/getMappingUint"
       | .mappingStruct _ _ =>
           throwErrorAt rhs s!"field '{f.name}' is a struct-valued mapping; use structMember"
       | .mappingStruct2 _ _ _ =>
           throwErrorAt rhs s!"field '{f.name}' is a nested struct mapping; use structMember2"
-      | .mapping2AddressToAddressToUint256 =>
+      | .mapping2AddressToAddressToUint256 | .mapping2AddressToAddressToEnum _ _ =>
           throwErrorAt rhs s!"field '{f.name}' is a double mapping; use getMapping2"
-      | .mappingChain _ =>
+      | .mappingChain _ | .mappingChainEnum _ _ _ =>
           throwErrorAt rhs s!"field '{f.name}' uses {storageTypeMappingDepth? f.ty |>.getD 0} mapping keys; use getMappingN"
       | .dynamicArray _ =>
           throwErrorAt rhs s!"field '{f.name}' is a storage dynamic array; use getStorageArrayLength/getStorageArrayElement"
@@ -2334,6 +2388,7 @@ partial def inferBindSourceType
       let f ← lookupStorageField fields (toString field.getId)
       match f.ty with
       | .mapping2AddressToAddressToUint256 => pure .uint256
+      | .mapping2AddressToAddressToEnum name memberCount => pure (.enum name memberCount)
       | .mappingStruct2 _ _ _ =>
           throwErrorAt rhs s!"field '{f.name}' is a nested struct mapping; use structMember2"
       | .mappingStruct _ _ =>
@@ -2347,7 +2402,9 @@ partial def inferBindSourceType
       match storageTypeMappingKeyTypes? f.ty with
       | some keyTypes =>
           if keyTerms.size == keyTypes.length then
-            pure .uint256
+            match f.ty with
+            | .mappingChainEnum _ name memberCount => pure (.enum name memberCount)
+            | _ => pure .uint256
           else
             throwErrorAt rhs s!"field '{f.name}' expects {keyTypes.length} mapping keys, but getMappingN received {keyTerms.size}"
       | none =>
@@ -4680,7 +4737,7 @@ def translateBindSource
   | `(term| getStorage $field:ident) =>
       let f ← lookupStorageField fields (toString field.getId)
       match f.ty with
-      | .scalar .uint256 | .scalar .int256 | .scalar (.newtype _ .uint256) | .scalar (.adt _ _) =>
+      | .scalar .uint256 | .scalar .int256 | .scalar (.newtype _ .uint256) | .scalar (.enum _ _) | .scalar (.adt _ _) =>
           `(Compiler.CompilationModel.Expr.storage $(strTerm f.name))
       | .scalar .bool => throwErrorAt rhs s!"field '{f.name}' is Bool; encode as Uint256 and use getStorage"
       | .scalar .address | .scalar (.newtype _ .address) =>
@@ -4720,13 +4777,13 @@ def translateBindSource
   | `(term| getMapping $field:ident $key:term) =>
       let f ← lookupStorageField fields (toString field.getId)
       match f.ty with
-      | .mappingAddressToUint256 =>
+      | .mappingAddressToUint256 | .mappingAddressToEnum _ _ =>
           `(Compiler.CompilationModel.Expr.mapping $(strTerm f.name) $(← translatePureExprWithTypes fields constDecls immutableDecls params locals key))
-      | .mappingUintToUint256 =>
+      | .mappingUintToUint256 | .mappingUintToEnum _ _ =>
           `(Compiler.CompilationModel.Expr.mappingUint $(strTerm f.name) $(← translatePureExprWithTypes fields constDecls immutableDecls params locals key))
-      | .mapping2AddressToAddressToUint256 =>
+      | .mapping2AddressToAddressToUint256 | .mapping2AddressToAddressToEnum _ _ =>
           throwErrorAt rhs s!"field '{f.name}' is a double mapping; use getMapping2"
-      | .mappingChain _ =>
+      | .mappingChain _ | .mappingChainEnum _ _ _ =>
           throwErrorAt rhs s!"field '{f.name}' uses {storageTypeMappingDepth? f.ty |>.getD 0} mapping keys; use getMappingN"
       | .dynamicArray _ =>
           throwErrorAt rhs s!"field '{f.name}' is a storage dynamic array; use getStorageArrayLength/getStorageArrayElement"
@@ -4740,9 +4797,11 @@ def translateBindSource
           `(Compiler.CompilationModel.Expr.mapping $(strTerm f.name) $(← translatePureExprWithTypes fields constDecls immutableDecls params locals key))
       | .mappingUintToUint256 =>
           throwErrorAt rhs s!"field '{f.name}' is Uint256-keyed; use getMappingUintAddr"
-      | .mapping2AddressToAddressToUint256 =>
+      | .mappingAddressToEnum _ _ | .mappingUintToEnum _ _ =>
+          throwErrorAt rhs s!"field '{f.name}' is enum-valued; use getMapping/getMappingUint"
+      | .mapping2AddressToAddressToUint256 | .mapping2AddressToAddressToEnum _ _ =>
           throwErrorAt rhs s!"field '{f.name}' is a double mapping; use getMapping2"
-      | .mappingChain _ =>
+      | .mappingChain _ | .mappingChainEnum _ _ _ =>
           throwErrorAt rhs s!"field '{f.name}' uses {storageTypeMappingDepth? f.ty |>.getD 0} mapping keys; use getMappingN"
       | .dynamicArray _ =>
           throwErrorAt rhs s!"field '{f.name}' is a storage dynamic array; use getStorageArrayLength/getStorageArrayElement"
@@ -4752,13 +4811,13 @@ def translateBindSource
   | `(term| getMappingUint $field:ident $key:term) =>
       let f ← lookupStorageField fields (toString field.getId)
       match f.ty with
-      | .mappingUintToUint256 =>
+      | .mappingUintToUint256 | .mappingUintToEnum _ _ =>
           `(Compiler.CompilationModel.Expr.mappingUint $(strTerm f.name) $(← translatePureExprWithTypes fields constDecls immutableDecls params locals key))
-      | .mappingAddressToUint256 =>
+      | .mappingAddressToUint256 | .mappingAddressToEnum _ _ =>
           throwErrorAt rhs s!"field '{f.name}' is Address-keyed; use getMapping"
-      | .mapping2AddressToAddressToUint256 =>
+      | .mapping2AddressToAddressToUint256 | .mapping2AddressToAddressToEnum _ _ =>
           throwErrorAt rhs s!"field '{f.name}' is a double mapping; use getMapping2"
-      | .mappingChain _ =>
+      | .mappingChain _ | .mappingChainEnum _ _ _ =>
           throwErrorAt rhs s!"field '{f.name}' uses {storageTypeMappingDepth? f.ty |>.getD 0} mapping keys; use getMappingN"
       | .dynamicArray _ =>
           throwErrorAt rhs s!"field '{f.name}' is a storage dynamic array; use getStorageArrayLength/getStorageArrayElement"
@@ -4772,9 +4831,11 @@ def translateBindSource
           `(Compiler.CompilationModel.Expr.mappingUint $(strTerm f.name) $(← translatePureExprWithTypes fields constDecls immutableDecls params locals key))
       | .mappingAddressToUint256 =>
           throwErrorAt rhs s!"field '{f.name}' is Address-keyed; use getMappingAddr"
-      | .mapping2AddressToAddressToUint256 =>
+      | .mappingAddressToEnum _ _ | .mappingUintToEnum _ _ =>
+          throwErrorAt rhs s!"field '{f.name}' is enum-valued; use getMapping/getMappingUint"
+      | .mapping2AddressToAddressToUint256 | .mapping2AddressToAddressToEnum _ _ =>
           throwErrorAt rhs s!"field '{f.name}' is a double mapping; use getMapping2"
-      | .mappingChain _ =>
+      | .mappingChain _ | .mappingChainEnum _ _ _ =>
           throwErrorAt rhs s!"field '{f.name}' uses {storageTypeMappingDepth? f.ty |>.getD 0} mapping keys; use getMappingN"
       | .dynamicArray _ =>
           throwErrorAt rhs s!"field '{f.name}' is a storage dynamic array; use getStorageArrayLength/getStorageArrayElement"
@@ -4784,12 +4845,13 @@ def translateBindSource
   | `(term| getMappingWord $field:ident $key:term $wordOffset:num) =>
       let f ← lookupStorageField fields (toString field.getId)
       match f.ty with
-      | .mappingAddressToUint256 | .mappingUintToUint256 =>
+      | .mappingAddressToUint256 | .mappingUintToUint256
+        | .mappingAddressToEnum _ _ | .mappingUintToEnum _ _ =>
           `(Compiler.CompilationModel.Expr.mappingWord
               $(strTerm f.name)
               $(← translatePureExprWithTypes fields constDecls immutableDecls params locals key)
               $wordOffset)
-      | .mapping2AddressToAddressToUint256 =>
+      | .mapping2AddressToAddressToUint256 | .mapping2AddressToAddressToEnum _ _ =>
           throwErrorAt rhs s!"field '{f.name}' is a double mapping; use getMapping2Word"
       | .mappingStruct _ _ =>
           throwErrorAt rhs s!"field '{f.name}' is a struct-valued mapping; use structMember"
@@ -4798,12 +4860,12 @@ def translateBindSource
       | .dynamicArray _ =>
           throwErrorAt rhs s!"field '{f.name}' is a storage dynamic array; use getStorageArrayLength/getStorageArrayElement"
       | .scalar _ => throwErrorAt rhs s!"field '{f.name}' is not a mapping"
-      | .mappingChain _ =>
+      | .mappingChain _ | .mappingChainEnum _ _ _ =>
           throwErrorAt rhs s!"field '{f.name}' uses {storageTypeMappingDepth? f.ty |>.getD 0} mapping keys; use getMappingN"
   | `(term| getMapping2 $field:ident $key1:term $key2:term) =>
       let f ← lookupStorageField fields (toString field.getId)
       match f.ty with
-      | .mapping2AddressToAddressToUint256 =>
+      | .mapping2AddressToAddressToUint256 | .mapping2AddressToAddressToEnum _ _ =>
           `(Compiler.CompilationModel.Expr.mapping2
               $(strTerm f.name)
               $(← translatePureExprWithTypes fields constDecls immutableDecls params locals key1)
diff --git a/Verity/Macro/Translate/Parsing.lean b/Verity/Macro/Translate/Parsing.lean
index 3b8325f32..a8088b8f6 100644
--- a/Verity/Macro/Translate/Parsing.lean
+++ b/Verity/Macro/Translate/Parsing.lean
@@ -220,6 +220,19 @@ def parseNewtype (stx : Syntax) : CommandElabM NewtypeDecl := do
       }
   | _ => throwErrorAt stx "invalid type declaration"
 
+def parseEnumDecl (stx : Syntax) : CommandElabM EnumDecl := do
+  match stx with
+  | `(verityEnumDecl| enum $name:ident { $[$members:ident],* }) =>
+      if members.size > 256 then
+        throwErrorAt name s!"enum '{toString name.getId}' has {members.size} members; Solidity enums support at most 256"
+      else
+        let names := members.map (fun m => toString m.getId)
+        for member in members do
+          if (names.filter (fun name => name == toString member.getId)).size > 1 then
+            throwErrorAt member s!"duplicate enum member '{toString member.getId}'"
+        pure { ident := name, name := toString name.getId, members }
+  | _ => throwErrorAt stx "invalid enum declaration"
+
 def parseStructDecl (newtypes : Array NewtypeDecl) (structDecls : Array StructDecl) (stx : Syntax) : CommandElabM StructDecl := do
   match stx with
   | `(verityStructDecl| struct $name:ident where $[$fields:verityParam],*) =>
diff --git a/Verity/Macro/Types.lean b/Verity/Macro/Types.lean
index 32523c76c..ff81894f5 100644
--- a/Verity/Macro/Types.lean
+++ b/Verity/Macro/Types.lean
@@ -31,6 +31,7 @@ inductive ValueType where
   | tuple (elemTys : List ValueType)
   | unit
   | newtype (name : String) (baseType : ValueType)  -- Semantic newtype; erased to baseType (#1727 Steps 3b/3c)
+  | enum (name : String) (memberCount : Nat) -- Solidity enum; erased to uint8
   | struct (name : String) (fields : List (String × ValueType)) -- Named ABI tuple with executable field access (#1750)
   | adt (name : String) (maxFields : Nat)  -- User-defined ADT (tagged union); maxFields = max variant field count (#1727 Step 5b)
   deriving Repr, BEq
@@ -52,9 +53,13 @@ inductive StorageType where
   | scalar (ty : ValueType)
   | dynamicArray (elemTy : Compiler.CompilationModel.StorageArrayElemType)
   | mappingAddressToUint256
+  | mappingAddressToEnum (name : String) (memberCount : Nat)
   | mapping2AddressToAddressToUint256
+  | mapping2AddressToAddressToEnum (name : String) (memberCount : Nat)
   | mappingUintToUint256
+  | mappingUintToEnum (name : String) (memberCount : Nat)
   | mappingChain (keyTypes : List MappingKeyType)
+  | mappingChainEnum (keyTypes : List MappingKeyType) (name : String) (memberCount : Nat)
   | mappingStruct (keyType : MappingKeyType) (members : List StructMemberDecl)
   | mappingStruct2 (outerKey : MappingKeyType) (innerKey : MappingKeyType) (members : List StructMemberDecl)
   deriving BEq
@@ -158,6 +163,13 @@ structure NewtypeDecl where
   ident : Ident
   name : String
   baseType : ValueType
+  enumMembers : Array Ident := #[]
+
+/-- A Solidity-compatible enum. Members are encoded in declaration order as uint8. -/
+structure EnumDecl where
+  ident : Ident
+  name : String
+  members : Array Ident
 
 /-- A named ABI struct declared in the `verity_contract` body.
     It elaborates to a Lean `structure` for executable tests, while the compiler
@@ -314,7 +326,8 @@ partial def valueTypeFromSyntax
     (newtypes : Array NewtypeDecl)
     (structDecls : Array StructDecl)
     (adtDecls : Array AdtDecl)
-    (ty : Term) : CommandElabM ValueType := do
+    (ty : Term)
+    (enumDecls : Array EnumDecl := #[]) : CommandElabM ValueType := do
   let ty := stripParens ty
   let (arrowArgs, _arrowResult) ← collectArrowChainTypes ty
   if !arrowArgs.isEmpty then
@@ -331,20 +344,20 @@ partial def valueTypeFromSyntax
   | `(term| String) => pure .string
   | `(term| Bytes) => pure .bytes
   | `(term| Array $elemTy:term) =>
-      let elem ← valueTypeFromSyntax newtypes structDecls adtDecls elemTy
+      let elem ← valueTypeFromSyntax newtypes structDecls adtDecls elemTy enumDecls
       match elem with
       | .unit => throwErrorAt ty "unsupported type '{ty}'; Array Unit is not allowed"
       | .array _ => throwErrorAt ty "unsupported type '{ty}'; nested arrays are not supported"
       | _ => pure (.array elem)
   | `(term| FixedArray $elemTy:term $size:num) =>
-      let elem ← valueTypeFromSyntax newtypes structDecls adtDecls elemTy
+      let elem ← valueTypeFromSyntax newtypes structDecls adtDecls elemTy enumDecls
       let n ← natFromSyntax size
       match elem with
       | .unit => throwErrorAt ty "unsupported type '{ty}'; FixedArray Unit is not allowed"
       | .array _ => throwErrorAt ty "unsupported type '{ty}'; FixedArray of dynamic Array is not supported"
       | _ => pure (.fixedArray elem n)
   | `(term| Tuple [ $[$elemTys:term],* ]) =>
-      let elems ← elemTys.mapM (valueTypeFromSyntax newtypes structDecls adtDecls)
+      let elems ← elemTys.mapM (fun elemTy => valueTypeFromSyntax newtypes structDecls adtDecls elemTy enumDecls)
       if elems.size < 2 then
         throwErrorAt ty "tuple types must have at least 2 elements"
       pure (.tuple elems.toList)
@@ -363,17 +376,21 @@ partial def valueTypeFromSyntax
       else
       -- Try resolving as a user-defined newtype (#1727, Axis 1 Steps 3a/3b)
       match newtypes.find? (fun nt => nt.name == tyName) with
-      | some nt => pure (.newtype nt.name nt.baseType)
+      | some nt =>
+          if nt.enumMembers.isEmpty then pure (.newtype nt.name nt.baseType)
+          else pure (.enum nt.name nt.enumMembers.size)
       | none =>
         -- Try resolving as a user-defined ADT (#1727, Axis 1 Step 5b)
         match structDecls.find? (fun s => s.name == tyName) with
         | some decl => pure (.struct decl.name (structValueTypeFields decl))
         | none =>
-          match adtDecls.find? (fun a => a.name == tyName) with
+          match enumDecls.find? (fun e => e.name == tyName) with
+          | some decl => pure (.enum decl.name decl.members.size)
+          | none => match adtDecls.find? (fun a => a.name == tyName) with
           | some decl =>
               let maxFields := decl.variants.foldl (fun acc v => max acc v.fields.size) 0
               pure (.adt decl.name maxFields)
-          | none => throwErrorAt ty "unsupported type '{ty}'; 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"
+          | none => throwErrorAt ty "unsupported type '{ty}'; expected a built-in type or a user-defined enum, struct, newtype, or inductive type"
   | _ =>
       throwErrorAt ty "unsupported type '{ty}'; 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"
 
diff --git a/artifacts/macro_property_tests/PropertyMacroEnumUsage.t.sol b/artifacts/macro_property_tests/PropertyMacroEnumUsage.t.sol
new file mode 100644
index 000000000..facd6d934
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyMacroEnumUsage.t.sol
@@ -0,0 +1,87 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyMacroEnumUsageTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/EnumFeatureTest.lean
+ */
+contract PropertyMacroEnumUsageTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("MacroEnumUsage");
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: identity returns the direct parameter value
+    function testAuto_Identity_ReturnsDirectParam() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("identity(uint8)", uint8(0)));
+        require(ok, "identity reverted unexpectedly");
+        assertEq(ret.length, 32, "identity ABI return length mismatch (expected 32 bytes)");
+        uint8 actual = abi.decode(ret, (uint8));
+        assertEq(actual, uint8(0), "identity should preserve the expected value");
+    }
+    // Property 2: TODO decode and assert `active` result
+    function testTODO_Active_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("active()"));
+        require(ok, "active reverted unexpectedly");
+        assertEq(ret.length, 32, "active ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 3: TODO decode and assert `castStatus` result
+    function testTODO_CastStatus_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("castStatus(uint256)", uint256(1)));
+        require(ok, "castStatus reverted unexpectedly");
+        assertEq(ret.length, 32, "castStatus ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 4: setStatus has no unexpected revert
+    function testAuto_SetStatus_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("setStatus(uint8)", uint8(0)));
+        require(ok, "setStatus reverted unexpectedly");
+    }
+    // Property 5: announceStatus has no unexpected revert
+    function testAuto_AnnounceStatus_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("announceStatus(uint8)", uint8(0)));
+        require(ok, "announceStatus reverted unexpectedly");
+    }
+    // Property 6: getStatus reads storage slot 0 and decodes the result
+    function testAuto_GetStatus_ReadsConfiguredStorage() public {
+        uint8 expected = uint8(0);
+        vm.store(target, bytes32(uint256(0)), bytes32(uint256(expected)));
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("getStatus()"));
+        require(ok, "getStatus reverted unexpectedly");
+        assertEq(ret.length, 32, "getStatus ABI return length mismatch (expected 32 bytes)");
+        uint8 actual = abi.decode(ret, (uint8));
+        assertEq(actual, expected, "getStatus should return storage slot 0");
+    }
+    // Property 7: setStatusAt has no unexpected revert
+    function testAuto_SetStatusAt_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("setStatusAt(uint256,uint8)", uint256(1), uint8(0)));
+        require(ok, "setStatusAt reverted unexpectedly");
+    }
+    // Property 8: getStatusAt reads the configured mapping value
+    function testAuto_GetStatusAt_ReadsConfiguredMapping() public {
+        uint8 expected = uint8(0);
+        vm.store(target, _mappingSlot(bytes32(uint256(uint256(1))), 1), bytes32(uint256(expected)));
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("getStatusAt(uint256)", uint256(1)));
+        require(ok, "getStatusAt reverted unexpectedly");
+        assertEq(ret.length, 32, "getStatusAt ABI return length mismatch (expected 32 bytes)");
+        uint8 actual = abi.decode(ret, (uint8));
+        assertEq(actual, expected, "getStatusAt should decode the configured mapping value");
+    }
+}
diff --git a/artifacts/verification_status.json b/artifacts/verification_status.json
index 385e4f567..8b54163d1 100644
--- a/artifacts/verification_status.json
+++ b/artifacts/verification_status.json
@@ -10,9 +10,9 @@
   "schema_version": 1,
   "tests": {
     "differential_total": 110000,
-    "foundry_functions": 525,
+    "foundry_functions": 528,
     "property_functions": 239,
-    "suites": 51
+    "suites": 52
   },
   "theorems": {
     "categories": 13,
diff --git a/docs/parity/erc4337.md b/docs/parity/erc4337.md
index 1a567731f..f5bd0b97c 100644
--- a/docs/parity/erc4337.md
+++ b/docs/parity/erc4337.md
@@ -139,9 +139,9 @@ issues [#1724](https://github.com/lfglabs-dev/verity/issues/1724),
 
 | Construct | Signature | Verity | Notes |
 | --- | --- | --- | --- |
-| enum | `PostOpMode { opSucceeded, opReverted, postOpReverted }` | ❌ | No `enum`. Workaround: `uint8` constants. |
+| enum | `PostOpMode { opSucceeded, opReverted, postOpReverted }` | ✅ | Native uint8-backed enum declarations, members, and checked casts (#2088). |
 | fn | `validatePaymasterUserOp(PackedUserOperation calldata, bytes32, uint256) returns (bytes, uint256)` | 🚧 | `bytes` return only lands as raw memory. |
-| fn | `postOp(PostOpMode, bytes calldata, uint256, uint256)` | ❌ | Enum arg. |
+| fn | `postOp(PostOpMode, bytes calldata, uint256, uint256)` | ✅ | Enum arguments erase to `uint8` in the ABI. |
 
 ## core/BasePaymaster.sol
 
diff --git a/docs/parity/lido.md b/docs/parity/lido.md
index 7e6ad0146..8a1752aa2 100644
--- a/docs/parity/lido.md
+++ b/docs/parity/lido.md
@@ -44,7 +44,7 @@ Constructs outside that scope are still listed so gaps can be counted honestly.
 
 | Construct | Signature | Status | Notes / needed feature |
 |---|---|---|---|
-| enum `StakingModuleStatus` | `{Active, DepositsPaused, Stopped}` | ❌ | `enum` — workaround: encode as `Uint8` (SRTypes docs literally say "stored as `uint8` to avoid problems") |
+| enum `StakingModuleStatus` | `{Active, DepositsPaused, Stopped}` | ✅ | Native uint8-backed enum declarations, members, and checked casts (#2088). |
 
 ### 1.2 Interfaces (referenced, not implemented)
 
@@ -85,7 +85,7 @@ Constructs outside that scope are still listed so gaps can be counted honestly.
 | `StakingModuleFeesSet` | `(uint256 indexed, uint256, uint256, address)` | ✅ | |
 | `StakingModuleMaxDepositsPerBlockSet` | `(uint256 indexed, uint256, address)` | ✅ | |
 | `StakingModuleMinDepositBlockDistanceSet` | `(uint256 indexed, uint256, address)` | ✅ | |
-| `StakingModuleStatusSet` | `(uint256 indexed, StakingModuleStatus, address)` | ❌ | enum payload — workaround: emit as `uint8` |
+| `StakingModuleStatusSet` | `(uint256 indexed, StakingModuleStatus, address)` | ✅ | Enum event payloads erase to `uint8` in the ABI. |
 | `WithdrawalCredentialsSet` | `(bytes32, address)` | ✅ | |
 | `StakingRouterETHDeposited` | `(uint256 indexed, uint256)` | ✅ | |
 | `DepositableEthReceived` | `(uint256)` | ✅ | |
@@ -168,12 +168,12 @@ For brevity: `external onlyRole(X)` in every management function collapses into
 | `getStakingModule(uint256) view returns (StakingModule)` | external | ❌ | same struct |
 | `getStakingModulesCount() view returns (uint256)` | external | ✅ | |
 | `hasStakingModule(uint256) view returns (bool)` | public | ✅ | |
-| `getStakingModuleStatus(uint256) view returns (StakingModuleStatus)` | public | ❌ | enum return |
+| `getStakingModuleStatus(uint256) view returns (StakingModuleStatus)` | public | ✅ | Enum returns erase to `uint8` in the ABI. |
 | `getContractVersion() view returns (uint256)` | external | ✅ | |
 | `getStakingModuleSummary` / `getNodeOperatorSummary` | external view | ✅ | scalar tuple returns |
 | `getAllStakingModuleDigests / getStakingModuleDigests(uint256[])` | external view | ❌ | nested-struct memory arrays |
 | `getAllNodeOperatorDigests / getNodeOperatorDigests(...)` | external view | 🚧 | flatten to tuple[] |
-| `setStakingModuleStatus(uint256, StakingModuleStatus)` | external `onlyRole` | ❌ | enum arg |
+| `setStakingModuleStatus(uint256, StakingModuleStatus)` | external `onlyRole` | ✅ | Enum parameters and storage values are supported. |
 | `getStakingModuleIsStopped / IsDepositsPaused / IsActive` | external view returns (bool) | ❌ | derived from enum status |
 | `getStakingModuleNonce / LastDepositBlock / MinDepositBlockDistance / MaxDepositsPerBlock` | external view returns (uint256) | 🚧 | value stored as `uint64`; cast up |
 | `getStakingModuleActiveValidatorsCount(uint256) view returns (uint256, uint256)` | external | ✅ | |
diff --git a/scripts/generate_macro_property_tests.py b/scripts/generate_macro_property_tests.py
index b582e0cff..61a617bf3 100644
--- a/scripts/generate_macro_property_tests.py
+++ b/scripts/generate_macro_property_tests.py
@@ -47,6 +47,7 @@
 NEWTYPE_RE = re.compile(
     r"^\s*([A-Z][A-Za-z0-9_]*)\s*:\s*([A-Za-z0-9_]+)\s*$",
 )
+ENUM_RE = re.compile(r"^\s*enum\s+([A-Z][A-Za-z0-9_]*)\s*\{[^}]+\}\s*$")
 STRUCT_RE = re.compile(r"^\s*struct\s+([A-Za-z_][A-Za-z0-9_]*)\s+where\s*(.*?)\s*$")
 INTERFACE_RE = re.compile(r"^\s*interface\s+([A-Za-z_][A-Za-z0-9_]*)\s+where\s*$")
 STORAGE_RE = re.compile(
@@ -315,6 +316,7 @@ def parse_contracts(text: str, source: Path) -> dict[str, ContractDecl]:
     current_body: list[str] = []
     guard_pending = False
     in_types_block = False
+    in_enums_block = False
     in_storage_block = False
     in_constants_block = False
     in_immutables_block = False
@@ -348,7 +350,7 @@ 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_constructor, current_storage_slots, current_transient_slots, current_storage_types, current_newtypes, current_structs, current_constants, current_immutables, current_functions, in_types_block, in_enums_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()
@@ -377,6 +379,7 @@ def flush_current() -> None:
         current_functions = []
         current_struct_block_comment = False
         in_types_block = False
+        in_enums_block = False
         in_storage_block = False
         in_constants_block = False
         in_immutables_block = False
@@ -424,6 +427,7 @@ def flush_current() -> None:
 
         if line.strip() == "types":
             in_types_block = True
+            in_enums_block = False
             in_storage_block = False
             in_constants_block = False
             in_immutables_block = False
@@ -440,9 +444,31 @@ def flush_current() -> None:
                 in_types_block = False
                 # fall through to check other sections
 
+        if line.strip() == "enums":
+            in_types_block = False
+            in_enums_block = True
+            in_storage_block = False
+            in_constants_block = False
+            in_immutables_block = False
+            pending_storage_lines = []
+            continue
+
+        if in_enums_block:
+            stripped = line.strip()
+            enum_decl = ENUM_RE.match(stripped)
+            if enum_decl:
+                # Preserve enum-ness long enough to choose an in-range fixture;
+                # it still erases to uint8 in generated Solidity signatures.
+                current_newtypes[enum_decl.group(1)] = "EnumUint8"
+                continue
+            if stripped:
+                in_enums_block = False
+                # fall through to check other sections
+
         if line.strip() == "storage":
             flush_struct()
             in_types_block = False
+            in_enums_block = False
             in_storage_block = True
             in_constants_block = False
             in_immutables_block = False
@@ -686,6 +712,8 @@ def _sol_type(lean_ty: str) -> str:
         return "int256"
     if ty == "Uint8":
         return "uint8"
+    if ty == "EnumUint8":
+        return "uint8"
     if ty == "Address":
         return "address"
     if ty == "Bool":
@@ -734,6 +762,8 @@ def _example_value(lean_ty: str) -> str:
         return "int256(1)"
     if ty == "Uint8":
         return "uint8(27)"
+    if ty == "EnumUint8":
+        return "uint8(0)"
     if ty == "Address":
         return "alice"
     if ty == "Bool":
@@ -976,7 +1006,7 @@ def _resolve_value_expr(
                 if lhs is not None and rhs is not None:
                     return f"({lhs} {sol_op} {rhs})"
 
-    if lean_type in {"Uint256", "Int256", "Uint8"}:
+    if lean_type in {"Uint256", "Int256", "Uint8", "EnumUint8"}:
         for lean_op, sol_op in {"/": "/", "%": "%"}.items():
             math_match = re.fullmatch(rf"(.+)\s*{re.escape(lean_op)}\s*(.+)", expr)
             if math_match is None:
@@ -1016,7 +1046,7 @@ def _resolve_value_expr(
             "shl": "<<",
             "shr": ">>",
         }
-        if op in op_map and len(args) == 2 and lean_type in {"Uint256", "Int256", "Uint8"}:
+        if op in op_map and len(args) == 2 and lean_type in {"Uint256", "Int256", "Uint8", "EnumUint8"}:
             lhs = _resolve_value_expr(
                 contract, args[0], lean_type, constructor_examples, seen, local_values
             )
@@ -1061,7 +1091,7 @@ def _resolve_value_expr(
                         folded = rhs_lit << lhs_lit
                     else:
                         folded = rhs_lit >> lhs_lit
-                    if lean_type in {"Uint256", "Uint8"}:
+                    if lean_type in {"Uint256", "Uint8", "EnumUint8"}:
                         return _format_uint_literal(folded)
                     return _format_int_literal(folded)
                 if op in {"shl", "shr"}:
@@ -1115,7 +1145,7 @@ def _resolve_value_expr(
                 value_lit = _parse_literal_int(value)
                 if byte_index_lit is not None and value_lit is not None:
                     return _format_uint_literal(_signextend_literal(byte_index_lit, value_lit))
-        if op in {"min", "max"} and len(args) == 2 and lean_type in {"Uint256", "Int256", "Uint8"}:
+        if op in {"min", "max"} and len(args) == 2 and lean_type in {"Uint256", "Int256", "Uint8", "EnumUint8"}:
             lhs = _resolve_value_expr(
                 contract, args[0], lean_type, constructor_examples, seen, local_values
             )
@@ -1206,7 +1236,7 @@ def _resolve_value_expr(
 
 def _return_shape_assertion(lean_ty: str, fn_name: str) -> str:
     ty = _normalize_type(lean_ty)
-    if (ty in {"Uint256", "Int256", "Uint8", "Address", "Bool", "Bytes32"}
+    if (ty in {"Uint256", "Int256", "Uint8", "EnumUint8", "Address", "Bool", "Bytes32"}
             or re.fullmatch(r"(?:Uint|Int|Bytes)\d+", ty)):
         return (
             f'        assertEq(ret.length, 32, "{fn_name} ABI return length mismatch (expected 32 bytes)");'
@@ -1231,7 +1261,7 @@ def _return_shape_assertion(lean_ty: str, fn_name: str) -> str:
 
 def _storage_word_expr(lean_ty: str, value_expr: str) -> str:
     ty = _normalize_type(lean_ty)
-    if ty in {"Uint256", "Int256", "Uint8"}:
+    if ty in {"Uint256", "Int256", "Uint8", "EnumUint8"}:
         return f"bytes32(uint256({value_expr}))"
     if ty == "Bool":
         return f"bytes32(uint256({value_expr} ? 1 : 0))"
@@ -1244,7 +1274,7 @@ def _storage_word_expr(lean_ty: str, value_expr: str) -> str:
 
 def _single_word_uint_expr(lean_ty: str, value_expr: str) -> str | None:
     ty = _normalize_type(lean_ty)
-    if ty in {"Uint256", "Int256", "Uint8"}:
+    if ty in {"Uint256", "Int256", "Uint8", "EnumUint8"}:
         return f"uint256({value_expr})"
     if ty == "Bool":
         return f"({value_expr} ? 1 : 0)"
@@ -1257,7 +1287,7 @@ def _single_word_uint_expr(lean_ty: str, value_expr: str) -> str | None:
 
 def _literal_expr(value: str, lean_ty: str) -> str | None:
     ty = _normalize_type(lean_ty)
-    if ty in {"Uint256", "Uint8"} and re.fullmatch(r"(0x[0-9A-Fa-f]+|[0-9]+)", value):
+    if ty in {"Uint256", "Uint8", "EnumUint8"} and re.fullmatch(r"(0x[0-9A-Fa-f]+|[0-9]+)", value):
         return value
     if ty == "Int256" and re.fullmatch(r"-?(0x[0-9A-Fa-f]+|[0-9]+)", value):
         return value if not value.startswith("-") else f"int256({value})"
@@ -1907,7 +1937,7 @@ def _mapping_key_expr(param: ParamDecl, value_expr: str) -> str:
     ty = _normalize_type(param.lean_type)
     if ty == "Address":
         return f"bytes32(uint256(uint160({value_expr})))"
-    if ty in {"Uint256", "Uint8", "Bytes32"}:
+    if ty in {"Uint256", "Uint8", "EnumUint8", "Bytes32"}:
         return f"bytes32(uint256({value_expr}))"
     raise ValueError(f"unsupported Lean key type for generated mapping setup: {ty!r}")
 
diff --git a/scripts/test_generate_macro_property_tests.py b/scripts/test_generate_macro_property_tests.py
index 5adc0afe0..421a97538 100644
--- a/scripts/test_generate_macro_property_tests.py
+++ b/scripts/test_generate_macro_property_tests.py
@@ -271,6 +271,24 @@ def test_parse_contracts_skips_higher_order_helpers(self) -> None:
         rendered = gen.render_contract_test(parsed["FunctionPointerParamSmoke"])
         self.assertNotIn("apply(", rendered)
 
+    def test_enum_fixtures_erase_to_uint8_and_stay_in_range(self) -> None:
+        src = textwrap.dedent(
+            """
+            verity_contract EnumConsumer where
+              enums
+                enum Only { Sole }
+
+              storage
+
+              function identity (value : Only) : Only := do
+                return value
+            """
+        )
+        parsed = gen.parse_contracts(src, gen.ROOT / "Contracts/Smoke.lean")
+        rendered = gen.render_contract_test(parsed["EnumConsumer"])
+        self.assertIn('identity(uint8)", uint8(0)', rendered)
+        self.assertNotIn("uint8(27)", rendered)
+
 
 class RenderTests(unittest.TestCase):
     def test_render_unit_and_non_unit_tests(self) -> None:
diff --git a/test/EnumFeature.t.sol b/test/EnumFeature.t.sol
new file mode 100644
index 000000000..e16ae0f12
--- /dev/null
+++ b/test/EnumFeature.t.sol
@@ -0,0 +1,77 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "forge-std/Test.sol";
+import "./yul/YulTestBase.sol";
+
+contract EnumFeatureReference {
+    enum Status { Pending, Active, Closed }
+
+    Status internal status;
+    mapping(uint256 => Status) internal statuses;
+    event StatusChanged(Status indexed previous, Status current);
+
+    function identity(Status value) external pure returns (Status) { return value; }
+    function active() external pure returns (Status) { return Status.Active; }
+    function castStatus(uint256 value) external pure returns (Status) { return Status(value); }
+    function setStatus(Status value) external { status = value; }
+    function announceStatus(Status value) external { emit StatusChanged(value, value); }
+    function getStatus() external view returns (Status) { return status; }
+    function setStatusAt(uint256 key, Status value) external { statuses[key] = value; }
+    function getStatusAt(uint256 key) external view returns (Status) { return statuses[key]; }
+}
+
+contract EnumFeatureTest is Test, YulTestBase {
+    address internal enumFeature;
+    EnumFeatureReference internal referenceContract;
+
+    function setUp() public {
+        enumFeature = deployCompiledVerityModule(
+            "Contracts.Smoke.EnumFeatureTest",
+            "MacroEnumUsage",
+            _smokeYulDir()
+        );
+        referenceContract = new EnumFeatureReference();
+    }
+
+    function _assertCallParity(bytes memory payload) internal {
+        (bool yulSuccess, bytes memory yulData) = enumFeature.call(payload);
+        (bool refSuccess, bytes memory refData) = address(referenceContract).call(payload);
+        assertEq(yulSuccess, refSuccess, "success mismatch");
+        assertEq(yulData, refData, "return/revert payload mismatch");
+    }
+
+    function _assertEnumParamRevert(bytes memory payload) internal {
+        (bool yulSuccess, bytes memory yulData) = enumFeature.call(payload);
+        (bool refSuccess, bytes memory refData) = address(referenceContract).call(payload);
+        assertFalse(yulSuccess, "generated enum parameter unexpectedly accepted");
+        assertFalse(refSuccess, "reference enum parameter unexpectedly accepted");
+        assertEq(yulData, abi.encodeWithSignature("Panic(uint256)", 0x21), "generated panic mismatch");
+        assertEq(refData, bytes(""), "reference ABI decoder revert mismatch");
+    }
+
+    function testMembersParamsReturnsAndCastParity() public {
+        _assertCallParity(abi.encodeWithSignature("active()"));
+        _assertCallParity(abi.encodeWithSignature("identity(uint8)", uint8(2)));
+        _assertEnumParamRevert(abi.encodeWithSignature("identity(uint8)", uint8(3)));
+        _assertCallParity(abi.encodeWithSignature("castStatus(uint256)", 0));
+        _assertCallParity(abi.encodeWithSignature("castStatus(uint256)", 2));
+        _assertCallParity(abi.encodeWithSignature("castStatus(uint256)", 3));
+        _assertCallParity(abi.encodeWithSignature("castStatus(uint256)", type(uint256).max));
+        _assertEnumParamRevert(abi.encodeWithSelector(bytes4(keccak256("identity(uint8)")), uint256(0x100)));
+    }
+
+    function testStorageAndMappingParity() public {
+        _assertCallParity(abi.encodeWithSignature("setStatus(uint8)", uint8(2)));
+        _assertCallParity(abi.encodeWithSignature("getStatus()"));
+        _assertCallParity(abi.encodeWithSignature("setStatusAt(uint256,uint8)", 7, uint8(1)));
+        _assertCallParity(abi.encodeWithSignature("getStatusAt(uint256)", 7));
+        assertEq(vm.load(enumFeature, bytes32(uint256(0))), vm.load(address(referenceContract), bytes32(uint256(0))));
+        bytes32 mapSlot = keccak256(abi.encode(uint256(7), uint256(1)));
+        assertEq(vm.load(enumFeature, mapSlot), vm.load(address(referenceContract), mapSlot));
+    }
+
+    function testEnumEventParamParity() public {
+        _assertCallParity(abi.encodeWithSignature("announceStatus(uint8)", uint8(1)));
+    }
+}