diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index a2d13ffaad..b365dbb51b 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -101,7 +101,7 @@ jobs:
             test-suite: 'test-prove-functional'
             test-args:
             timeout: 45
-            parallel: 2
+            parallel: 3
           - name: 'Optimizations'
             test-suite: 'test-prove-optimizations'
             test-args:
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 6732b424a3..95b5434c96 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -377,11 +377,22 @@ The `#next [_]` operator initiates execution by:
 -   `#stackDelta` is the delta the stack will have after the opcode executes.
 
 ```k
-    syntax Bool ::= #stackUnderflow ( WordStack , OpCode ) [symbol(#stackUnderflow), macro]
-                  | #stackOverflow  ( WordStack , OpCode ) [symbol(#stackOverflow), macro]
- // --------------------------------------------------------------------------------------
-    rule #stackUnderflow(WS, OP:OpCode) => #sizeWordStack(WS) <Int #stackNeeded(OP)
-    rule #stackOverflow (WS, OP) => (#stackDelta(OP) >Int 0) andBool (#sizeWordStack(WS) +Int #stackDelta(OP) >Int 1024)
+    syntax Bool ::= #stackUnderflow ( WordStack , OpCode ) [symbol(#stackUnderflow), function, total]
+                  | #stackOverflow  ( WordStack , OpCode ) [symbol(#stackOverflow), function, total]
+ // ------------------------------------------------------------------------------------------------
+    rule #stackUnderflow(                                                 _WS , _POP:PushOp      ) => false
+    rule #stackUnderflow(                                                 _WS , _IOP:InvalidOp   ) => false
+    rule #stackUnderflow(                                                 _WS , _NOP:NullStackOp ) => false
+    rule #stackUnderflow( _W0 :                                           _WS , _UOP:UnStackOp   ) => false
+    rule #stackUnderflow( _W0 : _W1 :                                     _WS , BOP:BinStackOp   ) => false requires notBool isLogOp(BOP)
+    rule #stackUnderflow( _W0 : _W1 : _W2 :                               _WS , _TOP:TernStackOp ) => false
+    rule #stackUnderflow( _W0 : _W1 : _W2 : _W3 :                         _WS , _QOP:QuadStackOp ) => false
+    rule #stackUnderflow( _W0 : _W1 : _W2 : _W3 : _W4 : _W5 : _W6 :       _WS , _CSOP:CallSixOp  ) => false
+    rule #stackUnderflow( _W0 : _W1 : _W2 : _W3 : _W4 : _W5 : _W6 : _W7 : _WS , COP:CallOp       ) => false requires notBool isCallSixOp(COP)
+    rule #stackUnderflow(WS, OP:OpCode) => #sizeWordStack(WS) <Int #stackNeeded(OP) [owise]
+
+    rule #stackOverflow(_WS, OP) => false requires #stackDelta(OP) <=Int 0
+    rule #stackOverflow(WS, OP) => 1024 <Int #sizeWordStack(WS) +Int #stackDelta(OP) [owise]
 
     syntax Int ::= #stackNeeded ( OpCode ) [symbol(#stackNeeded), function]
  // -----------------------------------------------------------------------