diff --git a/Compiler/CompilationModel/EcmAxiomCollection.lean b/Compiler/CompilationModel/EcmAxiomCollection.lean
index d9a5b62cc..d6092f193 100644
--- a/Compiler/CompilationModel/EcmAxiomCollection.lean
+++ b/Compiler/CompilationModel/EcmAxiomCollection.lean
@@ -23,6 +23,7 @@ where
     | _ => []
   collectExprEcmAxioms : Expr → List (String × String)
     | .ite cond a b => collectExprEcmAxioms cond ++ collectExprEcmAxioms a ++ collectExprEcmAxioms b
+    | .forkIfAtLeast _ thenExpr elseExpr => collectExprEcmAxioms thenExpr ++ collectExprEcmAxioms elseExpr
     | _ => []
 
 end Compiler.CompilationModel
diff --git a/Compiler/CompilationModel/ExpressionCompile.lean b/Compiler/CompilationModel/ExpressionCompile.lean
index 67a8c3f36..fa496a47f 100644
--- a/Compiler/CompilationModel/ExpressionCompile.lean
+++ b/Compiler/CompilationModel/ExpressionCompile.lean
@@ -453,6 +453,8 @@ def compileExpr (fields : List Field)
           if args.length != inArity then
             throw s!"Compilation error: intrinsic {name} builtin {builtinName} expects {inArity} arg(s), got {args.length}"
           pure (YulExpr.call builtinName argExprs)
+  | Expr.forkIfAtLeast required _thenExpr _elseExpr =>
+      throw s!"Compilation error: unresolved fork_if_at_least {required}; compile through compileSpecsWithOptions so the branch can be selected from --target-fork before Yul emission"
   | Expr.eq a b      => return yulBinOp "eq"  (← compileExpr fields dynamicSource a) (← compileExpr fields dynamicSource b)
   | Expr.gt a b      => return yulBinOp "gt"  (← compileExpr fields dynamicSource a) (← compileExpr fields dynamicSource b)
   | Expr.sgt a b     => return yulBinOp "sgt" (← compileExpr fields dynamicSource a) (← compileExpr fields dynamicSource b)
diff --git a/Compiler/CompilationModel/LogicalPurity.lean b/Compiler/CompilationModel/LogicalPurity.lean
index 9e9b5e725..428a5e2df 100644
--- a/Compiler/CompilationModel/LogicalPurity.lean
+++ b/Compiler/CompilationModel/LogicalPurity.lean
@@ -51,6 +51,8 @@ partial def exprContainsCallLike (expr : Expr) : Bool :=
       exprContainsCallLike a || exprContainsCallLike b
   | Expr.intrinsic _ _ _ args =>
       exprListContainsCallLike args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprContainsCallLike thenExpr || exprContainsCallLike elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c
   | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c =>
       exprContainsCallLike a || exprContainsCallLike b || exprContainsCallLike c
@@ -159,6 +161,8 @@ def exprContainsUnsafeLogicalCallLike (expr : Expr) : Bool :=
       exprContainsUnsafeLogicalCallLike a || exprContainsUnsafeLogicalCallLike b
   | Expr.intrinsic _ _ _ args =>
       exprListAnyUnsafeLogicalCallLike args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprContainsUnsafeLogicalCallLike thenExpr || exprContainsUnsafeLogicalCallLike elseExpr
   | Expr.mulDivDown a b c
   | Expr.mulDiv512Down a b c =>
       exprContainsUnsafeLogicalCallLike a || exprContainsUnsafeLogicalCallLike b || exprContainsUnsafeLogicalCallLike c
diff --git a/Compiler/CompilationModel/ScopeValidation.lean b/Compiler/CompilationModel/ScopeValidation.lean
index efbd3b389..aa0f11533 100644
--- a/Compiler/CompilationModel/ScopeValidation.lean
+++ b/Compiler/CompilationModel/ScopeValidation.lean
@@ -367,6 +367,9 @@ def validateScopedExprIdentifiers
       validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount b
   | Expr.intrinsic _ _ _ args =>
       validateScopedExprIdentifiersList context params paramScope dynamicParams localScope constructorArgCount args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr => do
+      validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount thenExpr
+      validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount elseExpr
   | Expr.wDivUp a b => do
       validateArithDuplicatedOperandPurity context [b]
       validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount a
diff --git a/Compiler/CompilationModel/Types.lean b/Compiler/CompilationModel/Types.lean
index bcac8a852..ae39fcab8 100644
--- a/Compiler/CompilationModel/Types.lean
+++ b/Compiler/CompilationModel/Types.lean
@@ -483,6 +483,14 @@ inductive Expr
       (lowering : Verity.Core.Intrinsics.YulLowering)
       (minFork : Verity.Core.Intrinsics.HardFork)
       (args : List Expr)
+  /-- Compile-time fork selection. `thenExpr` is selected when the compiler
+      target fork is at least `required`; otherwise `elseExpr` is selected.
+      The unselected branch is removed before intrinsic fork gates and Yul
+      lowering run, so this is suitable for explicit opcode/emulation fallback
+      pairs without silently weakening `min_fork` on the intrinsic itself. -/
+  | forkIfAtLeast
+      (required : Verity.Core.Intrinsics.HardFork)
+      (thenExpr elseExpr : Expr)
   | eq (a b : Expr)
   | ge (a b : Expr)
   | gt (a b : Expr)  -- Greater than (strict)
diff --git a/Compiler/CompilationModel/UsageAnalysis.lean b/Compiler/CompilationModel/UsageAnalysis.lean
index 1900a342c..4e68848ff 100644
--- a/Compiler/CompilationModel/UsageAnalysis.lean
+++ b/Compiler/CompilationModel/UsageAnalysis.lean
@@ -173,6 +173,9 @@ def exprUsesArrayElementKind (includePlain includeWord : Bool) : Expr → Bool
         exprUsesArrayElementKind includePlain includeWord b
   | Expr.intrinsic _ _ _ args =>
       exprListUsesArrayElementKind includePlain includeWord args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprUsesArrayElementKind includePlain includeWord thenExpr ||
+        exprUsesArrayElementKind includePlain includeWord elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c =>
       exprUsesArrayElementKind includePlain includeWord a ||
         exprUsesArrayElementKind includePlain includeWord b ||
@@ -356,6 +359,8 @@ def exprUsesArrayElement : Expr → Bool
     Expr.ceilDiv a b =>
       exprUsesArrayElement a || exprUsesArrayElement b
   | Expr.intrinsic _ _ _ args => exprListUsesArrayElement args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprUsesArrayElement thenExpr || exprUsesArrayElement elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c =>
       exprUsesArrayElement a || exprUsesArrayElement b || exprUsesArrayElement c
   | Expr.bitNot a | Expr.logicalNot a =>
@@ -559,6 +564,8 @@ def exprUsesParamDynamicHeadWord : Expr → Bool
   | Expr.wMulDown a b | Expr.wDivUp a b | Expr.min a b | Expr.max a b | Expr.ceilDiv a b =>
       exprUsesParamDynamicHeadWord a || exprUsesParamDynamicHeadWord b
   | Expr.intrinsic _ _ _ args => exprListUsesParamDynamicHeadWord args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprUsesParamDynamicHeadWord thenExpr || exprUsesParamDynamicHeadWord elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c
   | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c
   | Expr.ite a b c =>
@@ -701,6 +708,8 @@ def exprUsesMulDiv512 : Expr → Bool
   | Expr.wMulDown a b | Expr.wDivUp a b | Expr.min a b | Expr.max a b | Expr.ceilDiv a b =>
       exprUsesMulDiv512 a || exprUsesMulDiv512 b
   | Expr.intrinsic _ _ _ args => exprListUsesMulDiv512 args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprUsesMulDiv512 thenExpr || exprUsesMulDiv512 elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c | Expr.ite a b c =>
       exprUsesMulDiv512 a || exprUsesMulDiv512 b || exprUsesMulDiv512 c
   | Expr.literal _ | Expr.param _ | Expr.constructorArg _
@@ -859,6 +868,8 @@ def exprUsesStorageArrayElement : Expr → Bool
     Expr.ceilDiv a b =>
       exprUsesStorageArrayElement a || exprUsesStorageArrayElement b
   | Expr.intrinsic _ _ _ args => exprListUsesStorageArrayElement args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprUsesStorageArrayElement thenExpr || exprUsesStorageArrayElement elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c =>
       exprUsesStorageArrayElement a || exprUsesStorageArrayElement b || exprUsesStorageArrayElement c
   | Expr.bitNot a | Expr.logicalNot a =>
@@ -1021,6 +1032,8 @@ def exprUsesDynamicBytesEq : Expr → Bool
   | Expr.ceilDiv a b =>
       exprUsesDynamicBytesEq a || exprUsesDynamicBytesEq b
   | Expr.intrinsic _ _ _ args => exprListUsesDynamicBytesEq args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprUsesDynamicBytesEq thenExpr || exprUsesDynamicBytesEq elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c =>
       exprUsesDynamicBytesEq a || exprUsesDynamicBytesEq b || exprUsesDynamicBytesEq c
   | Expr.bitNot a | Expr.logicalNot a =>
diff --git a/Compiler/CompilationModel/Validation.lean b/Compiler/CompilationModel/Validation.lean
index 16f14a6f9..3df3a4928 100644
--- a/Compiler/CompilationModel/Validation.lean
+++ b/Compiler/CompilationModel/Validation.lean
@@ -302,6 +302,8 @@ def exprReadsStateOrEnv : Expr → Bool
     Expr.ceilDiv a b =>
       exprReadsStateOrEnv a || exprReadsStateOrEnv b
   | Expr.intrinsic _ _ _ args => exprListReadsStateOrEnv args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprReadsStateOrEnv thenExpr || exprReadsStateOrEnv elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c
   | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c =>
       exprReadsStateOrEnv a || exprReadsStateOrEnv b || exprReadsStateOrEnv c
@@ -361,6 +363,8 @@ def exprWritesState : Expr → Bool
   | Expr.externalCall name args =>
       if name == builtinExpName then exprListWritesState args else true
   | Expr.intrinsic _ _ _ args => exprListWritesState args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprWritesState thenExpr || exprWritesState elseExpr
   | Expr.internalCall _ _ => true
   | Expr.adtConstruct _ _ args => exprListWritesState args
   | Expr.extcodesize addr =>
@@ -519,6 +523,8 @@ def exprHasUntrackableWrites : Expr → Bool
   | Expr.byte a b =>
       exprHasUntrackableWrites a || exprHasUntrackableWrites b
   | Expr.intrinsic _ _ _ args => exprListHasUntrackableWrites args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprHasUntrackableWrites thenExpr || exprHasUntrackableWrites elseExpr
   | Expr.lt a b | Expr.gt a b | Expr.slt a b | Expr.sgt a b | Expr.eq a b
   | Expr.ge a b | Expr.le a b | Expr.signextend a b
   | Expr.logicalAnd a b | Expr.logicalOr a b
@@ -671,6 +677,8 @@ def exprContainsExternalCall : Expr → Bool
   | Expr.byte a b =>
       exprContainsExternalCall a || exprContainsExternalCall b
   | Expr.intrinsic _ _ _ args => exprListContainsExternalCall args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprContainsExternalCall thenExpr || exprContainsExternalCall elseExpr
   | Expr.lt a b | Expr.gt a b | Expr.slt a b | Expr.sgt a b | Expr.eq a b
   | Expr.ge a b | Expr.le a b | Expr.signextend a b
   | Expr.logicalAnd a b | Expr.logicalOr a b
@@ -753,6 +761,8 @@ def exprMayContainExternalCall : Expr → Bool
   | Expr.byte a b =>
       exprMayContainExternalCall a || exprMayContainExternalCall b
   | Expr.intrinsic _ _ _ args => exprListMayContainExternalCall args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprMayContainExternalCall thenExpr || exprMayContainExternalCall elseExpr
   | Expr.lt a b | Expr.gt a b | Expr.slt a b | Expr.sgt a b | Expr.eq a b
   | Expr.ge a b | Expr.le a b | Expr.signextend a b
   | Expr.logicalAnd a b | Expr.logicalOr a b
@@ -1065,6 +1075,9 @@ def exprWritesStateWithFunctionEffects
       exprWritesStateWithFunctionEffects effects a ||
         exprWritesStateWithFunctionEffects effects b
   | Expr.intrinsic _ _ _ args => exprListWritesStateWithFunctionEffects effects args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprWritesStateWithFunctionEffects effects thenExpr ||
+        exprWritesStateWithFunctionEffects effects elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c
   | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c =>
       exprWritesStateWithFunctionEffects effects a ||
@@ -1312,6 +1325,9 @@ def exprReadsStateOrEnvWithFunctionEffects
       exprReadsStateOrEnvWithFunctionEffects effects a ||
         exprReadsStateOrEnvWithFunctionEffects effects b
   | Expr.intrinsic _ _ _ args => exprListReadsStateOrEnvWithFunctionEffects effects args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprReadsStateOrEnvWithFunctionEffects effects thenExpr ||
+        exprReadsStateOrEnvWithFunctionEffects effects elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c
   | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c =>
       exprReadsStateOrEnvWithFunctionEffects effects a ||
@@ -1633,6 +1649,8 @@ def exprContainsAdtConstruct : Expr → Bool
   | Expr.byte a b =>
       exprContainsAdtConstruct a || exprContainsAdtConstruct b
   | Expr.intrinsic _ _ _ args => exprListContainsAdtConstruct args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprContainsAdtConstruct thenExpr || exprContainsAdtConstruct elseExpr
   | Expr.lt a b | Expr.gt a b | Expr.slt a b | Expr.sgt a b | Expr.eq a b
   | Expr.ge a b | Expr.le a b | Expr.signextend a b
   | Expr.logicalAnd a b | Expr.logicalOr a b
diff --git a/Compiler/CompilationModel/ValidationCalls.lean b/Compiler/CompilationModel/ValidationCalls.lean
index 0b5e72b34..48e1f839f 100644
--- a/Compiler/CompilationModel/ValidationCalls.lean
+++ b/Compiler/CompilationModel/ValidationCalls.lean
@@ -242,6 +242,9 @@ def validateInternalCallShapesInExpr
       validateInternalCallShapesInExpr functions callerName b
   | Expr.intrinsic _ _ _ args =>
       validateInternalCallShapesInExprList functions callerName args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr => do
+      validateInternalCallShapesInExpr functions callerName thenExpr
+      validateInternalCallShapesInExpr functions callerName elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c
   | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c => do
       validateInternalCallShapesInExpr functions callerName a
@@ -517,6 +520,9 @@ def validateExternalCallTargetsInExpr
       validateExternalCallTargetsInExpr externals context b
   | Expr.intrinsic _ _ _ args =>
       validateExternalCallTargetsInExprList externals context args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr => do
+      validateExternalCallTargetsInExpr externals context thenExpr
+      validateExternalCallTargetsInExpr externals context elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c
   | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c => do
       validateExternalCallTargetsInExpr externals context a
diff --git a/Compiler/CompilationModel/ValidationHelpers.lean b/Compiler/CompilationModel/ValidationHelpers.lean
index d43a15fdb..ee80dcc02 100644
--- a/Compiler/CompilationModel/ValidationHelpers.lean
+++ b/Compiler/CompilationModel/ValidationHelpers.lean
@@ -112,6 +112,7 @@ def collectExprNames : Expr → List String
   | Expr.byte index value => collectExprNames index ++ collectExprNames value
   | Expr.signextend byteIndex value => collectExprNames byteIndex ++ collectExprNames value
   | Expr.intrinsic _name _ _ args => collectExprListNames args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr => collectExprNames thenExpr ++ collectExprNames elseExpr
   | Expr.eq a b => collectExprNames a ++ collectExprNames b
   | Expr.ge a b => collectExprNames a ++ collectExprNames b
   | Expr.gt a b => collectExprNames a ++ collectExprNames b
diff --git a/Compiler/CompilationModel/ValidationInterop.lean b/Compiler/CompilationModel/ValidationInterop.lean
index 03112831a..de65ec953 100644
--- a/Compiler/CompilationModel/ValidationInterop.lean
+++ b/Compiler/CompilationModel/ValidationInterop.lean
@@ -105,6 +105,9 @@ def validateInteropExpr (context : String) : Expr → Except String Unit
       validateInteropExpr context b
   | Expr.intrinsic _ _ _ args =>
       validateInteropExprList context args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr => do
+      validateInteropExpr context thenExpr
+      validateInteropExpr context elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c
   | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c => do
       validateInteropExpr context a
diff --git a/Compiler/CompileDriverCommon.lean b/Compiler/CompileDriverCommon.lean
index ed7d06b1e..97b992bf2 100644
--- a/Compiler/CompileDriverCommon.lean
+++ b/Compiler/CompileDriverCommon.lean
@@ -166,10 +166,158 @@ private partial def collectIntrinsicUsesExpr : Expr → List IntrinsicUse
       keys.flatMap collectIntrinsicUsesExpr
   | .intrinsic name _ minFork args =>
       { name := name, minFork := minFork } :: args.flatMap collectIntrinsicUsesExpr
+  | .forkIfAtLeast _ thenExpr elseExpr =>
+      collectIntrinsicUsesExpr thenExpr ++ collectIntrinsicUsesExpr elseExpr
   | .dynamicBytesEq _ _ =>
       []
   | _ => []
 
+private partial def specializeForkExpr
+    (targetFork : Verity.Core.Intrinsics.HardFork) : Expr → Expr
+  | .mapping field key => .mapping field (specializeForkExpr targetFork key)
+  | .mappingWord field key wordOffset => .mappingWord field (specializeForkExpr targetFork key) wordOffset
+  | .mappingPackedWord field key wordOffset packed => .mappingPackedWord field (specializeForkExpr targetFork key) wordOffset packed
+  | .mapping2 field key1 key2 => .mapping2 field (specializeForkExpr targetFork key1) (specializeForkExpr targetFork key2)
+  | .mapping2Word field key1 key2 wordOffset => .mapping2Word field (specializeForkExpr targetFork key1) (specializeForkExpr targetFork key2) wordOffset
+  | .mappingUint field key => .mappingUint field (specializeForkExpr targetFork key)
+  | .mappingChain field keys => .mappingChain field (keys.map (specializeForkExpr targetFork))
+  | .structMember field key memberName => .structMember field (specializeForkExpr targetFork key) memberName
+  | .structMember2 field key1 key2 memberName => .structMember2 field (specializeForkExpr targetFork key1) (specializeForkExpr targetFork key2) memberName
+  | .extcodesize addr => .extcodesize (specializeForkExpr targetFork addr)
+  | .mload offset => .mload (specializeForkExpr targetFork offset)
+  | .tload offset => .tload (specializeForkExpr targetFork offset)
+  | .keccak256 offset size => .keccak256 (specializeForkExpr targetFork offset) (specializeForkExpr targetFork size)
+  | .call gas target value inOffset inSize outOffset outSize =>
+      .call (specializeForkExpr targetFork gas) (specializeForkExpr targetFork target)
+        (specializeForkExpr targetFork value) (specializeForkExpr targetFork inOffset)
+        (specializeForkExpr targetFork inSize) (specializeForkExpr targetFork outOffset)
+        (specializeForkExpr targetFork outSize)
+  | .staticcall gas target inOffset inSize outOffset outSize =>
+      .staticcall (specializeForkExpr targetFork gas) (specializeForkExpr targetFork target)
+        (specializeForkExpr targetFork inOffset) (specializeForkExpr targetFork inSize)
+        (specializeForkExpr targetFork outOffset) (specializeForkExpr targetFork outSize)
+  | .delegatecall gas target inOffset inSize outOffset outSize =>
+      .delegatecall (specializeForkExpr targetFork gas) (specializeForkExpr targetFork target)
+        (specializeForkExpr targetFork inOffset) (specializeForkExpr targetFork inSize)
+        (specializeForkExpr targetFork outOffset) (specializeForkExpr targetFork outSize)
+  | .calldataload offset => .calldataload (specializeForkExpr targetFork offset)
+  | .returndataOptionalBoolAt outOffset => .returndataOptionalBoolAt (specializeForkExpr targetFork outOffset)
+  | .externalCall name args => .externalCall name (args.map (specializeForkExpr targetFork))
+  | .internalCall name args => .internalCall name (args.map (specializeForkExpr targetFork))
+  | .arrayElement name index => .arrayElement name (specializeForkExpr targetFork index)
+  | .memoryArrayElement name index => .memoryArrayElement name (specializeForkExpr targetFork index)
+  | .arrayElementWord name index elementWords wordOffset => .arrayElementWord name (specializeForkExpr targetFork index) elementWords wordOffset
+  | .arrayElementDynamicWord name index wordOffset => .arrayElementDynamicWord name (specializeForkExpr targetFork index) wordOffset
+  | .arrayElementDynamicDataOffset name index => .arrayElementDynamicDataOffset name (specializeForkExpr targetFork index)
+  | .paramDynamicMemberElement name wordOffset innerIndex => .paramDynamicMemberElement name wordOffset (specializeForkExpr targetFork innerIndex)
+  | .arrayElementDynamicMemberLength name index wordOffset => .arrayElementDynamicMemberLength name (specializeForkExpr targetFork index) wordOffset
+  | .arrayElementDynamicMemberDataOffset name index wordOffset => .arrayElementDynamicMemberDataOffset name (specializeForkExpr targetFork index) wordOffset
+  | .arrayElementDynamicMemberElement name index wordOffset innerIndex =>
+      .arrayElementDynamicMemberElement name (specializeForkExpr targetFork index) wordOffset (specializeForkExpr targetFork innerIndex)
+  | .storageArrayElement field index => .storageArrayElement field (specializeForkExpr targetFork index)
+  | .add a b => .add (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .sub a b => .sub (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .mul a b => .mul (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .div a b => .div (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .sdiv a b => .sdiv (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .mod a b => .mod (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .smod a b => .smod (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .bitAnd a b => .bitAnd (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .bitOr a b => .bitOr (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .bitXor a b => .bitXor (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .bitNot a => .bitNot (specializeForkExpr targetFork a)
+  | .shl a b => .shl (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .shr a b => .shr (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .sar a b => .sar (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .byte a b => .byte (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .signextend a b => .signextend (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .intrinsic name lowering minFork args => .intrinsic name lowering minFork (args.map (specializeForkExpr targetFork))
+  | .forkIfAtLeast required thenExpr elseExpr =>
+      specializeForkExpr targetFork
+        (if Verity.Core.Intrinsics.HardFork.allows targetFork required then thenExpr else elseExpr)
+  | .eq a b => .eq (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .ge a b => .ge (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .gt a b => .gt (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .sgt a b => .sgt (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .lt a b => .lt (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .slt a b => .slt (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .le a b => .le (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .logicalAnd a b => .logicalAnd (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .logicalOr a b => .logicalOr (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .logicalNot a => .logicalNot (specializeForkExpr targetFork a)
+  | .ceilDiv a b => .ceilDiv (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .mulDivDown a b c => .mulDivDown (specializeForkExpr targetFork a) (specializeForkExpr targetFork b) (specializeForkExpr targetFork c)
+  | .mulDivUp a b c => .mulDivUp (specializeForkExpr targetFork a) (specializeForkExpr targetFork b) (specializeForkExpr targetFork c)
+  | .mulDiv512Down a b c => .mulDiv512Down (specializeForkExpr targetFork a) (specializeForkExpr targetFork b) (specializeForkExpr targetFork c)
+  | .mulDiv512Up a b c => .mulDiv512Up (specializeForkExpr targetFork a) (specializeForkExpr targetFork b) (specializeForkExpr targetFork c)
+  | .wMulDown a b => .wMulDown (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .wDivUp a b => .wDivUp (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .min a b => .min (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .max a b => .max (specializeForkExpr targetFork a) (specializeForkExpr targetFork b)
+  | .ite a b c => .ite (specializeForkExpr targetFork a) (specializeForkExpr targetFork b) (specializeForkExpr targetFork c)
+  | .adtConstruct adt variant args => .adtConstruct adt variant (args.map (specializeForkExpr targetFork))
+  | other => other
+
+private partial def specializeForkStmt
+    (targetFork : Verity.Core.Intrinsics.HardFork) : Stmt → Stmt
+  | .letVar name value => .letVar name (specializeForkExpr targetFork value)
+  | .assignVar name value => .assignVar name (specializeForkExpr targetFork value)
+  | .setStorage field value => .setStorage field (specializeForkExpr targetFork value)
+  | .setStorageAddr field value => .setStorageAddr field (specializeForkExpr targetFork value)
+  | .setStorageWord field wordOffset value => .setStorageWord field wordOffset (specializeForkExpr targetFork value)
+  | .storageArrayPush field value => .storageArrayPush field (specializeForkExpr targetFork value)
+  | .setStorageArrayElement field index value => .setStorageArrayElement field (specializeForkExpr targetFork index) (specializeForkExpr targetFork value)
+  | .setMapping field key value => .setMapping field (specializeForkExpr targetFork key) (specializeForkExpr targetFork value)
+  | .setMappingWord field key wordOffset value => .setMappingWord field (specializeForkExpr targetFork key) wordOffset (specializeForkExpr targetFork value)
+  | .setMappingPackedWord field key wordOffset packed value => .setMappingPackedWord field (specializeForkExpr targetFork key) wordOffset packed (specializeForkExpr targetFork value)
+  | .setMapping2 field key1 key2 value => .setMapping2 field (specializeForkExpr targetFork key1) (specializeForkExpr targetFork key2) (specializeForkExpr targetFork value)
+  | .setMapping2Word field key1 key2 wordOffset value => .setMapping2Word field (specializeForkExpr targetFork key1) (specializeForkExpr targetFork key2) wordOffset (specializeForkExpr targetFork value)
+  | .setMappingUint field key value => .setMappingUint field (specializeForkExpr targetFork key) (specializeForkExpr targetFork value)
+  | .setMappingChain field keys value => .setMappingChain field (keys.map (specializeForkExpr targetFork)) (specializeForkExpr targetFork value)
+  | .setStructMember field key memberName value => .setStructMember field (specializeForkExpr targetFork key) memberName (specializeForkExpr targetFork value)
+  | .setStructMember2 field key1 key2 memberName value => .setStructMember2 field (specializeForkExpr targetFork key1) (specializeForkExpr targetFork key2) memberName (specializeForkExpr targetFork value)
+  | .require cond message => .require (specializeForkExpr targetFork cond) message
+  | .requireError cond errorName args => .requireError (specializeForkExpr targetFork cond) errorName (args.map (specializeForkExpr targetFork))
+  | .revertError errorName args => .revertError errorName (args.map (specializeForkExpr targetFork))
+  | .return value => .return (specializeForkExpr targetFork value)
+  | .returnValues values => .returnValues (values.map (specializeForkExpr targetFork))
+  | .mstore offset value => .mstore (specializeForkExpr targetFork offset) (specializeForkExpr targetFork value)
+  | .tstore offset value => .tstore (specializeForkExpr targetFork offset) (specializeForkExpr targetFork value)
+  | .calldatacopy dest source size => .calldatacopy (specializeForkExpr targetFork dest) (specializeForkExpr targetFork source) (specializeForkExpr targetFork size)
+  | .returndataCopy dest source size => .returndataCopy (specializeForkExpr targetFork dest) (specializeForkExpr targetFork source) (specializeForkExpr targetFork size)
+  | .ite cond thenBranch elseBranch => .ite (specializeForkExpr targetFork cond) (thenBranch.map (specializeForkStmt targetFork)) (elseBranch.map (specializeForkStmt targetFork))
+  | .forEach varName count body => .forEach varName (specializeForkExpr targetFork count) (body.map (specializeForkStmt targetFork))
+  | .emit eventName args => .emit eventName (args.map (specializeForkExpr targetFork))
+  | .internalCall functionName args => .internalCall functionName (args.map (specializeForkExpr targetFork))
+  | .internalCallAssign names functionName args => .internalCallAssign names functionName (args.map (specializeForkExpr targetFork))
+  | .rawLog topics dataOffset dataSize => .rawLog (topics.map (specializeForkExpr targetFork)) (specializeForkExpr targetFork dataOffset) (specializeForkExpr targetFork dataSize)
+  | .externalCallBind resultVars externalName args => .externalCallBind resultVars externalName (args.map (specializeForkExpr targetFork))
+  | .tryExternalCallBind successVar resultVars externalName args => .tryExternalCallBind successVar resultVars externalName (args.map (specializeForkExpr targetFork))
+  | .ecm mod args => .ecm mod (args.map (specializeForkExpr targetFork))
+  | .unsafeBlock reason body => .unsafeBlock reason (body.map (specializeForkStmt targetFork))
+  | .matchAdt adtName scrutinee branches =>
+      .matchAdt adtName (specializeForkExpr targetFork scrutinee)
+        (branches.map fun (variantName, boundVarNames, body) =>
+          (variantName, boundVarNames, body.map (specializeForkStmt targetFork)))
+  | other => other
+
+private def specializeForkConstructor
+    (targetFork : Verity.Core.Intrinsics.HardFork)
+    (ctor : ConstructorSpec) : ConstructorSpec :=
+  { ctor with body := ctor.body.map (specializeForkStmt targetFork) }
+
+private def specializeForkFunction
+    (targetFork : Verity.Core.Intrinsics.HardFork)
+    (fn : FunctionSpec) : FunctionSpec :=
+  { fn with body := fn.body.map (specializeForkStmt targetFork) }
+
+private def specializeForkSpec
+    (targetFork : Verity.Core.Intrinsics.HardFork)
+    (spec : CompilationModel) : CompilationModel :=
+  { spec with
+    «constructor» := spec.constructor.map (specializeForkConstructor targetFork)
+    functions := spec.functions.map (specializeForkFunction targetFork) }
+
 private partial def collectIntrinsicUsesStmt : Stmt → List IntrinsicUse
   | .letVar _ value | .assignVar _ value | .setStorage _ value
   | .setStorageAddr _ value | .setStorageWord _ _ value
@@ -366,6 +514,8 @@ def compileSpecsWithOptions
   | some dir => IO.FS.createDirAll dir
   | none => pure ()
 
+  let specs := specs.map (specializeForkSpec options.targetFork)
+
   unless options.allowFutureForkIntrinsics do
     ensureIntrinsicForksAllowed options.targetFork specs
 
diff --git a/Compiler/CompileDriverTest.lean b/Compiler/CompileDriverTest.lean
index 40adae031..5a849116c 100644
--- a/Compiler/CompileDriverTest.lean
+++ b/Compiler/CompileDriverTest.lean
@@ -87,6 +87,27 @@ private def futureForkIntrinsicSpec : CompilationModel := {
   ]
 }
 
+private def forkConditionalIntrinsicSpec : CompilationModel := {
+  name := "ForkConditionalIntrinsicSmoke"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "useSelectedIntrinsic"
+      params := [{ name := "x", ty := ParamType.uint256 }]
+      returnType := some FieldType.uint256
+      body := [
+        Stmt.return
+          (Expr.forkIfAtLeast Verity.Core.Intrinsics.HardFork.osaka
+            (Expr.intrinsic "futureIntrinsic"
+              (Verity.Core.Intrinsics.YulLowering.verbatim 1 1 "1e")
+              Verity.Core.Intrinsics.HardFork.osaka
+              [Expr.param "x"])
+            (Expr.add (Expr.param "x") (Expr.literal 7)))
+      ]
+    }
+  ]
+}
+
 private def layoutReportSpec : CompilationModel := {
   name := "LayoutReportSmoke"
   fields := [
@@ -1124,6 +1145,8 @@ unsafe def runTests : IO Unit := do
   let missingLib := "/tmp/definitely-missing-library.yul"
   let linkedLib := s!"/tmp/verity-compile-driver-test-{nonce}-poseidon.yul"
   let earlySuccessfulAbi := s!"{abiDir}/AbiSmoke.abi.json"
+  let forkCondCancunOut := s!"/tmp/verity-compile-driver-test-{nonce}-fork-cond-cancun"
+  let forkCondOsakaOut := s!"/tmp/verity-compile-driver-test-{nonce}-fork-cond-osaka"
 
   IO.FS.createDirAll outDir
   IO.FS.createDirAll abiDir
@@ -1165,6 +1188,21 @@ unsafe def runTests : IO Unit := do
     false [] { allowFutureForkIntrinsics := true } none none none none
   IO.println "✓ compileSpecsWithOptions accepts future-fork intrinsic with explicit override"
 
+  compileSpecsWithOptions [forkConditionalIntrinsicSpec]
+    forkCondCancunOut
+    false [] { targetFork := Verity.Core.Intrinsics.HardFork.cancun } none none none none
+  expectFileContains
+    "fork_if_at_least selects fallback below required fork"
+    s!"{forkCondCancunOut}/ForkConditionalIntrinsicSmoke.yul"
+    [ "add(x, 7)" ]
+  compileSpecsWithOptions [forkConditionalIntrinsicSpec]
+    forkCondOsakaOut
+    false [] { targetFork := Verity.Core.Intrinsics.HardFork.osaka } none none none none
+  expectFileContains
+    "fork_if_at_least selects intrinsic at matching fork"
+    s!"{forkCondOsakaOut}/ForkConditionalIntrinsicSmoke.yul"
+    [ "verbatim_1i_1o(hex\"1e\", x)" ]
+
   IO.FS.writeFile linkedLib
     "function PoseidonT3_hash(a, b) -> out {\n    out := add(a, b)\n}\n"
   compileSpecsWithOptions [linkedLibrarySpec] outDir false [linkedLib] {} none none none none
diff --git a/Compiler/Proofs/IRGeneration/ExprCore.lean b/Compiler/Proofs/IRGeneration/ExprCore.lean
index 44202e3f8..840a34f59 100644
--- a/Compiler/Proofs/IRGeneration/ExprCore.lean
+++ b/Compiler/Proofs/IRGeneration/ExprCore.lean
@@ -68,6 +68,8 @@ def exprBoundNames : Expr → List String
   | .bitNot a | .logicalNot a => exprBoundNames a
   | .ite cond thenVal elseVal =>
       exprBoundNames cond ++ exprBoundNames thenVal ++ exprBoundNames elseVal
+  | .forkIfAtLeast _ thenExpr elseExpr =>
+      exprBoundNames thenExpr ++ exprBoundNames elseExpr
   | .mappingChain _ keys => exprListBoundNames keys
   | .dynamicBytesEq lhsName rhsName => [lhsName, rhsName]
   | .literal _ | .constructorArg _ | .storage _ | .storageAddr _ | .caller
diff --git a/Compiler/Proofs/IRGeneration/GenericInduction.lean b/Compiler/Proofs/IRGeneration/GenericInduction.lean
index c9288b3ec..2712beee4 100644
--- a/Compiler/Proofs/IRGeneration/GenericInduction.lean
+++ b/Compiler/Proofs/IRGeneration/GenericInduction.lean
@@ -3381,6 +3381,11 @@ private theorem exprCompileCore_of_exprTouchesUnsupportedContractSurface_eq_fals
         (exprCompileCore_of_exprTouchesUnsupportedContractSurface_eq_false hsurface.1.1)
         (exprCompileCore_of_exprTouchesUnsupportedContractSurface_eq_false hsurface.1.2)
         (exprCompileCore_of_exprTouchesUnsupportedContractSurface_eq_false hsurface.2)
+  | .forkIfAtLeast _ _ _, hsurface =>
+      -- Unspecialized fork conditionals are rejected by source semantics and
+      -- expression compilation. They must be specialized by the compile driver
+      -- before reaching the generic proof surface.
+      simp [exprTouchesUnsupportedContractSurface] at hsurface
   | .mulDiv512Down _ _ _, hsurface | .mulDiv512Up _ _ _, hsurface =>
       -- `mulDiv512Down/Up` is unsupported by the contract surface (verity#1761
       -- codegen-only; no `ExprCompileCore` constructor), so this branch is
diff --git a/Compiler/Proofs/IRGeneration/SourceSemantics.lean b/Compiler/Proofs/IRGeneration/SourceSemantics.lean
index 3504f5f98..8b50cf938 100644
--- a/Compiler/Proofs/IRGeneration/SourceSemantics.lean
+++ b/Compiler/Proofs/IRGeneration/SourceSemantics.lean
@@ -895,6 +895,7 @@ def evalExpr (fields : List Field) (state : RuntimeState) : Expr → Option Nat
         evalExpr fields state thenVal
       else
         evalExpr fields state elseVal
+  | .forkIfAtLeast _ _ _ => none
   | .shl shift value => do
       let shiftVal ← evalExpr fields state shift
       let wordVal ← evalExpr fields state value
@@ -1823,6 +1824,13 @@ private theorem evalExpr_ite
       else
         evalExpr fields state elseVal) := rfl
 
+private theorem evalExpr_forkIfAtLeast
+    (fields : List Field)
+    (state : RuntimeState)
+    (required : Verity.Core.Intrinsics.HardFork)
+    (thenExpr elseExpr : Expr) :
+    evalExpr fields state (.forkIfAtLeast required thenExpr elseExpr) = none := rfl
+
 mutual
   def execStmtWithEvents (fields : List Field) (events : List EventDef) :
       RuntimeState → Stmt → StmtResult
@@ -3028,6 +3036,7 @@ mutual
     | .keccak256 _ _
     | .call _ _ _ _ _ _ _ | .staticcall _ _ _ _ _ _ | .delegatecall _ _ _ _ _ _
     | .externalCall _ _ | .mappingChain _ _ | .intrinsic _ _ _ _
+    | .forkIfAtLeast _ _ _
     | .dynamicBytesEq _ _
     | .adtConstruct _ _ _ | .adtTag _ _ | .adtField _ _ _ _ _ => none
   termination_by expr => (fuel, sizeOf expr)
@@ -4127,6 +4136,8 @@ mutual
         have helse :=
           evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed spec fields fuel state elseVal hsurface.2
         simpa [evalExprWithHelpers, evalExpr_ite, hcond, hthen, helse]
+    | forkIfAtLeast required thenExpr elseExpr =>
+        simpa [evalExprWithHelpers, evalExpr_forkIfAtLeast]
 
   theorem evalExprListWithHelpers_eq_evalExprList_of_helperSurfaceClosed
       (spec : CompilationModel)
diff --git a/Compiler/Proofs/IRGeneration/SupportedSpec.lean b/Compiler/Proofs/IRGeneration/SupportedSpec.lean
index a22db0d5d..8c88c6bd9 100644
--- a/Compiler/Proofs/IRGeneration/SupportedSpec.lean
+++ b/Compiler/Proofs/IRGeneration/SupportedSpec.lean
@@ -604,6 +604,9 @@ def exprTouchesUnsupportedConstructorRawCalldataSurface : Expr → Bool
   | .mappingChain _ keys | .internalCall _ keys | .externalCall _ keys =>
       exprListTouchesUnsupportedConstructorRawCalldataSurface keys
   | .intrinsic _ _ _ _ => true
+  | .forkIfAtLeast _ thenExpr elseExpr =>
+      exprTouchesUnsupportedConstructorRawCalldataSurface thenExpr ||
+        exprTouchesUnsupportedConstructorRawCalldataSurface elseExpr
   | .keccak256 a b =>
       exprTouchesUnsupportedConstructorRawCalldataSurface a ||
         exprTouchesUnsupportedConstructorRawCalldataSurface b
@@ -715,6 +718,7 @@ def exprTouchesUnsupportedCoreSurface : Expr → Bool
   | .ite a b c =>
       exprTouchesUnsupportedCoreSurface a || exprTouchesUnsupportedCoreSurface b ||
         exprTouchesUnsupportedCoreSurface c
+  | .forkIfAtLeast _ _ _ => true
   | .wMulDown a b | .wDivUp a b =>
       exprTouchesUnsupportedCoreSurface a || exprTouchesUnsupportedCoreSurface b
   | .mulDivDown a b c | .mulDivUp a b c =>
@@ -773,6 +777,9 @@ def exprTouchesUnsupportedStateSurface : Expr → Bool
       exprTouchesUnsupportedStateSurface cond ||
         exprTouchesUnsupportedStateSurface thenVal ||
         exprTouchesUnsupportedStateSurface elseVal
+  | .forkIfAtLeast _ thenExpr elseExpr =>
+      exprTouchesUnsupportedStateSurface thenExpr ||
+        exprTouchesUnsupportedStateSurface elseExpr
   | .shl a b | .shr a b | .sar a b | .byte a b | .signextend a b =>
       exprTouchesUnsupportedStateSurface a || exprTouchesUnsupportedStateSurface b
   | .mulDivDown a b c | .mulDivUp a b c
@@ -840,6 +847,9 @@ def exprTouchesUnsupportedCallSurface : Expr → Bool
       exprTouchesUnsupportedCallSurface cond ||
         exprTouchesUnsupportedCallSurface thenVal ||
         exprTouchesUnsupportedCallSurface elseVal
+  | .forkIfAtLeast _ thenExpr elseExpr =>
+      exprTouchesUnsupportedCallSurface thenExpr ||
+        exprTouchesUnsupportedCallSurface elseExpr
   | .mapping2 _ a b | .mapping2Word _ a b _ | .structMember2 _ a b _ =>
       exprTouchesUnsupportedCallSurface a || exprTouchesUnsupportedCallSurface b
   | .mulDivDown a b c | .mulDivUp a b c
@@ -895,6 +905,9 @@ def exprTouchesUnsupportedHelperSurface : Expr → Bool
       exprTouchesUnsupportedHelperSurface cond ||
         exprTouchesUnsupportedHelperSurface thenVal ||
         exprTouchesUnsupportedHelperSurface elseVal
+  | .forkIfAtLeast _ thenExpr elseExpr =>
+      exprTouchesUnsupportedHelperSurface thenExpr ||
+        exprTouchesUnsupportedHelperSurface elseExpr
   | .mapping2 _ a b | .mapping2Word _ a b _ | .structMember2 _ a b _ =>
       exprTouchesUnsupportedHelperSurface a || exprTouchesUnsupportedHelperSurface b
   | .mulDivDown a b c | .mulDivUp a b c
@@ -961,6 +974,9 @@ def exprTouchesInternalHelperSurface : Expr → Bool
       exprTouchesInternalHelperSurface cond ||
         exprTouchesInternalHelperSurface thenVal ||
         exprTouchesInternalHelperSurface elseVal
+  | .forkIfAtLeast _ thenExpr elseExpr =>
+      exprTouchesInternalHelperSurface thenExpr ||
+        exprTouchesInternalHelperSurface elseExpr
   | .mapping2 _ a b | .mapping2Word _ a b _ | .structMember2 _ a b _ =>
       exprTouchesInternalHelperSurface a || exprTouchesInternalHelperSurface b
   | .mulDivDown a b c | .mulDivUp a b c
@@ -1017,6 +1033,9 @@ def exprTouchesUnsupportedForeignSurface : Expr → Bool
       exprTouchesUnsupportedForeignSurface cond ||
         exprTouchesUnsupportedForeignSurface thenVal ||
         exprTouchesUnsupportedForeignSurface elseVal
+  | .forkIfAtLeast _ thenExpr elseExpr =>
+      exprTouchesUnsupportedForeignSurface thenExpr ||
+        exprTouchesUnsupportedForeignSurface elseExpr
   | .mapping2 _ a b | .mapping2Word _ a b _ | .structMember2 _ a b _ =>
       exprTouchesUnsupportedForeignSurface a || exprTouchesUnsupportedForeignSurface b
   | .mulDivDown a b c | .mulDivUp a b c
@@ -1072,6 +1091,9 @@ def exprTouchesUnsupportedLowLevelSurface : Expr → Bool
       exprTouchesUnsupportedLowLevelSurface cond ||
         exprTouchesUnsupportedLowLevelSurface thenVal ||
         exprTouchesUnsupportedLowLevelSurface elseVal
+  | .forkIfAtLeast _ thenExpr elseExpr =>
+      exprTouchesUnsupportedLowLevelSurface thenExpr ||
+        exprTouchesUnsupportedLowLevelSurface elseExpr
   | .mapping2 _ a b | .mapping2Word _ a b _ | .structMember2 _ a b _ =>
       exprTouchesUnsupportedLowLevelSurface a || exprTouchesUnsupportedLowLevelSurface b
   | .mulDivDown a b c | .mulDivUp a b c
@@ -1109,6 +1131,7 @@ def exprTouchesUnsupportedContractSurface (expr : Expr) : Bool :=
   | .ite a b c =>
       exprTouchesUnsupportedContractSurface a || exprTouchesUnsupportedContractSurface b ||
         exprTouchesUnsupportedContractSurface c
+  | .forkIfAtLeast _ _ _ => true
   | .wMulDown a b | .wDivUp a b =>
       exprTouchesUnsupportedContractSurface a || exprTouchesUnsupportedContractSurface b
   | .mulDivDown a b c | .mulDivUp a b c =>
@@ -1785,6 +1808,8 @@ mutual
     | .ite cond thenVal elseVal =>
         exprInternalHelperCallNames cond ++ exprInternalHelperCallNames thenVal ++
           exprInternalHelperCallNames elseVal
+    | .forkIfAtLeast _ thenExpr elseExpr =>
+        exprInternalHelperCallNames thenExpr ++ exprInternalHelperCallNames elseExpr
     | .externalCall _ args | .intrinsic _ _ _ args =>
         exprListInternalHelperCallNames args
     -- Pure leaves: no internal helper calls. Listed explicitly (rather than
@@ -3361,6 +3386,11 @@ mutual
           exprTouchesInternalHelperSurface_eq_false_of_helperSurfaceClosed hsurface.1.1,
           exprTouchesInternalHelperSurface_eq_false_of_helperSurfaceClosed hsurface.1.2,
           exprTouchesInternalHelperSurface_eq_false_of_helperSurfaceClosed hsurface.2]
+    | forkIfAtLeast _ thenExpr elseExpr =>
+        simp only [exprTouchesUnsupportedHelperSurface, Bool.or_eq_false_iff] at hsurface
+        simp [exprTouchesInternalHelperSurface,
+          exprTouchesInternalHelperSurface_eq_false_of_helperSurfaceClosed hsurface.1,
+          exprTouchesInternalHelperSurface_eq_false_of_helperSurfaceClosed hsurface.2]
   termination_by sizeOf expr
 
   theorem exprListTouchesInternalHelperSurface_eq_false_of_helperSurfaceClosed
@@ -3758,6 +3788,12 @@ private theorem exprTouchesUnsupportedCallSurface_eq_featureOr
           exprTouchesUnsupportedCallSurface_eq_featureOr thenVal,
           exprTouchesUnsupportedCallSurface_eq_featureOr elseVal]
       simp [Bool.or_assoc, Bool.or_left_comm, Bool.or_comm]
+  | forkIfAtLeast _ thenExpr elseExpr =>
+      simp only [exprTouchesUnsupportedCallSurface, exprTouchesUnsupportedHelperSurface,
+        exprTouchesUnsupportedForeignSurface, exprTouchesUnsupportedLowLevelSurface]
+      rw [exprTouchesUnsupportedCallSurface_eq_featureOr thenExpr,
+          exprTouchesUnsupportedCallSurface_eq_featureOr elseExpr]
+      simp [Bool.or_assoc, Bool.or_left_comm, Bool.or_comm]
   | mapping2 _ a b | mapping2Word _ a b _
   | structMember2 _ a b _ =>
       simp only [exprTouchesUnsupportedCallSurface, exprTouchesUnsupportedHelperSurface,
@@ -3956,6 +3992,8 @@ private theorem exprTouchesUnsupportedContractSurface_eq_false_of_featureClosed
         exprTouchesUnsupportedContractSurface_eq_false_of_featureClosed cond hcore.1.1 hstate.1.1 hcalls.1.1,
         exprTouchesUnsupportedContractSurface_eq_false_of_featureClosed thenVal hcore.1.2 hstate.1.2 hcalls.1.2,
         exprTouchesUnsupportedContractSurface_eq_false_of_featureClosed elseVal hcore.2 hstate.2 hcalls.2]
+  | forkIfAtLeast _ thenExpr elseExpr =>
+      simp [exprTouchesUnsupportedCoreSurface] at hcore
   | wMulDown lhs rhs | wDivUp lhs rhs =>
       simp only [exprTouchesUnsupportedCoreSurface, Bool.or_eq_false_iff] at hcore
       simp only [exprTouchesUnsupportedStateSurface, Bool.or_eq_false_iff] at hstate
@@ -4051,6 +4089,8 @@ private theorem exprTouchesUnsupportedCallSurface_eq_false_of_coreClosed
         exprTouchesUnsupportedCallSurface_eq_false_of_coreClosed cond hcore.1.1,
         exprTouchesUnsupportedCallSurface_eq_false_of_coreClosed thenVal hcore.1.2,
         exprTouchesUnsupportedCallSurface_eq_false_of_coreClosed elseVal hcore.2]
+  | forkIfAtLeast _ thenExpr elseExpr =>
+      simp [exprTouchesUnsupportedCoreSurface] at hcore
   | mulDivDown a b c | mulDivUp a b c =>
       simp only [exprTouchesUnsupportedCoreSurface, Bool.or_eq_false_iff] at hcore
       simp [exprTouchesUnsupportedCallSurface,
@@ -4343,6 +4383,8 @@ theorem exprTouchesUnsupportedHelperSurface_eq_false_of_contractSurfaceClosed
         exprTouchesUnsupportedHelperSurface_eq_false_of_contractSurfaceClosed hsurface.1.1,
         exprTouchesUnsupportedHelperSurface_eq_false_of_contractSurfaceClosed hsurface.1.2,
         exprTouchesUnsupportedHelperSurface_eq_false_of_contractSurfaceClosed hsurface.2]
+  | forkIfAtLeast _ thenExpr elseExpr =>
+      simp [exprTouchesUnsupportedContractSurface] at hsurface
   | bitNot a =>
       simp only [exprTouchesUnsupportedContractSurface] at hsurface
       simp [exprTouchesUnsupportedHelperSurface,
@@ -4577,6 +4619,8 @@ private theorem exprUsesArrayElement_eq_false_of_coreClosed
         exprUsesArrayElement_eq_false_of_coreClosed hcore.1.1,
         exprUsesArrayElement_eq_false_of_coreClosed hcore.1.2,
         exprUsesArrayElement_eq_false_of_coreClosed hcore.2]
+  | forkIfAtLeast _ thenExpr elseExpr =>
+      simp [exprTouchesUnsupportedCoreSurface] at hcore
   | storage _ | storageAddr _ => simp [exprUsesArrayElement]
   | _ => simp [exprTouchesUnsupportedCoreSurface] at hcore
 termination_by sizeOf expr
@@ -4625,6 +4669,8 @@ private theorem exprUsesStorageArrayElement_eq_false_of_coreClosed
         exprUsesStorageArrayElement_eq_false_of_coreClosed hcore.1.1,
         exprUsesStorageArrayElement_eq_false_of_coreClosed hcore.1.2,
         exprUsesStorageArrayElement_eq_false_of_coreClosed hcore.2]
+  | forkIfAtLeast _ thenExpr elseExpr =>
+      simp [exprTouchesUnsupportedCoreSurface] at hcore
   | storage _ | storageAddr _ => simp [exprUsesStorageArrayElement]
   | arrayElement _ _ =>
       simp [exprTouchesUnsupportedCoreSurface] at hcore
@@ -4675,6 +4721,8 @@ private theorem exprUsesDynamicBytesEq_eq_false_of_coreClosed
         exprUsesDynamicBytesEq_eq_false_of_coreClosed hcore.1.1,
         exprUsesDynamicBytesEq_eq_false_of_coreClosed hcore.1.2,
         exprUsesDynamicBytesEq_eq_false_of_coreClosed hcore.2]
+  | forkIfAtLeast _ thenExpr elseExpr =>
+      simp [exprTouchesUnsupportedCoreSurface] at hcore
   | storage _ | storageAddr _ => simp [exprUsesDynamicBytesEq]
   | _ => simp [exprTouchesUnsupportedCoreSurface] at hcore
 termination_by sizeOf expr
diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index 59e28eba2..39b2d6707 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -2994,6 +2994,7 @@ end Verity.AxiomAudit
   -- Compiler.Proofs.IRGeneration.SourceSemantics.evalExpr_mulDivDown  -- private
   -- Compiler.Proofs.IRGeneration.SourceSemantics.evalExpr_mulDivUp  -- private
   -- Compiler.Proofs.IRGeneration.SourceSemantics.evalExpr_ite  -- private
+  -- Compiler.Proofs.IRGeneration.SourceSemantics.evalExpr_forkIfAtLeast  -- private
   Compiler.Proofs.IRGeneration.SourceSemantics.execStmtWithEvents_nil_eq_execStmt
   Compiler.Proofs.IRGeneration.SourceSemantics.execStmtListWithEvents_nil_eq_execStmtList
   Compiler.Proofs.IRGeneration.SourceSemantics.bindSupportedParams_take_param_length
@@ -5543,4 +5544,4 @@ end Verity.AxiomAudit
   Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
 ]
 
--- Total: 5242 theorems/lemmas (3628 public, 1614 private, 0 sorry'd)
+-- Total: 5243 theorems/lemmas (3628 public, 1615 private, 0 sorry'd)
diff --git a/Verity/Macro/Syntax.lean b/Verity/Macro/Syntax.lean
index b3242dacc..ed83b83ca 100644
--- a/Verity/Macro/Syntax.lean
+++ b/Verity/Macro/Syntax.lean
@@ -95,6 +95,7 @@ syntax "intrinsic_cancun " term:max ppSpace term:max ppSpace term:max : term
 syntax "intrinsic_prague " term:max ppSpace term:max ppSpace term:max : term
 syntax "intrinsic_fusaka " term:max ppSpace term:max ppSpace term:max : term
 syntax "intrinsic_osaka " term:max ppSpace term:max ppSpace term:max : term
+syntax "fork_if_at_least " ident ppSpace "then " term:max ppSpace "else " term:max : term
 syntax "adt " str : term
 syntax "adt " str " [" sepBy(term, ",") "]" : term
 syntax "tryCatch " term:max ppSpace term:max : doElem
@@ -110,6 +111,8 @@ macro_rules
       `(panic! "verity intrinsic has no default EDSL semantics; add a consumer macro_rules override")
   | `(intrinsic_osaka $_name:term $_lowering:term $_args:term) =>
       `(panic! "verity intrinsic has no default EDSL semantics; add a consumer macro_rules override")
+  | `(fork_if_at_least $_fork:ident then $thenExpr:term else $_elseExpr:term) =>
+      `($thenExpr)
   | `(adt $_variant:str) => `(0)
   | `(adt $_variant:str [ $[$_args:term],* ]) => `(0)
 syntax "revert " ident "(" sepBy(term, ",") ")" : doElem
diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index a226c5de5..22cae314b 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -36,6 +36,13 @@ private def hardForkTermFromParsed (fork : Verity.Core.Intrinsics.HardFork) : Co
   | .prague => `(Verity.Core.Intrinsics.HardFork.prague)
   | .osaka => `(Verity.Core.Intrinsics.HardFork.osaka)
 
+private def hardForkTermFromIdent (fork : TSyntax `ident) : CommandElabM Term := do
+  match Verity.Core.Intrinsics.HardFork.parse? (toString fork.getId) with
+  | some parsed => hardForkTermFromParsed parsed
+  | none =>
+      throwErrorAt fork
+        s!"unknown fork '{toString fork.getId}' (expected cancun, prague, osaka, or fusaka alias)"
+
 inductive ValueType where
   | uint256
   | int256
@@ -3227,6 +3234,14 @@ private partial def inferPureExprType
               (← inferPureExprType fields constDecls immutableDecls externalDecls params locals x visitingConstants)
           pure .uint256
       | _ => throwErrorAt args "expected list literal [..]"
+  | `(term| fork_if_at_least $fork:ident then $thenExpr:term else $elseExpr:term) =>
+      let thenTy ← inferPureExprType fields constDecls immutableDecls externalDecls params locals thenExpr visitingConstants
+      let elseTy ← inferPureExprType fields constDecls immutableDecls externalDecls params locals elseExpr visitingConstants
+      unless thenTy == elseTy do
+        throwErrorAt elseExpr
+          s!"fork_if_at_least branches must have the same type, got {renderValueType thenTy} and {renderValueType elseTy}"
+      let _ ← hardForkTermFromIdent fork
+      pure thenTy
   | `(term| structMember $field:term $key:term $member:term) => do
       let fieldName := ← expectStringOrIdent field
       let memberName := ← expectStringOrIdent member
@@ -4408,6 +4423,11 @@ partial def translatePureExprWithTypes
               s!"unknown intrinsic '{intrinsicName}'; declare it first with `verity_intrinsic` so the compiler can enforce min_fork"
       let minForkTerm ← hardForkTermFromParsed minFork
       translateIntrinsic name lowering args minForkTerm
+  | `(term| fork_if_at_least $fork:ident then $thenExpr:term else $elseExpr:term) =>
+      `(Compiler.CompilationModel.Expr.forkIfAtLeast
+          $(← hardForkTermFromIdent fork)
+          $(← translatePureExprWithTypes fields constDecls immutableDecls params locals thenExpr visitingConstants)
+          $(← translatePureExprWithTypes fields constDecls immutableDecls params locals elseExpr visitingConstants))
   | `(term| structMember $field:term $key:term $member:term) =>
       let fieldName := ← expectStringOrIdent field
       let memberName := ← expectStringOrIdent member
diff --git a/docs-site/content/intrinsics.mdx b/docs-site/content/intrinsics.mdx
index b073e2ef3..5d786e893 100644
--- a/docs-site/content/intrinsics.mdx
+++ b/docs-site/content/intrinsics.mdx
@@ -94,6 +94,33 @@ intrinsics while using an older target, it must pass
 `--allow-future-fork-intrinsics`; otherwise compilation fails before Yul is
 written.
 
+## Fork-Aware Fallback
+
+Use `fork_if_at_least` when a library has two semantically equivalent
+implementations and one implementation uses a newer opcode intrinsic:
+
+```lean
+def clz (x : Uint256) : Uint256 :=
+  fork_if_at_least osaka then
+    intrinsic_osaka "clz"
+      (Verity.Core.Intrinsics.YulLowering.verbatim 1 1 "1e")
+      [x]
+  else
+    clz_emulated x
+```
+
+This is compile-time selection. Both branches are typechecked by Verity, but the
+compiler erases the unselected branch according to `--target-fork` before
+running intrinsic fork checks and before emitting Yul. That means the native
+branch above remains a strict Osaka intrinsic, while a Cancun or Prague build
+sees only the emulated fallback.
+
+The semantic obligation belongs to the consumer: the selected branches should be
+proved or documented as equivalent for the source-level function. The default
+Lean elaboration of `fork_if_at_least` reduces to the `then` branch, so consumers
+that need fork-specific proof behavior should add their own local wrapper lemma
+or macro rule.
+
 ## Trust model
 
 Intrinsics deliberately keep Verity's project-level axiom count at zero. The
diff --git a/docs/INTRINSICS.md b/docs/INTRINSICS.md
index c9e94c7a1..a2427cf5c 100644
--- a/docs/INTRINSICS.md
+++ b/docs/INTRINSICS.md
@@ -111,6 +111,33 @@ intrinsics while using an older target, it must pass
 `--allow-future-fork-intrinsics`; otherwise compilation fails before Yul is
 written.
 
+## Fork-Aware Fallback
+
+Use `fork_if_at_least` when a library has two semantically equivalent
+implementations and one implementation uses a newer opcode intrinsic:
+
+```lean
+def clz (x : Uint256) : Uint256 :=
+  fork_if_at_least osaka then
+    intrinsic_osaka "clz"
+      (Verity.Core.Intrinsics.YulLowering.verbatim 1 1 "1e")
+      [x]
+  else
+    clz_emulated x
+```
+
+This is compile-time selection. Both branches are typechecked by Verity, but the
+compiler erases the unselected branch according to `--target-fork` before
+running intrinsic fork checks and before emitting Yul. That means the native
+branch above remains a strict Osaka intrinsic, while a Cancun or Prague build
+sees only the emulated fallback.
+
+The semantic obligation belongs to the consumer: the selected branches should be
+proved or documented as equivalent for the source-level function. The default
+Lean elaboration of `fork_if_at_least` reduces to the `then` branch, so consumers
+that need fork-specific proof behavior should add their own local wrapper lemma
+or macro rule.
+
 ## Audit Surface
 
 Consumer builds that use intrinsics should archive the normal compiler