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 dba74d67fc..5376080ccb 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md
@@ -31,8 +31,8 @@ module SCHEDULE
                           | "Ghaswarmcoinbase"        | "Ghaswithdrawals"  | "Ghastransient"       | "Ghasmcopy"
                           | "Ghasbeaconroot"          | "Ghaseip6780"      | "Ghasblobbasefee"     | "Ghasblobhash"
                           | "Ghasbls12msmdiscount"    | "Ghashistory"      | "Ghasrequests"        | "Ghasauthority"
-                          | "Ghasfloorcost"           | "Ghasclz"
- // -------------------------------------------------------------
+                          | "Ghasfloorcost"           | "Ghasclz"          | "Ghastxgaslimit"
+ // -----------------------------------------------------------------------------------------
 ```
 
 ### Schedule Constants
@@ -53,7 +53,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
                            | "Gaccessliststoragekey"           | "Rmaxquotient"  | "Ginitcodewordcost" | "maxInitCodeSize"    | "Gwarmstoragedirtystore"
                            | "Gpointeval"    | "Gmaxblobgas"   | "Gminbasefee"   | "Gtargetblobgas"    | "Gperblob"           | "Blobbasefeeupdatefraction"
                            | "Gbls12g1add"   | "Gbls12g1mul"   | "Gbls12g2add"   | "Gbls12g2mul"       | "Gbls12mapfptog1"    | "Gbls12PairingCheckMul"
-                           | "Gbls12PairingCheckAdd"           | "Gauthbase"     | "Gbls12mapfp2tog2"  | "Gtxdatafloor"
+                           | "Gbls12PairingCheckAdd"           | "Gauthbase"     | "Gbls12mapfp2tog2"  | "Gtxdatafloor"       | "Gmaxtxgaslimit"
  // -------------------------------------------------------------------------------------------------------------------------------------------------------
 ```
 
@@ -148,6 +148,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule [Gbls12PairingCheckAddDefault]: Gbls12PairingCheckAdd < DEFAULT > => 0
     rule [Gbls12mapfptog1Default]:       Gbls12mapfptog1       < DEFAULT > => 0
     rule [Gbls12mapfp2tog2Default]:      Gbls12mapfp2tog2      < DEFAULT > => 0
+    rule [GmaxtxgaslimitDefault]:        Gmaxtxgaslimit        < DEFAULT > => 0
 
     rule [GselfdestructnewaccountDefault]: Gselfdestructnewaccount << DEFAULT >> => false
     rule [GstaticcalldepthDefault]:        Gstaticcalldepth        << DEFAULT >> => true
@@ -183,6 +184,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule [GhasauthorityDefault]:           Ghasauthority           << DEFAULT >> => false
     rule [GhasfloorcostDefault]:           Ghasfloorcost           << DEFAULT >> => false
     rule [GhasclzDefault]:                 Ghasclz                 << DEFAULT >> => false
+    rule [GhastxgaslimitDefault]:          Ghastxgaslimit          << DEFAULT >> => false
 ```
 
 ### Frontier Schedule
@@ -504,12 +506,16 @@ A `ScheduleConst` is a constant determined by the fee schedule.
 ```k
     syntax Schedule ::= "OSAKA" [symbol(OSAKA_EVM), smtlib(schedule_OSAKA)]
  // -----------------------------------------------------------------------
-    rule [SCHEDCONSTOsaka]: SCHEDCONST < OSAKA > => SCHEDCONST < PRAGUE >
-
-    rule [GhasclzOsaka]:    Ghasclz    << OSAKA >> => true
-    rule [SCHEDFLAGOsaka]:  SCHEDFLAG  << OSAKA >> => SCHEDFLAG << PRAGUE >>
-      requires notBool ( SCHEDFLAG ==K Ghasclz )
-    
+    rule [GmaxtxgaslimitOsaka]: Gmaxtxgaslimit < OSAKA > => 16777216
+    rule [SCHEDCONSTOsaka]:     SCHEDCONST     < OSAKA > => SCHEDCONST < PRAGUE >
+      requires notBool ( SCHEDCONST ==K Gmaxtxgaslimit )
+
+    rule [GhasclzOsaka]:        Ghasclz        << OSAKA >> => true
+    rule [GhastxgaslimitOsaka]: Ghastxgaslimit << OSAKA >> => true
+    rule [SCHEDFLAGOsaka]:      SCHEDFLAG      << OSAKA >> => SCHEDFLAG << PRAGUE >>
+      requires notBool ( SCHEDFLAG ==K Ghasclz
+                  orBool SCHEDFLAG ==K Ghastxgaslimit
+                       )
 ```
 
 ```k
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md
index 70edd93a16..fb05f739f6 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md
@@ -612,6 +612,7 @@ The `"rlp"` key loads the block information.
       andBool TX_MAX_PRIORITY_FEE <=Int TX_MAX_FEE
       andBool BAL >=Int TX_GAS_LIMIT *Int TX_MAX_FEE +Int VALUE
       andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT
+      andBool (notBool Ghastxgaslimit << SCHED >> orBool TX_GAS_LIMIT <=Int Gmaxtxgaslimit < SCHED >)
       andBool size(TX_AUTH_LIST) >Int 0 andBool #checkAuthorityList(TX_AUTH_LIST)
 
     rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]]
@@ -648,6 +649,7 @@ The `"rlp"` key loads the block information.
       andBool TX_MAX_BLOB_FEE >=Int Cbasefeeperblob(SCHED, EXCESS_BLOB_GAS)
       andBool BAL >=Int TX_GAS_LIMIT *Int TX_MAX_FEE +Int (Ctotalblob(SCHED, size(TVH)) *Int TX_MAX_BLOB_FEE) +Int VALUE
       andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT
+      andBool (notBool Ghastxgaslimit << SCHED >> orBool TX_GAS_LIMIT <=Int Gmaxtxgaslimit < SCHED >)
       andBool Ctotalblob(SCHED, size(TVH)) <=Int Gmaxblobgas < SCHED>
 
     rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]]
@@ -677,6 +679,7 @@ The `"rlp"` key loads the block information.
       andBool TX_MAX_PRIORITY_FEE <=Int TX_MAX_FEE
       andBool BAL >=Int TX_GAS_LIMIT *Int TX_MAX_FEE +Int VALUE
       andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT
+      andBool (notBool Ghastxgaslimit << SCHED >> orBool TX_GAS_LIMIT <=Int Gmaxtxgaslimit < SCHED >)
 
     rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]]
          <schedule> SCHED </schedule>
@@ -704,6 +707,7 @@ The `"rlp"` key loads the block information.
       andBool BASE_FEE <=Int TX_GAS_PRICE
       andBool BAL >=Int TX_GAS_LIMIT *Int TX_GAS_PRICE +Int VALUE
       andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT
+      andBool (notBool Ghastxgaslimit << SCHED >> orBool TX_GAS_LIMIT <=Int Gmaxtxgaslimit < SCHED >)
 
     rule #isValidTransaction (_, _) => false [owise]
 ```