diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
index f879eacde5..7abd7970c9 100644
--- a/kevm-pyk/pyproject.toml
+++ b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.411"
+version = "1.0.412"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
index ad71417dc7..cc29c3b0e4 100644
--- a/kevm-pyk/src/kevm_pyk/__init__.py
+++ b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.411'
+VERSION: Final = '1.0.412'
diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py
index 8ca993b36a..b097960374 100644
--- a/kevm-pyk/src/kevm_pyk/kevm.py
+++ b/kevm-pyk/src/kevm_pyk/kevm.py
@@ -12,7 +12,7 @@
 from pyk.ktool.kprove import KProve
 from pyk.ktool.krun import KRun
 from pyk.prelude.kint import intToken, ltInt
-from pyk.prelude.ml import mlEqualsTrue
+from pyk.prelude.ml import mlEqualsFalse, mlEqualsTrue
 from pyk.prelude.string import stringToken
 from pyk.proof.reachability import APRBMCProof, APRProof
 from pyk.proof.show import APRBMCProofNodePrinter, APRProofNodePrinter
@@ -242,6 +242,21 @@ def short_info(self, cterm: CTerm) -> list[str]:
 
     @staticmethod
     def add_invariant(cterm: CTerm) -> CTerm:
+        def _add_account_invariant(account: KApply) -> list[KApply]:
+            _account_constraints = []
+            acct_id, balance, nonce = account.args[0], account.args[1], account.args[5]
+
+            if type(acct_id) is KApply and type(acct_id.args[0]) is KVariable:
+                _account_constraints.append(mlEqualsTrue(KEVM.range_address(acct_id.args[0])))
+                _account_constraints.append(
+                    mlEqualsFalse(KEVM.is_precompiled_account(acct_id.args[0], cterm.cell('SCHEDULE_CELL')))
+                )
+            if type(balance) is KApply and type(balance.args[0]) is KVariable:
+                _account_constraints.append(mlEqualsTrue(KEVM.range_uint(256, balance.args[0])))
+            if type(nonce) is KApply and type(nonce.args[0]) is KVariable:
+                _account_constraints.append(mlEqualsTrue(KEVM.range_nonce(nonce.args[0])))
+            return _account_constraints
+
         constraints = []
         word_stack = cterm.cell('WORDSTACK_CELL')
         if type(word_stack) is not KVariable:
@@ -249,9 +264,17 @@ def add_invariant(cterm: CTerm) -> CTerm:
             for i in word_stack_items[:-1]:
                 constraints.append(mlEqualsTrue(KEVM.range_uint(256, i)))
 
-        gas_cell = cterm.cell('GAS_CELL')
-        if not (type(gas_cell) is KApply and gas_cell.label.name == 'infGas'):
-            constraints.append(mlEqualsTrue(KEVM.range_uint(256, gas_cell)))
+        accounts_cell = cterm.cell('ACCOUNTS_CELL')
+        if type(accounts_cell) is not KApply('.AccountCellMap'):
+            accounts = flatten_label('_AccountCellMap_', cterm.cell('ACCOUNTS_CELL'))
+            for wrapped_account in accounts:
+                if not (type(wrapped_account) is KApply and wrapped_account.label.name == 'AccountCellMapItem'):
+                    continue
+
+                account = wrapped_account.args[1]
+                if type(account) is KApply:
+                    constraints.extend(_add_account_invariant(account))
+
         constraints.append(mlEqualsTrue(KEVM.range_address(cterm.cell('ID_CELL'))))
         constraints.append(mlEqualsTrue(KEVM.range_address(cterm.cell('CALLER_CELL'))))
         constraints.append(mlEqualsTrue(KEVM.range_address(cterm.cell('ORIGIN_CELL'))))
@@ -315,6 +338,10 @@ def range_bool(i: KInner) -> KApply:
     def range_bytes(width: KInner, ba: KInner) -> KApply:
         return KApply('#rangeBytes(_,_)_WORD_Bool_Int_Int', [width, ba])
 
+    @staticmethod
+    def range_nonce(i: KInner) -> KApply:
+        return KApply('#rangeNonce(_)_WORD_Bool_Int', [i])
+
     @staticmethod
     def range_blocknum(ba: KInner) -> KApply:
         return KApply('#rangeBlockNum(_)_WORD_Bool_Int', [ba])
@@ -343,6 +370,10 @@ def bin_runtime(c: KInner) -> KApply:
     def init_bytecode(c: KInner) -> KApply:
         return KApply('initBytecode', [c])
 
+    @staticmethod
+    def is_precompiled_account(i: KInner, s: KInner) -> KApply:
+        return KApply('#isPrecompiledAccount(_,_)_EVM_Bool_Int_Schedule', [i, s])
+
     @staticmethod
     def hashed_location(compiler: str, base: KInner, offset: KInner, member_offset: int = 0) -> KApply:
         location = KApply(
diff --git a/package/version b/package/version
index 144afd4a20..2b9c98c876 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-1.0.411
+1.0.412