diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs
index 210d37a37..294de0ee4 100644
--- a/src/EVM/SMT.hs
+++ b/src/EVM/SMT.hs
@@ -28,6 +28,7 @@ import Data.Text.Lazy (Text)
 import Data.Text qualified as TS
 import Data.Text.Lazy qualified as T
 import Data.Text.Lazy.Builder
+import Data.Text.Read (decimal)
 import Language.SMT2.Parser (getValueRes, parseCommentFreeFileMsg)
 import Language.SMT2.Syntax (Symbol, SpecConstant(..), GeneralRes(..), Term(..), QualIdentifier(..), Identifier(..), Sort(..), Index(..), VarBinding(..))
 import Numeric (readHex, readBin)
@@ -232,6 +233,7 @@ assertPropsNoSimp psPreConc = do
   <> smt2Line ""
   <> keccakAssertions'
   <> readAssumes'
+  <> gasOrder
   <> smt2Line ""
   <> SMT2 (fmap (\p -> "(assert " <> p <> ")") encs) mempty mempty
   <> SMT2 smt mempty mempty
@@ -256,6 +258,7 @@ assertPropsNoSimp psPreConc = do
     allVars = fmap referencedVars toDeclarePsElim <> fmap referencedVars bufVals <> fmap referencedVars storeVals <> [abstrVars abst]
     frameCtx = fmap referencedFrameContext toDeclarePsElim <> fmap referencedFrameContext bufVals <> fmap referencedFrameContext storeVals
     blockCtx = fmap referencedBlockContext toDeclarePsElim <> fmap referencedBlockContext bufVals <> fmap referencedBlockContext storeVals
+    gasOrder = enforceGasOrder psPreConc
 
     abstrVars :: AbstState -> [Builder]
     abstrVars (AbstState b _) = map ((\v->fromString ("abst_" ++ show v)) . snd) (Map.toList b)
@@ -321,7 +324,7 @@ referencedFrameContext expr = nubOrd $ foldTerm go [] expr
     go = \case
       TxValue -> [(fromString "txvalue", [])]
       v@(Balance a) -> [(fromString "balance_" <> formatEAddr a, [PLT v (Lit $ 2 ^ (96 :: Int))])]
-      Gas {} -> internalError "TODO: GAS"
+      Gas freshVar -> [(fromString ("gas_" <> show freshVar), [])]
       _ -> []
 
 referencedBlockContext :: TraversableTerm a => a -> [(Builder, [Prop])]
@@ -438,6 +441,23 @@ declareAddrs names = SMT2 (["; symbolic addresseses"] <> fmap declare names) cex
     declare n = "(declare-fun " <> n <> " () Addr)"
     cexvars = (mempty :: CexVars){ addrs = fmap toLazyText names }
 
+enforceGasOrder :: [Prop] -> SMT2
+enforceGasOrder ps = SMT2 (["; gas ordering"] <> order names) mempty mempty
+  where
+    order :: [Int] -> [Builder]
+    order n = consecutivePairs n >>= \case
+      -- The GAS instruction itself costs gas, so it's strictly decreasing
+      (x, y) -> ["(assert (bvult gas_" <> (fromString . show $ x) <> " gas_" <> (fromString . show $ y) <> "))"]
+    consecutivePairs :: [Int] -> [(Int, Int)]
+    consecutivePairs [] = []
+    consecutivePairs [_] = []
+    consecutivePairs (x:y:xs) = (x, y) : consecutivePairs (y:xs)
+    names :: [Int] = nubOrd $ concatMap (foldProp go mempty) ps
+    go :: Expr a -> [Int]
+    go e = case e of
+      Gas freshVar -> [freshVar]
+      _ -> []
+
 declareFrameContext :: [(Builder, [Prop])] -> Err SMT2
 declareFrameContext names = do
   decls <- concatMapM declare names
@@ -845,6 +865,7 @@ exprToSMT = \case
     encPrev <- exprToSMT prev
     pure $ "(store" `sp` encPrev `sp` encIdx `sp` encVal <> ")"
   SLoad idx store -> op2 "select" store idx
+  Gas freshVar -> pure $ fromLazyText $ "gas_"  <> (T.pack $ show freshVar)
 
   a -> internalError $ "TODO: implement: " <> show a
   where
@@ -1015,6 +1036,11 @@ parseEAddr name
   | Just a <- TS.stripPrefix "symaddr_" name = SymAddr a
   | otherwise = internalError $ "cannot parse: " <> show name
 
+textToInt :: TS.Text -> Int
+textToInt text = case decimal text of
+  Right (value, _) -> value
+  Left _ -> internalError $ "cannot parse '" <> (TS.unpack text) <> "' into an Int"
+
 parseBlockCtx :: TS.Text -> Expr EWord
 parseBlockCtx "origin" = Origin
 parseBlockCtx "coinbase" = Coinbase
@@ -1024,12 +1050,14 @@ parseBlockCtx "prevrandao" = PrevRandao
 parseBlockCtx "gaslimit" = GasLimit
 parseBlockCtx "chainid" = ChainId
 parseBlockCtx "basefee" = BaseFee
-parseBlockCtx t = internalError $ "cannot parse " <> (TS.unpack t) <> " into an Expr"
+parseBlockCtx gas | TS.isPrefixOf (TS.pack "gas_") gas = Gas (textToInt $ TS.drop 4 gas)
+parseBlockCtx val = internalError $ "cannot parse '" <> (TS.unpack val) <> "' into an Expr"
 
 parseTxCtx :: TS.Text -> Expr EWord
 parseTxCtx name
   | name == "txvalue" = TxValue
   | Just a <- TS.stripPrefix "balance_" name = Balance (parseEAddr a)
+  | Just a <- TS.stripPrefix "gas_" name = Gas (textToInt a)
   | otherwise = internalError $ "cannot parse " <> (TS.unpack name) <> " into an Expr"
 
 getAddrs :: (TS.Text -> Expr EAddr) -> (Text -> IO Text) -> [TS.Text] -> IO (Map (Expr EAddr) Addr)
diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
index 13aac47f3..766dbd7fc 100644
--- a/src/EVM/Types.hs
+++ b/src/EVM/Types.hs
@@ -286,7 +286,7 @@ data Expr (a :: EType) where
 
   Balance        :: Expr EAddr -> Expr EWord
 
-  Gas            :: Int                -- frame idx
+  Gas            :: Int                -- fresh gas variable
                  -> Expr EWord
 
   -- code