diff --git a/test/FixedPointMathLib.k.sol b/test/FixedPointMathLib.k.sol
index 4ed260c8..74794028 100644
--- a/test/FixedPointMathLib.k.sol
+++ b/test/FixedPointMathLib.k.sol
@@ -10,7 +10,7 @@ contract FixedPointMathLibVerification is Test, KontrolCheats {
     // Constants
     uint256 constant WAD = 1e18;
 
-    // Public wrapper for mulWad since Kontrol doesn't support vm.expectRevert
+        // Public wrapper for mulWad since Kontrol doesn't support vm.expectRevert
     // for internal calls, and FixedPointMathLib.mulWad is internal
     function mulWad(uint x, uint y) public pure returns (uint256) {
         return FixedPointMathLib.mulWad(x, y);
@@ -30,7 +30,7 @@ contract FixedPointMathLibVerification is Test, KontrolCheats {
 
             assert(zImpl == zSpec);
         } else {
-            vm.expectRevert(FixedPointMathLib.MulWadFailed.selector); // FixedPointMathLib.MulWadFailed.selector
+            vm.expectRevert(FixedPointMathLib.MulWadFailed.selector);
             this.mulWad(x, y);
         }
 
@@ -44,8 +44,60 @@ contract FixedPointMathLibVerification is Test, KontrolCheats {
 
             assert(zImpl == zSpec);
         } else {
-            vm.expectRevert(FixedPointMathLib.MulWadFailed.selector); // FixedPointMathLib.MulWadFailed.selector
+            vm.expectRevert(FixedPointMathLib.MulWadFailed.selector);
             this.mulWadUp(x, y);
         }
     }
+
+    //function log2(uint256 x) internal pure returns (uint256 r) {
+    //    /// @solidity memory-safe-assembly
+    //    assembly {
+    //        r := shl(7, lt(0xffffffffffffffffffffffffffffffff, x))
+    //        r := or(r, shl(6, lt(0xffffffffffffffff, shr(r, x))))
+    //        r := or(r, shl(5, lt(0xffffffff, shr(r, x))))
+    //        r := or(r, shl(4, lt(0xffff, shr(r, x))))
+    //        r := or(r, shl(3, lt(0xff, shr(r, x))))
+    //        r := or(r, shl(2, lt(0xf, shr(r, x))))
+    //        r := or(r, byte(shr(r, x), hex"00000101020202020303030303030303"))
+    //    }
+    //}
+
+    //function testMyLog2(uint256 x) public {
+    //    uint256 r = log2(x);
+    //    if(x > 0)
+    //        assertLe(2**r, x);
+    //    else
+    //        assertEq(r,0);
+    //}
+
+    function testLog2(uint256 x) public pure {
+
+        unchecked {
+          uint256 y = x; uint256 z = 0;
+          if (2 ** 128 - 1 < y) { y = y >> 128; } else { }
+          if (2 **  64 - 1 < y) { y = y >>  64; } else { }
+          if (2 **  32 - 1 < y) { y = y >>  32; } else { }
+          if (2 **  16 - 1 < y) { y = y >>  16; } else { }
+          if (2 **   8 - 1 < y) { y = y >>   8; } else { }
+          if (2 **   4 - 1 < y) { y = y >>   4; } else { }
+
+          if (2 ** 3 - 1 < y) z = 4; else
+          if (2 ** 2 - 1 < y) z = 3; else
+          if (2 ** 1 - 1 < y) z = 2; else
+          if (2 ** 0 - 1 < y) z = 1;
+        }
+
+        uint256 r = FixedPointMathLib.log2(x);
+
+        if(x > 0){
+            assertLe(2**r, x);
+            if (r < 255) {
+              assertLt(x, 2**(r+1));
+            } else {
+              assertEq(r, 255);
+            }
+        }
+        else
+            assertEq(r,0);
+    }
 }
diff --git a/test/run-kevm.sh b/test/run-kevm.sh
index 4fdd7f30..c0c996e3 100755
--- a/test/run-kevm.sh
+++ b/test/run-kevm.sh
@@ -7,14 +7,15 @@ forge_build() {
 }
 
 kontrol_kompile() {
-    kontrol build                     \
-            --verbose                 \
-            --require ${lemmas}       \
-            --module-import ${module} \
+    GHCRTS='' kontrol build                     \
+          --verbose                 \
+          --require ${lemmas}       \
+          --module-import ${module} \
             ${rekompile}
 }
 
 kontrol_prove() {
+    export GHCRTS='-N6'
     kontrol prove                              \
             --max-depth ${max_depth}           \
             --max-iterations ${max_iterations} \
@@ -29,7 +30,8 @@ kontrol_prove() {
             ${break_every_step}                \
             ${break_on_calls}                  \
             ${tests}                           \
-            ${use_booster}
+            --max-frontier-parallel 6 \
+            --kore-rpc-command 'kore-rpc-booster --equation-max-recursion 10'
 }
 
 kontrol_claim() {
@@ -51,7 +53,7 @@ smt_timeout=100000
 
 # Number of processes run by the prover in parallel
 # Should be at most (M - 8) / 8 in a machine with M GB of RAM
-workers=12
+workers=3
 
 # Switch the options below to turn them on or off
 rekompile=--rekompile
@@ -89,9 +91,10 @@ use_booster=--use-booster
 tests=""
 tests+="--match-test FixedPointMathLibVerification.testMulWad(uint256,uint256) "
 tests+="--match-test FixedPointMathLibVerification.testMulWadUp "
+tests+="--match-test FixedPointMathLibVerification.testLog2 "
 
 # Name of the claim to execute
-claim=mulWadUp-first-roadblock
+claim=log2-06
 
 # Comment these lines as needed
 pkill kore-rpc || true
diff --git a/test/solady-lemmas.k b/test/solady-lemmas.k
index d3f301a5..49dcfe4b 100644
--- a/test/solady-lemmas.k
+++ b/test/solady-lemmas.k
@@ -20,7 +20,6 @@ module SOLADY-LEMMAS
 
     rule <k> runLemma(T) => doneLemma(T) ... </k>
 
-
     //
     // Bool
     //
@@ -28,28 +27,180 @@ module SOLADY-LEMMAS
     rule bool2Word ( X ) => 1 requires X         [simplification]
     rule bool2Word ( X ) => 0 requires notBool X [simplification]
 
+    rule chop ( bool2Word ( X ) <<Int Y ) => bool2Word ( X ) <<Int Y requires Y <Int 256 [simplification]
+
+    rule chop ( 1 <<Int Y ) => 1 <<Int Y requires Y <Int 256 [simplification]
+
+    rule ( A:Int >>Int B:Int ) >>Int C:Int => A >>Int ( B +Int C ) [simplification]
+
+    rule A =/=Int B => notBool ( A ==Int B )
+      [simplification, comm]
+
+    rule #Ceil ( byte (X:Int, Y:Int) ) => #Top
+      requires 0 <=Int X andBool X <Int 32
+       andBool 0 <=Int Y andBool Y <Int pow256
+       [simplification]
+
     //
-    // ML
+    // Bitwise
     //
 
-    rule #Not ( { false #Equals X:Bool andBool Y:Bool } ) => {true #Equals X } #And { true #Equals Y } [simplification]
+    rule A >>Int B ==Int 0 => log2Int ( A ) <=Int B
+      [simplification, comm, concrete(A)]
 
-    //
-    // Arithmetic
-    // 
+    rule 0 <=Int A >>Int B => true
+      requires 0 <=Int A andBool 0 <=Int B
+      [simplification]
+
+    rule A >>Int B <=Int C => A <=Int ( C <<Int B ) +Int ( 2 ^Int B ) -Int 1
+      requires C +Int 1 ==Int 2 ^Int ( log2Int ( C +Int 1 ) )
+      [simplification, concrete(B, C)]
+
+    rule C <Int A >>Int B => ( C <<Int B ) +Int ( 2 ^Int B ) -Int 1 <Int A
+    requires C +Int 1 ==Int 2 ^Int ( log2Int ( C +Int 1 ) )
+      [simplification, concrete(B, C)]
 
     rule X xorInt maxUInt256 => maxUInt256 -Int X
       requires #rangeUInt ( 256 , X )
       [simplification]
 
+    //
+    // Comparisons
+    //
+
+    // Concrete to the left of comparisons, prioritising <=Int and <Int
+    rule X >=Int Y => Y <=Int X [simplification, concrete(Y)]
+    rule X  >Int Y => Y  <Int X [simplification, concrete(Y)]
+
+    // Negations at K-level
+    rule notBool X <=Int Y => Y  <Int X [simplification]
+    rule notBool X  <Int Y => Y <=Int X [simplification]
+    rule notBool X  >Int Y => X <=Int Y [simplification]
+    rule notBool X >=Int Y => X  <Int Y [simplification]
+
+    // Negations ad ML-level
+    rule { true #Equals ( notBool X <=Int Y ) } => { true #Equals Y  <Int X } [simplification]
+    rule { true #Equals ( notBool X  <Int Y ) } => { true #Equals Y <=Int X } [simplification]
+    rule { true #Equals ( notBool X  >Int Y ) } => { true #Equals X <=Int Y } [simplification]
+    rule { true #Equals ( notBool X >=Int Y ) } => { true #Equals X  <Int Y } [simplification]
+    rule { ( notBool X <=Int Y ) #Equals true } => { true #Equals Y  <Int X } [simplification]
+    rule { ( notBool X  <Int Y ) #Equals true } => { true #Equals Y <=Int X } [simplification]
+    rule { ( notBool X  >Int Y ) #Equals true } => { true #Equals X <=Int Y } [simplification]
+    rule { ( notBool X >=Int Y ) #Equals true } => { true #Equals X  <Int Y } [simplification]
+
+    //
+    // Arithmetic
+    //
+
+    rule A modInt B => A
+      requires 0 <=Int A andBool A <Int B
+      [simplification]
+
+    rule A *Int B <Int C => A <Int C /Int B
+      requires C modInt B ==Int 0
+      [simplification, concrete(B, C)]
+
+    rule A <=Int B *Int C => A /Int C <=Int B
+      requires A modInt C ==Int 0
+      [simplification, concrete(A, C)]
+
+    rule A <=Int B -Int C => C <=Int B -Int A
+      [simplification, concrete(A, B)]
+
+    //
+    // Specialised
+    //
+
+    syntax Int ::= "cachedBytesConstant" [alias]
+    rule cachedBytesConstant => 6928917744019834342450304135053993530982274426945361611473370484834304
+
+    rule ( cachedBytesConstant >>Int ( ( maxUInt5 -Int Y ) *Int 8 ) ) modInt 256 => 0
+      requires 0 <=Int Y andBool Y <Int 32
+       andBool ( Y <=Int 1 orBool Y >=Int 16 )
+      [simplification]
+
+    rule ( cachedBytesConstant >>Int ( ( maxUInt5 -Int Y ) *Int 8 ) ) modInt 256 => 1
+      requires 0 <=Int Y andBool Y <Int 32
+       andBool 1 <Int Y andBool Y <=Int 3
+      [simplification]
+
+    rule ( cachedBytesConstant >>Int ( ( maxUInt5 -Int Y ) *Int 8 ) ) modInt 256 => 2
+      requires 0 <=Int Y andBool Y <Int 32
+       andBool 3 <Int Y andBool Y <=Int 7
+      [simplification]
+
+    rule ( cachedBytesConstant >>Int ( ( maxUInt5 -Int Y ) *Int 8 ) ) modInt 256 => 3
+      requires 0 <=Int Y andBool Y <Int 32
+       andBool 7 <Int Y andBool Y <=Int 15
+      [simplification]
+
+    rule byte ( X:Int >>Int Y:Int , cachedBytesConstant ) => 3
+         requires 0 <=Int X andBool 0 <=Int Y
+          andBool X <=Int ( 2 ^Int ( Y +Int 4 ) -Int 1 )
+          andBool 7 <Int X >>Int Y
+          [simplification, concrete(Y)]
+
+    rule byte ( X:Int >>Int Y:Int , cachedBytesConstant ) => 2
+         requires 0 <=Int X andBool 0 <=Int Y
+          andBool X <=Int ( 2 ^Int ( Y +Int 4 ) -Int 1 )
+          andBool notBool 7 <Int X >>Int Y
+          andBool 3 <Int X >>Int Y
+          [simplification, concrete(Y)]
+
+    rule byte ( X:Int >>Int Y:Int , cachedBytesConstant ) => 1
+         requires 0 <=Int X andBool 0 <=Int Y
+          andBool X <=Int ( 2 ^Int ( Y +Int 4 ) -Int 1 )
+          andBool notBool 3 <Int X >>Int Y
+          andBool 1 <Int X >>Int Y
+          [simplification, concrete(Y)]
+
+    rule byte ( X:Int >>Int Y:Int , cachedBytesConstant ) => 0
+         requires 0 <=Int X andBool 0 <=Int Y
+          andBool X <=Int ( 2 ^Int ( Y +Int 4 ) -Int 1 )
+          andBool notBool 1 <Int X >>Int Y
+          andBool 0 <Int X >>Int Y
+          [simplification, concrete(Y)]
+
 endmodule
 
 module SOLADY-LEMMAS-SPEC
     imports SOLADY-LEMMAS
 
-    claim [first-roadblock]: <k> runLemma(bool2Word( notBool ( notBool ( ( notBool X:Int ==Int 0 ) andBool maxUInt256 /Word X:Int <Int 0 ) ) )) => doneLemma(0) ...  </k>
-    claim [mulWad-first-roadblock]: <k> runLemma(bool2Word( notBool ( notBool ( ( notBool X:Int ==Int 0 ) andBool maxUInt256 /Word X:Int <Int 0 ) ) )) => doneLemma(0) ...  </k>
-      requires 0 <=Int X
+    //claim [log2-01]: <k> runLemma(chop (bool2Word ( X:Bool ) <<Int 7)) => doneLemma(128) ...  </k>
+    //  requires X:Bool
+
+    //claim [log2-02]: <k> runLemma(chop (bool2Word ( X:Bool ) <<Int 7)) => doneLemma(0) ...  </k>
+    //  requires notBool X:Bool
+
+    //claim [log2-03]: <k> runLemma(1 <<Word (bool2Word ( X:Bool ) <<Int 7)) => doneLemma(pow128) ...  </k>
+    //  requires X:Bool
+
+    //claim [log2-04]: <k> runLemma(bool2Word ( X:Bool ) <<Int 7) => doneLemma(128) ...  </k>
+    //  requires X:Bool
+
+    //claim [log2-05]: <k> runLemma( maxUInt8 <Int chop ( bool2Word ( _ ) <<Int 7) ) => doneLemma(false) ... </k>
+
+    //claim [log2-06]: <k> runLemma (maxUInt8 <Int ( bool2Word ( maxUInt64 <Int X:Int >>Int bool2Word ( maxUInt128 <Int X:Int ) <<Int 7 ) <<Int 6 |Int bool2Word ( maxUInt128 <Int X:Int ) <<Int 7 ) ) => doneLemma(false) ... </k>
+
+    // claim [log2-07]: <k> runLemma (1 <<Int ( bool2Word ( maxUInt64 <Int X:Int >>Int bool2Word ( maxUInt128 <Int X:Int ) <<Int 7 ) <<Int 6 |Int bool2Word ( maxUInt128 <Int X:Int ) <<Int 7 ) <=Int X:Int) => doneLemma(maxUInt128 <Int X:Int) ... </k>
+
+    claim [arith-01]:
+      <k>
+        runLemma (
+                  notBool ( maxUInt8 <=Int ( 4 |Int ( ( cachedBytesConstant >>Int ( ( maxUInt5 -Int ( VV0_x_114b9705:Int >>Int 4 ) ) *Int 8 ) ) modInt 256 ) ) )
+          andBool VV0_x_114b9705 >>Int 4 <Int 32
+        ) => doneLemma (
+          true
+        )
+      </k>
+      requires 0 <=Int VV0_x_114b9705:Int
+       andBool VV0_x_114b9705:Int >>Int 4 <=Int 1
+
+    claim [arith-02]:
+      <k>
+        runLemma ( maxUInt64 <Int VV0_x_114b9705:Int >>Int 128 ) => doneLemma ( false )
+      </k>
+      requires VV0_x_114b9705 <=Int maxUInt192
 
     claim [mulWadUp-second-roadblock]: <k> runLemma( notBool ( ( notBool X:Int ==Int 0 ) andBool maxUInt256 /Word X:Int <Int Y:Int ) ) => doneLemma(false) ... </k>
       requires ( notBool ( notBool ( ( notBool X:Int ==Int 0 ) andBool maxUInt256 /Word X:Int <Int Y:Int ) ) )