diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
index 74209e98c4..3ea19db9d9 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -1273,13 +1273,14 @@ These operators make queries about the current execution state.
     rule <k> BASEFEE     => BFEE                        ~> #push ... </k> <baseFee> BFEE </baseFee>
     rule <k> BLOBBASEFEE => Cbasefeeperblob(SCHED, EXCESS_BLOB_GAS) ~> #push ... </k> <excessBlobGas> EXCESS_BLOB_GAS </excessBlobGas> <schedule> SCHED </schedule>  requires notBool #rangeNegUInt64(EXCESS_BLOB_GAS)
 
-    syntax NullStackOp ::= "COINBASE" | "TIMESTAMP" | "NUMBER" | "DIFFICULTY" | "PREVRANDAO"
- // ----------------------------------------------------------------------------------------
+    syntax NullStackOp ::= "COINBASE" | "TIMESTAMP" | "NUMBER" | "DIFFICULTY" | "PREVRANDAO" | "SLOTNUM"
+ // ---------------------------------------------------------------------------------------------------
     rule <k> COINBASE   => CB   ~> #push ... </k> <coinbase> CB </coinbase>
     rule <k> TIMESTAMP  => TS   ~> #push ... </k> <timestamp> TS </timestamp>
     rule <k> NUMBER     => NUMB ~> #push ... </k> <number> NUMB </number>
     rule <k> DIFFICULTY => DIFF ~> #push ... </k> <difficulty> DIFF </difficulty>
     rule <k> PREVRANDAO => RDAO ~> #push ... </k> <mixHash> RDAO </mixHash>
+    rule <k> SLOTNUM    => SN   ~> #push ... </k> <slotNumber> SN </slotNumber>
 
     syntax NullStackOp ::= "ADDRESS" | "ORIGIN" | "CALLER" | "CALLVALUE" | "CHAINID" | "SELFBALANCE"
  // ------------------------------------------------------------------------------------------------
@@ -2961,6 +2962,7 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H).
     rule <k> #gasExec(SCHED, COINBASE)       => Gbase < SCHED > ... </k>
     rule <k> #gasExec(SCHED, TIMESTAMP)      => Gbase < SCHED > ... </k>
     rule <k> #gasExec(SCHED, NUMBER)         => Gbase < SCHED > ... </k>
+    rule <k> #gasExec(SCHED, SLOTNUM)        => Gbase < SCHED > ... </k>
     rule <k> #gasExec(SCHED, DIFFICULTY)     => Gbase < SCHED > ... </k>
     rule <k> #gasExec(SCHED, PREVRANDAO)     => Gbase < SCHED > ... </k>
     rule <k> #gasExec(SCHED, GASLIMIT)       => Gbase < SCHED > ... </k>
@@ -3255,6 +3257,7 @@ After interpreting the strings representing programs as a `WordStack`, it should
     rule #dasmOpCode(  72, SCHED ) => BASEFEE     requires Ghasbasefee     << SCHED >>
     rule #dasmOpCode(  73, SCHED ) => BLOBHASH    requires Ghasblobhash    << SCHED >>
     rule #dasmOpCode(  74, SCHED ) => BLOBBASEFEE requires Ghasblobbasefee << SCHED >>
+    rule #dasmOpCode(  75, SCHED ) => SLOTNUM     requires Ghasslotnum     << SCHED >>
     rule #dasmOpCode(  80,     _ ) => POP
     rule #dasmOpCode(  81,     _ ) => MLOAD
     rule #dasmOpCode(  82,     _ ) => MSTORE
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md
index c00fda36af..c81a8a6e68 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md
@@ -32,6 +32,7 @@ module SCHEDULE
                           | "Ghasbeaconroot"          | "Ghaseip6780"      | "Ghasblobbasefee"     | "Ghasblobhash"
                           | "Ghasbls12msmdiscount"    | "Ghashistory"      | "Ghasrequests"        | "Ghasauthority"
                           | "Ghasfloorcost"           | "Ghasclz"          | "Ghasreserve"         | "Ghastxgaslimit"
+                          | "Ghasslotnum"
  // -----------------------------------------------------------------------------------------------------------------
 ```
 
@@ -187,6 +188,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule [GhasclzDefault]:                 Ghasclz                 << DEFAULT >> => false
     rule [GhasreserveDefault]:             Ghasreserve             << DEFAULT >> => false
     rule [GhastxgaslimitDefault]:          Ghastxgaslimit          << DEFAULT >> => false
+    rule [GhasslotnumDefault]:             Ghasslotnum             << DEFAULT >> => false
 ```
 
 ### Frontier Schedule
@@ -543,7 +545,9 @@ A `ScheduleConst` is a constant determined by the fee schedule.
                   orBool SCHEDCONST ==K maxInitCodeSize
                        )
 
-    rule [SCHEDFLAGAmsterdam]: SCHEDFLAG << AMSTERDAM >> => SCHEDFLAG << OSAKA >>
+    rule [GhasslotnumAmsterdam]: Ghasslotnum << AMSTERDAM >> => true
+    rule [SCHEDFLAGAmsterdam]:   SCHEDFLAG   << AMSTERDAM >> => SCHEDFLAG << OSAKA >>
+      requires notBool ( SCHEDFLAG ==K Ghasslotnum )
 ```
 
 ```k