diff --git a/Makefile b/Makefile
index 2befb41e3a..6826796a64 100644
--- a/Makefile
+++ b/Makefile
@@ -59,7 +59,7 @@ test-prove-kprove: tests/specs/opcodes/evm-optimizations-spec.md poetry
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_kprove_prove"
 
 # to generate optimizations.md, run: ./optimizer/optimize.sh &> output
-tests/specs/opcodes/evm-optimizations-spec.md:
+tests/specs/opcodes/evm-optimizations-spec.md: kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
 	cat kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md | sed 's/^rule/claim/' | sed 's/EVM-OPTIMIZATIONS/EVM-OPTIMIZATIONS-SPEC/' | grep -v 'priority(40)' > $@
 
 
@@ -108,7 +108,7 @@ tests/specs/%.prove: tests/specs/% tests/specs/$$(firstword $$(subst /, ,$$*))/$
 		--definition tests/specs/$(firstword $(subst /, ,$*))/$(KPROVE_FILE)/$(TEST_SYMBOLIC_BACKEND)
 
 tests/specs/%/timestamp: tests/specs/$$(firstword $$(subst /, ,$$*))/$$(KPROVE_FILE).$$(KPROVE_EXT)
-	$(POETRY_RUN) kevm-pyk kompile                                                                             \
+	$(POETRY_RUN) kevm-pyk kompile-spec                                                                         \
 		$<                                                                                                      \
 		--target $(word 3, $(subst /, , $*))                                                                    \
 		--output-definition tests/specs/$(firstword $(subst /, ,$*))/$(KPROVE_FILE)/$(word 3, $(subst /, , $*)) \
diff --git a/README.md b/README.md
index 07767b7aaf..2e11d4b9b4 100644
--- a/README.md
+++ b/README.md
@@ -207,7 +207,7 @@ Finally, you can build the semantics.
 poetry -C kevm-pyk run kevm-dist --verbose build -j4
 ```
 
-You can build specific targets using options `evm-semantics.{llvm,haskell,haskell-standalone}`, e.g.:
+You can build specific targets using options `evm-semantics.{llvm,haskell,haskell-standalone,plugin}`, e.g.:
 
 ```sh
 poetry -C kevm-pyk run kevm-dist build -j2 evm-semantics.llvm evm-semantics.haskell
diff --git a/VERIFICATION.md b/VERIFICATION.md
index 60a913e82a..d3a3a35de9 100644
--- a/VERIFICATION.md
+++ b/VERIFICATION.md
@@ -18,13 +18,12 @@ It has two modules:
 The first step is kompiling the `.k` file with the below command.
 
 ```sh
-kevm kompile sum-to-n-spec.k --target haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition sum-to-n-spec/haskell
+kevm kompile-spec sum-to-n-spec.k --target haskell-booster --syntax-module VERIFICATION --main-module VERIFICATION --definition sum-to-n-spec/haskell
 ```
 
 In this example, the arguments used are:
 
-  - `—-pyk`: a flag that enables the pyk library.
-  - `—-backend haskell`: used to kompile the definition with the Haskell backend, enabling the symbolic execution ([more about it here]).
+  - `--target haskell-booster`: specify which symbolic backend to use for reasoning.
   - `--syntax-module VERIFICATION`: explicitly state the syntax module.
   - `--main-module VERIFICATION`: explicitly state the main module.
   - `--definition sum-to-n-spec/haskell`: the path where the kompiled definition is stored.
@@ -61,7 +60,7 @@ These rules are then used in the claims. As an example, the `#binRuntime(ERC20)`
 Following this, we can compile the Markdown file with:
 
 ```sh
-kevm kompile erc20-spec.md --target haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition erc20-spec/haskell
+kevm kompile-spec erc20-spec.md --syntax-module VERIFICATION --main-module VERIFICATION --definition erc20-spec/haskell
 ```
 
 Next, run the prover with:
@@ -101,7 +100,7 @@ A running example:
 
 ```sh
 mkdir kcfgs
-kevm kompile --target haskell tests/specs/benchmarks/verification.k --definition tests/specs/benchmarks/verification/haskell --main-module VERIFICATION --syntax-module VERIFICATION
+kevm kompile-spec tests/specs/benchmarks/verification.k --definition tests/specs/benchmarks/verification/haskell --main-module VERIFICATION --syntax-module VERIFICATION
 kevm prove tests/specs/benchmarks/address00-spec.k --definition tests/specs/benchmarks/verification/haskell --verbose --save-directory kcfgs
 kevm view-kcfg --verbose kcfgs tests/specs/benchmarks/address00-spec.k --definition tests/specs/benchmarks/verification/haskell
 ```
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
index 4e1ad329b6..0502c02fa9 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.357"
+version = "1.0.358"
 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 767e0c8fd5..7a63623948 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.357'
+VERSION: Final = '1.0.358'
diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
index ab324e4e97..028836f4d9 100644
--- a/kevm-pyk/src/kevm_pyk/__main__.py
+++ b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -87,7 +87,7 @@ def exec_version(**kwargs: Any) -> None:
     print(f'KEVM Version: {VERSION}')
 
 
-def exec_kompile(
+def exec_kompile_spec(
     output_dir: Path | None,
     main_file: Path,
     emit_json: bool,
@@ -109,7 +109,12 @@ def exec_kompile(
     **kwargs: Any,
 ) -> None:
     if target is None:
-        target = KompileTarget.LLVM
+        target = KompileTarget.HASKELL_BOOSTER
+
+    if target not in [KompileTarget.HASKELL, KompileTarget.HASKELL_BOOSTER, KompileTarget.MAUDE]:
+        raise ValueError(
+            f'Can only call kevm kompile-spec with --target [haskell,haskell-booster,maude], got: {target.value}'
+        )
 
     output_dir = output_dir or Path()
 
@@ -671,17 +676,17 @@ def parse(s: str) -> list[T]:
 
     command_parser.add_parser('version', help='Print KEVM version and exit.', parents=[kevm_cli_args.logging_args])
 
-    kevm_kompile_args = command_parser.add_parser(
-        'kompile',
+    kevm_kompile_spec_args = command_parser.add_parser(
+        'kompile-spec',
         help='Kompile KEVM specification.',
         parents=[kevm_cli_args.logging_args, kevm_cli_args.k_args, kevm_cli_args.kompile_args],
     )
-    kevm_kompile_args.add_argument('main_file', type=file_path, help='Path to file with main module.')
-    kevm_kompile_args.add_argument('--target', type=KompileTarget, help='[llvm|haskell|haskell-booster]')
-    kevm_kompile_args.add_argument(
+    kevm_kompile_spec_args.add_argument('main_file', type=file_path, help='Path to file with main module.')
+    kevm_kompile_spec_args.add_argument('--target', type=KompileTarget, help='[haskell|haskell-booster|maude]')
+    kevm_kompile_spec_args.add_argument(
         '-o', '--output-definition', type=Path, dest='output_dir', help='Path to write kompiled definition to.'
     )
-    kevm_kompile_args.add_argument(
+    kevm_kompile_spec_args.add_argument(
         '--debug-build', dest='debug_build', default=False, help='Enable debug symbols in LLVM builds.'
     )
 
diff --git a/kevm-pyk/src/kevm_pyk/kdist/plugin.py b/kevm-pyk/src/kevm_pyk/kdist/plugin.py
index 0f0f230006..15a62c6531 100644
--- a/kevm-pyk/src/kevm_pyk/kdist/plugin.py
+++ b/kevm-pyk/src/kevm_pyk/kdist/plugin.py
@@ -11,33 +11,34 @@
 from .api import Target
 
 if TYPE_CHECKING:
-    from collections.abc import Iterable, Mapping
+    from collections.abc import Mapping
     from pathlib import Path
     from typing import Any, Final
 
 
 class KEVMTarget(Target):
     _kompile_args: dict[str, Any]
-    _deps: tuple[str, ...]
 
-    def __init__(self, kompile_args: Mapping[str, Any], *, deps: Iterable[str] | None = None):
+    def __init__(self, kompile_args: Mapping[str, Any]):
         self._kompile_args = dict(kompile_args)
-        self._deps = tuple(deps) if deps is not None else ()
 
     def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any]) -> None:
         verbose = args.get('verbose', False)
         enable_llvm_debug = args.get('enable_llvm_debug', False)
+        debug_build = args.get('debug_build', False)
+        ccopts = args.get('ccopts', [])
 
         kevm_kompile(
             output_dir=output_dir,
             enable_llvm_debug=enable_llvm_debug,
             verbose=verbose,
-            plugin_dir=deps.get('evm-semantics.plugin'),
+            ccopts=ccopts,
+            debug_build=debug_build,
             **self._kompile_args,
         )
 
     def deps(self) -> tuple[str, ...]:
-        return self._deps
+        return ('evm-semantics.plugin',)
 
 
 class PluginTarget(Target):
@@ -76,7 +77,6 @@ def build(self, output_dir: Path, deps: dict[str, Any], args: dict[str, Any]) ->
             'syntax_module': 'ETHEREUM-SIMULATION',
             'optimization': 2,
         },
-        deps=('evm-semantics.plugin',),
     ),
     'haskell': KEVMTarget(
         {
diff --git a/kevm-pyk/src/kevm_pyk/kompile.py b/kevm-pyk/src/kevm_pyk/kompile.py
index d48c9622ef..c6810a88c3 100644
--- a/kevm-pyk/src/kevm_pyk/kompile.py
+++ b/kevm-pyk/src/kevm_pyk/kompile.py
@@ -10,7 +10,7 @@
 from pyk.ktool.kompile import HaskellKompile, KompileArgs, LLVMKompile, LLVMKompileType, MaudeKompile
 from pyk.utils import run_process
 
-from . import config
+from . import config, kdist
 
 if TYPE_CHECKING:
     from collections.abc import Iterable
@@ -45,8 +45,49 @@ def md_selector(self) -> str:
 def kevm_kompile(
     target: KompileTarget,
     output_dir: Path,
+    main_file: Path,
     *,
+    main_module: str | None,
+    syntax_module: str | None,
+    includes: Iterable[str] = (),
+    emit_json: bool = True,
+    read_only: bool = False,
+    ccopts: Iterable[str] = (),
+    optimization: int = 0,
+    llvm_kompile_type: LLVMKompileType | None = None,
+    enable_llvm_debug: bool = False,
+    llvm_library: Path | None = None,
+    debug_build: bool = False,
+    debug: bool = False,
+    verbose: bool = False,
+) -> Path:
+    plugin_dir = kdist.get('evm-semantics.plugin')
+    ccopts = list(ccopts) + _lib_ccopts(plugin_dir, debug_build=debug_build)
+    return run_kompile(
+        target,
+        output_dir,
+        main_file,
+        main_module=main_module,
+        syntax_module=syntax_module,
+        includes=includes,
+        emit_json=emit_json,
+        read_only=read_only,
+        ccopts=ccopts,
+        optimization=optimization,
+        llvm_kompile_type=llvm_kompile_type,
+        enable_llvm_debug=enable_llvm_debug,
+        llvm_library=llvm_library,
+        debug_build=debug_build,
+        debug=debug,
+        verbose=verbose,
+    )
+
+
+def run_kompile(
+    target: KompileTarget,
+    output_dir: Path,
     main_file: Path,
+    *,
     main_module: str | None,
     syntax_module: str | None,
     includes: Iterable[str] = (),
@@ -57,7 +98,6 @@ def kevm_kompile(
     llvm_kompile_type: LLVMKompileType | None = None,
     enable_llvm_debug: bool = False,
     llvm_library: Path | None = None,
-    plugin_dir: Path | None = None,
     debug_build: bool = False,
     debug: bool = False,
     verbose: bool = False,
@@ -65,9 +105,6 @@ def kevm_kompile(
     if llvm_library is None:
         llvm_library = output_dir / 'llvm-library'
 
-    if target in [KompileTarget.LLVM, KompileTarget.HASKELL_BOOSTER] and not plugin_dir:
-        raise ValueError(f'Parameter plugin_dir is required for target: {target.value}')
-
     include_dirs = [Path(include) for include in includes]
     include_dirs += config.INCLUDE_DIRS
 
@@ -89,8 +126,6 @@ def kevm_kompile(
     try:
         match target:
             case KompileTarget.LLVM:
-                assert plugin_dir
-                ccopts = list(ccopts) + _lib_ccopts(plugin_dir, kernel, debug_build=debug_build)
                 kompile = LLVMKompile(
                     base_args=base_args,
                     ccopts=ccopts,
@@ -129,9 +164,8 @@ def _kompile_haskell() -> None:
                     [future.result() for future in futures]
 
                 return output_dir
+
             case KompileTarget.HASKELL_BOOSTER:
-                assert plugin_dir
-                ccopts = list(ccopts) + _lib_ccopts(plugin_dir, kernel, debug_build=debug_build)
                 base_args_llvm = KompileArgs(
                     main_file=main_file,
                     main_module=main_module,
@@ -173,7 +207,9 @@ def _kompile_haskell() -> None:
         raise
 
 
-def _lib_ccopts(plugin_dir: Path, kernel: str, debug_build: bool = False) -> list[str]:
+def _lib_ccopts(plugin_dir: Path, debug_build: bool = False) -> list[str]:
+    kernel = sys.platform
+
     ccopts = ['-std=c++17']
 
     if debug_build:
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
index 4985f896a9..5c546e97d6 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
@@ -7,7 +7,7 @@ These optimizations work on the LLVM and Haskell backend and are generated by th
 requires "evm.md"
 requires "lemmas/int-simplification.k"
 
-module EVM-OPTIMIZATIONS-LEMMAS [kore, symbolic]
+module EVM-OPTIMIZATIONS-LEMMAS [kore]
     imports EVM
 
     rule #sizeWordStack(WS           , N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0                [simplification]
diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py
index 4b2e1bb147..ae75ceb671 100644
--- a/kevm-pyk/src/tests/integration/test_prove.py
+++ b/kevm-pyk/src/tests/integration/test_prove.py
@@ -9,7 +9,7 @@
 from pyk.cterm import CTerm
 from pyk.proof.reachability import APRProof
 
-from kevm_pyk import config, kdist
+from kevm_pyk import config
 from kevm_pyk.__main__ import exec_prove
 from kevm_pyk.kevm import KEVM
 from kevm_pyk.kompile import KompileTarget, kevm_kompile
@@ -117,7 +117,6 @@ class Target(NamedTuple):
     def __call__(self, output_dir: Path) -> Path:
         definition_subdir = 'kompiled' if not self.use_booster else 'kompiled-booster'
         definition_dir = output_dir / definition_subdir
-        plugin_dir = kdist.get('evm-semantics.plugin') if self.use_booster else None
         target = KompileTarget.HASKELL if not self.use_booster else KompileTarget.HASKELL_BOOSTER
         return kevm_kompile(
             output_dir=definition_dir,
@@ -125,8 +124,6 @@ def __call__(self, output_dir: Path) -> Path:
             main_file=self.main_file,
             main_module=self.main_module_name,
             syntax_module=self.main_module_name,
-            includes=[],
-            plugin_dir=plugin_dir,
             debug=True,
         )
 
diff --git a/package/test-package.sh b/package/test-package.sh
index 1fd34b7428..eedc0890e4 100755
--- a/package/test-package.sh
+++ b/package/test-package.sh
@@ -30,3 +30,16 @@ if ! ${APPLE_SILICON:-false}; then
         || git --no-pager diff --no-index --ignore-all-space -R tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.llvm-out tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected
     rm -rf tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.llvm-out
 fi
+
+kevm kompile-spec tests/specs/benchmarks/verification.k             \
+    --output-definition tests/specs/benchmarks/verification/haskell \
+    --main-module VERIFICATION                                      \
+    --syntax-module VERIFICATION                                    \
+    --target haskell-booster                                        \
+    --verbose
+
+kevm prove tests/specs/benchmarks/structarg00-spec.k         \
+    --definition tests/specs/benchmarks/verification/haskell \
+    --save-directory proofs                                  \
+    --verbose                                                \
+    --use-booster
diff --git a/package/version b/package/version
index 99d98ea697..7e7e90ec49 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-1.0.357
+1.0.358
diff --git a/tests/specs/examples/sum-to-n-foundry-spec.k b/tests/specs/examples/sum-to-n-foundry-spec.k
index 2ef42ef090..e1e7ba86cf 100644
--- a/tests/specs/examples/sum-to-n-foundry-spec.k
+++ b/tests/specs/examples/sum-to-n-foundry-spec.k
@@ -4,6 +4,7 @@ requires "gas.md"
 module VERIFICATION
     imports LEMMAS
     imports INFINITE-GAS
+    imports EVM
 
     rule N xorInt maxUInt256 => maxUInt256 -Int N
     requires #rangeUInt(256, N)
diff --git a/tests/specs/functional/infinite-gas-spec.k b/tests/specs/functional/infinite-gas-spec.k
index e424c2c4a7..4d4a4326c3 100644
--- a/tests/specs/functional/infinite-gas-spec.k
+++ b/tests/specs/functional/infinite-gas-spec.k
@@ -4,6 +4,7 @@ requires "lemmas/lemmas.k"
 module VERIFICATION
     imports INFINITE-GAS
     imports LEMMAS
+    imports EVM
 endmodule
 
 module INFINITE-GAS-SPEC