diff --git a/Compiler/CompilationModelFeatureTest.lean b/Compiler/CompilationModelFeatureTest.lean
index 439440340..81504e4d6 100644
--- a/Compiler/CompilationModelFeatureTest.lean
+++ b/Compiler/CompilationModelFeatureTest.lean
@@ -1881,6 +1881,9 @@ open Verity.EVM.Uint256
 verity_contract MacroEventTrace where
   storage
 
+  event_defs
+    event Transfer(@indexed amount : Uint256, total : Uint256)
+
   function emitNamed (amount : Uint256, bonus : Uint256) : Unit := do
     emit "Transfer" [amount, add amount bonus]
 
@@ -1909,6 +1912,17 @@ def emitDynamicLogModelUsesStmtRawLog : Bool :=
 
 example : emitDynamicLogModelUsesStmtRawLog = true := by native_decide
 
+def eventTraceSpecCarriesEventMetadata : Bool :=
+  match MacroEventTrace.spec.events with
+  | [{ name := "Transfer",
+       params := [
+        { name := "amount", ty := ParamType.uint256, kind := EventParamKind.indexed },
+        { name := "total", ty := ParamType.uint256, kind := EventParamKind.unindexed }
+       ] }] => true
+  | _ => false
+
+example : eventTraceSpecCarriesEventMetadata = true := by native_decide
+
 def emitNamedExecutableAppendsNamedEvent : Bool :=
   match MacroEventTrace.emitNamed 7 5 Verity.defaultState with
   | .success () state =>
@@ -4082,6 +4096,8 @@ set_option maxRecDepth 4096 in
     MacroImmutableSmoke.typedImmutableExecutableReadsConvertedValues
   expectTrue "macro emit lowers to Stmt.emit"
     MacroEventTraceSmoke.emitNamedModelUsesStmtEmit
+  expectTrue "macro event declarations populate CompilationModel event metadata"
+    MacroEventTraceSmoke.eventTraceSpecCarriesEventMetadata
   expectTrue "macro rawLog lowers to Stmt.rawLog with dynamic topic expressions"
     MacroEventTraceSmoke.emitDynamicLogModelUsesStmtRawLog
   expectTrue "macro emit executable path appends the named event trace"
diff --git a/Verity/Macro/Elaborate.lean b/Verity/Macro/Elaborate.lean
index c61bec24d..bb4d7e013 100644
--- a/Verity/Macro/Elaborate.lean
+++ b/Verity/Macro/Elaborate.lean
@@ -13,7 +13,7 @@ set_option hygiene false
 
 @[command_elab verityContractCmd]
 def elabVerityContract : CommandElab := fun stx => do
-  let (contractName, _newtypeDecls, structDecls, adtDecls, fields, errorDecls, constDecls, immutableDecls, externalDecls, ctor, functions, storageNamespace) ← parseContractSyntax stx
+  let (contractName, _newtypeDecls, structDecls, adtDecls, fields, errorDecls, eventDecls, constDecls, immutableDecls, externalDecls, ctor, functions, storageNamespace) ← parseContractSyntax stx
 
   validateGeneratedDefNamesPublic fields constDecls immutableDecls functions
   validateConstantDeclsPublic constDecls
@@ -48,7 +48,7 @@ def elabVerityContract : CommandElab := fun stx => do
         elabCommand cmd
       elabCommand (← mkBridgeCommand fn.ident)
 
-    elabCommand (← mkSpecCommandPublic (toString contractName.getId) fields errorDecls constDecls immutableDecls externalDecls ctor functions adtDecls storageNamespace)
+    elabCommand (← mkSpecCommandPublic (toString contractName.getId) fields errorDecls eventDecls constDecls immutableDecls externalDecls ctor functions adtDecls storageNamespace)
 
     let findIdxSimpCmds ← mkFindIdxFieldSimpCommandsPublic contractName fields
     for cmd in findIdxSimpCmds do
diff --git a/Verity/Macro/Syntax.lean b/Verity/Macro/Syntax.lean
index ef7300493..80c458321 100644
--- a/Verity/Macro/Syntax.lean
+++ b/Verity/Macro/Syntax.lean
@@ -8,6 +8,8 @@ declare_syntax_cat verityStorageField
 declare_syntax_cat verityStructMember
 declare_syntax_cat verityParam
 declare_syntax_cat verityError
+declare_syntax_cat verityEventParam
+declare_syntax_cat verityEvent
 declare_syntax_cat verityConstant
 declare_syntax_cat verityImmutable
 declare_syntax_cat verityExternal
@@ -33,6 +35,9 @@ syntax "MappingStruct(" term "," "[" sepBy(verityStructMember, ",") "]" ")" : te
 syntax "MappingStruct2(" term "," term "," "[" sepBy(verityStructMember, ",") "]" ")" : term
 syntax ident " : " term : verityParam
 syntax "error " ident "(" sepBy(term, ",") ")" : verityError
+syntax ident " : " term : verityEventParam
+syntax "@indexed " ident " : " term : verityEventParam
+syntax "event " ident "(" sepBy(verityEventParam, ",") ")" : verityEvent
 syntax ident " : " term:max " := " term:max : verityConstant
 syntax ident " : " term:max " := " term:max : verityImmutable
 syntax "external " ident "(" sepBy(term, ",") ")" (" -> " "(" sepBy(term, ",") ")")? : verityExternal
@@ -82,6 +87,7 @@ syntax (name := verityContractCmd)
   "storage " verityStorageField*
   (verityStructDecl)*
   ("errors " verityError+)?
+  ("event_defs " verityEvent+)?
   ("constants " verityConstant+)?
   ("immutables " verityImmutable+)?
   ("linked_externals " verityExternal+)?
diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index f157050bf..7dcb17f55 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -75,6 +75,17 @@ structure ErrorDecl where
   name : String
   params : Array ValueType
 
+structure EventParamDecl where
+  ident : Ident
+  name : String
+  ty : ValueType
+  isIndexed : Bool
+
+structure EventDecl where
+  ident : Ident
+  name : String
+  params : Array EventParamDecl
+
 structure ConstantDecl where
   ident : Ident
   name : String
@@ -788,6 +799,42 @@ private def parseError (newtypes : Array NewtypeDecl) (structDecls : Array Struc
       }
   | _ => throwErrorAt stx "invalid custom error declaration"
 
+private def parseEventParam
+    (newtypes : Array NewtypeDecl)
+    (structDecls : Array StructDecl)
+    (adtDecls : Array AdtDecl)
+    (stx : Syntax) : CommandElabM EventParamDecl := do
+  match stx with
+  | `(verityEventParam| $name:ident : $ty:term) =>
+      pure {
+        ident := name
+        name := toString name.getId
+        ty := ← valueTypeFromSyntax newtypes structDecls adtDecls ty
+        isIndexed := false
+      }
+  | `(verityEventParam| @indexed $name:ident : $ty:term) =>
+      pure {
+        ident := name
+        name := toString name.getId
+        ty := ← valueTypeFromSyntax newtypes structDecls adtDecls ty
+        isIndexed := true
+      }
+  | _ => throwErrorAt stx "invalid event parameter declaration"
+
+private def parseEvent
+    (newtypes : Array NewtypeDecl)
+    (structDecls : Array StructDecl)
+    (adtDecls : Array AdtDecl)
+    (stx : Syntax) : CommandElabM EventDecl := do
+  match stx with
+  | `(verityEvent| event $name:ident ($[$params:verityEventParam],*)) =>
+      pure {
+        ident := name
+        name := toString name.getId
+        params := ← params.mapM (parseEventParam newtypes structDecls adtDecls)
+      }
+  | _ => throwErrorAt stx "invalid event declaration"
+
 private def parseConstant (newtypes : Array NewtypeDecl) (stx : Syntax) : CommandElabM ConstantDecl := do
   match stx with
   | `(verityConstant| $name:ident : $ty:term := $body:term) =>
@@ -6321,6 +6368,24 @@ private def mkModelErrorTerm (err : ErrorDecl) : CommandElabM Term := do
       $(strTerm err.name)
       [ $[$paramTerms],* ])
 
+private def mkModelEventParamTerm (param : EventParamDecl) : CommandElabM Term := do
+  let tyTerm ← modelParamTypeTerm param.ty
+  let kindTerm ←
+    if param.isIndexed then
+      `(Compiler.CompilationModel.EventParamKind.indexed)
+    else
+      `(Compiler.CompilationModel.EventParamKind.unindexed)
+  `(Compiler.CompilationModel.EventParam.mk
+      $(strTerm param.name)
+      $tyTerm
+      $kindTerm)
+
+private def mkModelEventTerm (ev : EventDecl) : CommandElabM Term := do
+  let paramTerms ← ev.params.mapM mkModelEventParamTerm
+  `(Compiler.CompilationModel.EventDef.mk
+      $(strTerm ev.name)
+      [ $[$paramTerms],* ])
+
 private def mkModelExternalTerm (ext : ExternalDecl) : CommandElabM Term := do
   let paramTerms ← ext.params.mapM modelParamTypeTerm
   let returnTerms ← ext.returnTys.mapM modelParamTypeTerm
@@ -6405,6 +6470,7 @@ private def mkSpecCommand
     (contractName : String)
     (fields : Array StorageFieldDecl)
     (errorDecls : Array ErrorDecl)
+    (eventDecls : Array EventDecl)
     (constDecls : Array ConstantDecl)
     (immutableDecls : Array ImmutableDecl)
     (externalDecls : Array ExternalDecl)
@@ -6416,6 +6482,7 @@ private def mkSpecCommand
   let allFields := fields ++ immutableFields
   let fieldTerms ← allFields.mapM mkModelFieldTerm
   let errorTerms ← errorDecls.mapM mkModelErrorTerm
+  let eventTerms ← eventDecls.mapM mkModelEventTerm
   let externalTerms ← externalDecls.mapM mkModelExternalTerm
   let constructorTerm ←
     match ctor, immutableDecls.isEmpty with
@@ -6499,6 +6566,7 @@ private def mkSpecCommand
     name := $(strTerm contractName)
     fields := [ $[$fieldTerms],* ]
     «errors» := [ $[$errorTerms],* ]
+    «events» := [ $[$eventTerms],* ]
     «constructor» := $constructorTerm
     functions := [ $[$allFunctionTerms],* ]
     «externals» := [ $[$externalTerms],* ]
@@ -6599,9 +6667,9 @@ def computeStorageNamespaceKey (key : String) : Nat :=
 def parseContractSyntax
     (stx : Syntax)
     : CommandElabM
-        (Ident × Array NewtypeDecl × Array StructDecl × Array AdtDecl × Array StorageFieldDecl × Array ErrorDecl × Array ConstantDecl × Array ImmutableDecl × Array ExternalDecl × Option ConstructorDecl × Array FunctionDecl × Option Nat) := do
+        (Ident × Array NewtypeDecl × Array StructDecl × Array AdtDecl × Array StorageFieldDecl × Array ErrorDecl × Array EventDecl × Array ConstantDecl × Array ImmutableDecl × Array ExternalDecl × Option ConstructorDecl × Array FunctionDecl × Option Nat) := do
   match stx with
-  | `(command| verity_contract $contractName:ident where $[types $[$newtypeDecls:verityNewtype]*]? $[inductive $[$adtDecls:verityAdtDecl]*]? $[$nsSpec:verityNamespaceSpec]? storage $[$storageFields:verityStorageField]* $[$structDecls:verityStructDecl]* $[errors $[$errorDecls:verityError]*]? $[constants $[$constantDecls:verityConstant]*]? $[immutables $[$immutableDecls:verityImmutable]*]? $[linked_externals $[$externalDecls:verityExternal]*]? $[$ctor:verityConstructor]? $[$entrypoints:veritySpecialEntrypoint]* $[$functions:verityFunction]*) =>
+  | `(command| verity_contract $contractName:ident where $[types $[$newtypeDecls:verityNewtype]*]? $[inductive $[$adtDecls:verityAdtDecl]*]? $[$nsSpec:verityNamespaceSpec]? storage $[$storageFields:verityStorageField]* $[$structDecls:verityStructDecl]* $[errors $[$errorDecls:verityError]*]? $[event_defs $[$eventDecls:verityEvent]*]? $[constants $[$constantDecls:verityConstant]*]? $[immutables $[$immutableDecls:verityImmutable]*]? $[linked_externals $[$externalDecls:verityExternal]*]? $[$ctor:verityConstructor]? $[$entrypoints:veritySpecialEntrypoint]* $[$functions:verityFunction]*) =>
       -- Parse newtypes first — they are needed by all downstream type resolution
       let parsedNewtypes ←
         match newtypeDecls with
@@ -6665,6 +6733,10 @@ def parseContractSyntax
         match errorDecls with
         | some decls => decls.mapM (parseError parsedNewtypes parsedStructs parsedAdts)
         | none => pure #[]
+      let parsedEvents ←
+        match eventDecls with
+        | some decls => decls.mapM (parseEvent parsedNewtypes parsedStructs parsedAdts)
+        | none => pure #[]
       let parsedConstants ←
         match constantDecls with
         | some decls => decls.mapM (parseConstant parsedNewtypes)
@@ -6691,6 +6763,7 @@ def parseContractSyntax
         , parsedAdts
         , parsedFields
         , parsedErrors
+        , parsedEvents
         , parsedConstants
         , parsedImmutables
         , parsedExternals
@@ -7016,6 +7089,7 @@ def mkSpecCommandPublic
     (contractName : String)
     (fields : Array StorageFieldDecl)
     (errorDecls : Array ErrorDecl)
+    (eventDecls : Array EventDecl)
     (constDecls : Array ConstantDecl)
     (immutableDecls : Array ImmutableDecl)
     (externalDecls : Array ExternalDecl)
@@ -7023,7 +7097,7 @@ def mkSpecCommandPublic
     (functions : Array FunctionDecl)
     (adtDecls : Array AdtDecl)
     (storageNamespace : Option Nat) : CommandElabM Cmd :=
-  mkSpecCommand contractName fields errorDecls constDecls immutableDecls externalDecls ctor functions adtDecls storageNamespace
+  mkSpecCommand contractName fields errorDecls eventDecls constDecls immutableDecls externalDecls ctor functions adtDecls storageNamespace
 
 def mkFindIdxFieldSimpCommandsPublic
     (contractIdent : Ident)