diff --git a/examples/specs/imp-sum-spec.k b/examples/specs/imp-sum-spec.k
index 389005b..4c44ac2 100644
--- a/examples/specs/imp-sum-spec.k
+++ b/examples/specs/imp-sum-spec.k
@@ -42,4 +42,4 @@ module IMP-SUM-SPEC
   requires N >=Int 0
    andBool M >=Int 0
 
-endmodule
\ No newline at end of file
+endmodule
diff --git a/kimp/src/kimp/__main__.py b/kimp/src/kimp/__main__.py
index c43b598..9b83b36 100644
--- a/kimp/src/kimp/__main__.py
+++ b/kimp/src/kimp/__main__.py
@@ -4,14 +4,11 @@
 import os
 from argparse import ArgumentParser
 from pathlib import Path
-from tempfile import NamedTemporaryFile
 from typing import TYPE_CHECKING, Any, Final
 
 from pyk.cli.utils import dir_path, file_path
-from pyk.ktool.kprint import KAstOutput
-from pyk.ktool.krun import KRunOutput
 
-from .kimp import KIMP
+from .kimp import KImp
 
 if TYPE_CHECKING:
     from argparse import Namespace
@@ -66,37 +63,19 @@ def main() -> None:
 
 
 def exec_run(
-    input_file: str,
-    definition_dir: str,
-    input_term: str | None = None,
-    output: str = 'none',
-    ignore_return_code: bool = False,
+    input_file: Path,
+    env_list: list[list[tuple[str, int]]] | None,
+    definition_dir: Path | None,
     depth: int | None = None,
     **kwargs: Any,
 ) -> None:
-    krun_output = KRunOutput[output.upper()]
-
-    definition_dir_path = find_target('llvm') if definition_dir is None else Path(definition_dir)
-    kimp = KIMP(definition_dir_path, definition_dir_path)
-
-    try:
-        with NamedTemporaryFile(mode='w') as f:
-            temp_file = Path(f.name)
-            if input_term is not None:
-                temp_file.write_text(input_term)
-            else:
-                temp_file.write_text(Path(input_file).read_text())
-            proc_res = kimp.run_program(temp_file, output=krun_output, depth=depth)
-            if output != KAstOutput.NONE:
-                print(proc_res.stdout)
-    except RuntimeError as err:
-        if ignore_return_code:
-            msg, stdout, stderr = err.args
-            print(stdout)
-            print(stderr)
-            print(msg)
-        else:
-            raise
+    definition_dir = find_target('llvm') if definition_dir is None else definition_dir
+    kimp = KImp(definition_dir, definition_dir)
+    pgm = input_file.read_text()
+    env = {var: val for assign in env_list for var, val in assign} if env_list else {}
+    pattern = kimp.pattern(pgm=pgm, env=env)
+    output = kimp.run(pattern, depth=depth)
+    print(kimp.pretty(output, color=True))
 
 
 def exec_prove(
@@ -114,7 +93,7 @@ def exec_prove(
         definition_dir = str(find_target('haskell'))
     k_src_dir = str(find_target('source') / 'imp-semantics')
 
-    kimp = KIMP(definition_dir, definition_dir)
+    kimp = KImp(definition_dir, definition_dir)
 
     try:
         kimp.prove(
@@ -128,7 +107,6 @@ def exec_prove(
         )
     except ValueError as err:
         _LOGGER.critical(err.args)
-        # exit(1)
         raise
     except RuntimeError as err:
         if ignore_return_code:
@@ -147,7 +125,7 @@ def exec_show(
     **kwargs: Any,
 ) -> None:
     definition_dir = str(find_target('haskell'))
-    kimp = KIMP(definition_dir, definition_dir)
+    kimp = KImp(definition_dir, definition_dir)
     kimp.show_kcfg(spec_module, claim_id)
 
 
@@ -158,7 +136,7 @@ def exec_view(
     **kwargs: Any,
 ) -> None:
     definition_dir = str(find_target('haskell'))
-    kimp = KIMP(definition_dir, definition_dir)
+    kimp = KImp(definition_dir, definition_dir)
     kimp.view_kcfg(spec_module, claim_id)
 
 
@@ -170,7 +148,6 @@ def create_argument_parser() -> ArgumentParser:
     shared_args.add_argument(
         '--definition',
         dest='definition_dir',
-        nargs='?',
         type=dir_path,
         help='Path to compiled K definition to use.',
     )
@@ -198,61 +175,41 @@ def create_argument_parser() -> ArgumentParser:
     explore_args = ArgumentParser(add_help=False)
     explore_args.add_argument(
         '--reinit',
-        dest='reinit',
         default=False,
         action='store_true',
         help='Reinitialize proof even if it already exists.',
     )
     explore_args.add_argument(
         '--max-depth',
-        dest='max_depth',
         default=100,
         type=int,
         help='Max depth of execution',
     )
     explore_args.add_argument(
         '--max-iterations',
-        dest='max_iterations',
         default=1000,
         type=int,
         help='Store every Nth state in the CFG for inspection.',
     )
 
-    parser = ArgumentParser(prog='kimp', description='KIMP command line tool')
+    parser = ArgumentParser(prog='kimp', description='KImp command line tool')
     command_parser = parser.add_subparsers(dest='command', required=True, help='Command to execute')
 
     # Run
+    def env(s: str) -> list[tuple[str, int]]:
+        return [(var.strip(), int(val)) for var, val in (assign.split('=') for assign in s.split(','))]
+
     run_subparser = command_parser.add_parser('run', help='Run an IMP program', parents=[shared_args])
-    input_group = run_subparser.add_mutually_exclusive_group(required=True)
-    input_group.add_argument(
-        '--input-file',
-        type=file_path,
-        help='Path to .imp file',
-    )
-    input_group.add_argument(
-        '--input-term',
-        dest='input_term',
-        type=str,
-        help='Program to run, as a literal string',
-    )
+    run_subparser.add_argument('input_file', metavar='INPUT_FILE', type=file_path, help='Path to .imp file')
     run_subparser.add_argument(
-        '--output',
-        dest='output',
-        type=str,
-        default='pretty',
-        help='Output mode',
-        choices=['pretty', 'program', 'json', 'kore', 'kast', 'none'],
-        required=False,
-    )
-    run_subparser.add_argument(
-        '--ignore-return-code',
-        action='store_true',
-        default=False,
-        help='Ignore return code of krun, alwasys return 0 (use for debugging only)',
+        '--env',
+        dest='env_list',
+        action='append',
+        type=env,
+        help='Assigments of initial values in form x=0,y=1,...',
     )
     run_subparser.add_argument(
         '--depth',
-        dest='depth',
         type=int,
         help='Execute at most DEPTH rewrite steps',
     )
diff --git a/kimp/src/kimp/kdist/imp-semantics/statements.k b/kimp/src/kimp/kdist/imp-semantics/statements.k
index f498362..529c94b 100644
--- a/kimp/src/kimp/kdist/imp-semantics/statements.k
+++ b/kimp/src/kimp/kdist/imp-semantics/statements.k
@@ -19,17 +19,18 @@ endmodule
 module STATEMENTS-RULES
   imports STATEMENTS-SYNTAX
 
-  rule if ( true  ) E1 else _  => E1
-  rule if ( false ) _  else E2 => E2
+  rule [if-true]:  if ( true  ) E1 else _  => E1
+  rule [if-false]: if ( false ) _  else E2 => E2
 
-  rule if ( C ) E => if ( C ) E else {}
+  rule [if-else]: if ( C ) E => if ( C ) E else {}
 
   rule [while]:
     while ( C ) E
-    => if ( C ) {
-        E
-        while ( C ) E
-       }
+    =>
+    if ( C ) {
+      E
+      while ( C ) E
+    }
 
   rule [block]: { E } => E ~> {}
 
@@ -40,22 +41,21 @@ module STATEMENTS-RULES
 endmodule
 
 module STATEMENTS
-
   imports EXPRESSIONS
   imports VARIABLES-SYNTAX
   imports STATEMENTS-RULES
 
   configuration
-    <k> $PGM:Stmt </k>   // changed!
-    <env> .Map    </env>
+    <k   color="green">  $PGM:Stmt </k>   // changed!
+    <env color="yellow"> $ENV:Map  </env>
 
   // changed configuration, need to repeat the variable rule
-  rule
+  rule [var]:
     <k> X:Id => V ...</k>
     <env> X |-> V ...</env>
 
   // assignment rule accesses configuration
-  rule
+  rule [assign]:
     <k> X = V:Value ; => .K ...</k>
     <env> E => E [ X <- V ] </env>
 endmodule
diff --git a/kimp/src/kimp/kimp.py b/kimp/src/kimp/kimp.py
index 4109305..460643d 100644
--- a/kimp/src/kimp/kimp.py
+++ b/kimp/src/kimp/kimp.py
@@ -2,17 +2,16 @@
 
 from pyk.kcfg.show import NodePrinter
 
-__all__ = ['KIMP']
+__all__ = ['KImp']
 
 import logging
 from contextlib import contextmanager
 from dataclasses import dataclass
 from functools import cached_property
 from pathlib import Path
-from tempfile import NamedTemporaryFile
 from typing import TYPE_CHECKING, final
 
-from pyk.cli.utils import check_dir_path, check_file_path
+from pyk.cli.utils import check_dir_path
 from pyk.cterm.symbolic import CTermSymbolic
 from pyk.kast.formatter import Formatter
 from pyk.kast.inner import KApply, KLabel, KSequence, KVariable
@@ -23,21 +22,20 @@
 from pyk.kore.rpc import KoreClient, kore_server
 from pyk.ktool.claim_loader import ClaimLoader
 from pyk.ktool.kprove import KProve
-from pyk.ktool.krun import KRun, KRunOutput, _krun
 from pyk.proof.reachability import APRProof, APRProver
 from pyk.proof.show import APRProofShow
 from pyk.proof.tui import APRProofViewer
 from pyk.utils import single
 
 if TYPE_CHECKING:
-    from collections.abc import Iterable, Iterator
-    from subprocess import CompletedProcess
+    from collections.abc import Iterable, Iterator, Mapping
     from typing import Final
 
     from pyk.cterm.cterm import CTerm
     from pyk.kast.outer import KDefinition
     from pyk.kcfg.kcfg import KCFG, KCFGExtendResult
     from pyk.kore.rpc import FallbackReason
+    from pyk.kore.syntax import Pattern
     from pyk.ktool.kprint import KPrint
     from pyk.utils import BugReport
 
@@ -87,7 +85,7 @@ def is_mergeable(self, c1: CTerm, c2: CTerm) -> bool:
 
 @final
 @dataclass(frozen=True)
-class KIMP:
+class KImp:
     llvm_dir: Path
     haskell_dir: Path
     proof_dir: Path
@@ -106,10 +104,6 @@ def __init__(self, llvm_dir: str | Path, haskell_dir: str | Path):
         object.__setattr__(self, 'haskell_dir', haskell_dir)
         object.__setattr__(self, 'proof_dir', proof_dir)
 
-    @cached_property
-    def parser(self) -> Path:
-        return self.llvm_dir / 'parser_PGM'
-
     @cached_property
     def definition(self) -> KDefinition:
         return read_kast_definition(self.llvm_dir / 'compiled.json')
@@ -122,45 +116,51 @@ def format(self) -> Formatter:
     def kprove(self) -> KProve:
         return KProve(definition_dir=self.haskell_dir, use_directory=self.proof_dir)
 
-    @cached_property
-    def krun(self) -> KRun:
-        krun = KRun(definition_dir=self.llvm_dir)
-        return krun
-
-    def run_program(
+    def run(
         self,
-        program_file: str | Path,
+        pattern: Pattern,
         *,
-        output: KRunOutput = KRunOutput.NONE,
-        check: bool = True,
-        temp_file: str | Path | None = None,
-        depth: int | None,
-    ) -> CompletedProcess:
-        def run(program_file: Path) -> CompletedProcess:
-            return _krun(
-                input_file=program_file,
-                definition_dir=self.llvm_dir,
-                output=output,
-                check=check,
-                depth=depth,
-                pipe_stderr=True,
-                pmap={'PGM': str(self.parser)},
+        depth: int | None = None,
+    ) -> Pattern:
+        from pyk.ktool.krun import llvm_interpret
+
+        return llvm_interpret(definition_dir=self.llvm_dir, pattern=pattern, depth=depth)
+
+    def pattern(self, *, pgm: str, env: Mapping[str, int]) -> Pattern:
+        from pyk.kore.prelude import ID, INT, SORT_K_ITEM, inj, map_pattern, top_cell_initializer
+        from pyk.kore.syntax import DV, SortApp, String
+
+        pgm_pattern = self.parse(pgm)
+        env_pattern = map_pattern(
+            *(
+                (
+                    inj(ID, SORT_K_ITEM, DV(ID, String(var))),
+                    inj(INT, SORT_K_ITEM, DV(INT, String(str(val)))),
+                )
+                for var, val in env.items()
             )
+        )
+        return top_cell_initializer(
+            {
+                '$PGM': inj(SortApp('SortStmt'), SORT_K_ITEM, pgm_pattern),
+                '$ENV': inj(SortApp('SortMap'), SORT_K_ITEM, env_pattern),
+            }
+        )
+
+    def parse(self, pgm: str) -> Pattern:
+        from pyk.kore.parser import KoreParser
+        from pyk.utils import run_process_2
 
-        def preprocess_and_run(program_file: Path, temp_file: Path) -> CompletedProcess:
-            temp_file.write_text(program_file.read_text())
-            return run(temp_file)
+        parser = self.llvm_dir / 'parser_PGM'
+        args = [str(parser), '/dev/stdin']
 
-        program_file = Path(program_file)
-        check_file_path(program_file)
+        kore_text = run_process_2(args, input=pgm).stdout
+        return KoreParser(kore_text).pattern()
 
-        if temp_file is None:
-            with NamedTemporaryFile(mode='w') as f:
-                temp_file = Path(f.name)
-                return preprocess_and_run(program_file, temp_file)
+    def pretty(self, pattern: Pattern, color: bool | None = None) -> str:
+        from pyk.kore.tools import kore_print
 
-        temp_file = Path(temp_file)
-        return preprocess_and_run(program_file, temp_file)
+        return kore_print(pattern, definition_dir=self.llvm_dir, color=bool(color))
 
     def prove(
         self,
@@ -222,7 +222,7 @@ def view_kcfg(
         claim_id: str,
     ) -> None:
         proof = APRProof.read_proof_data(proof_dir=self.proof_dir, id=f'{spec_module}.{claim_id}')
-        kcfg_viewer = APRProofViewer(proof, self.kprove, node_printer=KIMPNodePrinter(kimp=self))
+        kcfg_viewer = APRProofViewer(proof, self.kprove, node_printer=ImpNodePrinter(kimp=self))
         kcfg_viewer.run()
 
     def show_kcfg(
@@ -231,7 +231,7 @@ def show_kcfg(
         claim_id: str,
     ) -> None:
         proof = APRProof.read_proof_data(proof_dir=self.proof_dir, id=f'{spec_module}.{claim_id}')
-        proof_show = APRProofShow(self.kprove, node_printer=KIMPNodePrinter(kimp=self))
+        proof_show = APRProofShow(self.kprove, node_printer=ImpNodePrinter(kimp=self))
         res_lines = proof_show.show(
             proof,
         )
@@ -303,10 +303,10 @@ def legacy_explore(
             )
 
 
-class KIMPNodePrinter(NodePrinter):
-    kimp: KIMP
+class ImpNodePrinter(NodePrinter):
+    kimp: KImp
 
-    def __init__(self, kimp: KIMP):
+    def __init__(self, kimp: KImp):
         NodePrinter.__init__(self, kimp.kprove)
         self.kimp = kimp
 
diff --git a/package/smoke-test.sh b/package/smoke-test.sh
index 6be4246..69a4ca1 100755
--- a/package/smoke-test.sh
+++ b/package/smoke-test.sh
@@ -4,7 +4,7 @@ set -euxo pipefail
 
 kimp --help
 
-kimp run --verbose --input-file examples/sumto10.imp
+kimp run --verbose examples/sumto10.imp --env 'x=0,y=1' --env z=2
 
 kimp prove --verbose examples/specs/imp-sum-spec.k IMP-SUM-SPEC sum-spec