diff --git a/pyk/src/pyk/ktool/krun.py b/pyk/src/pyk/ktool/krun.py
index ce2b1d54927..3f8340c04b4 100644
--- a/pyk/src/pyk/ktool/krun.py
+++ b/pyk/src/pyk/ktool/krun.py
@@ -2,8 +2,12 @@
 
 import logging
 from enum import Enum
+from os import execvp
 from pathlib import Path
-from subprocess import CalledProcessError
+from shlex import join, split
+from subprocess import PIPE, CalledProcessError, run
+from sys import stderr, stdout
+from time import time
 from typing import TYPE_CHECKING
 
 from ..cli.utils import check_dir_path, check_file_path
@@ -99,6 +103,104 @@ def run_process(
                 debugger=debugger,
             )
 
+    def run_proof_hint(
+        self,
+        pgm: Pattern,
+        *,
+        cmap: Mapping[str, str] | None = None,
+        pmap: Mapping[str, str] | None = None,
+        output: KRunOutput | None = None,
+        parser: str | None = None,
+        term: bool = False,
+        temp_dir: Path | None = None,
+        depth: int | None = None,
+        expand_macros: bool = True,
+        search_final: bool = False,
+        no_pattern: bool = False,
+        check: bool = False,
+        pipe_stderr: bool = True,
+        debugger: bool = False,
+        proof_hint: bool = False,
+    ) -> bytes:
+        with self._temp_file() as ntf:
+            pgm.write(ntf)
+            ntf.flush()
+
+        args = _build_arg_list(
+            command='krun',
+            input_file=Path(ntf.name),
+            definition_dir=self.definition_dir,
+            output=output,
+            parser=parser,
+            depth=depth,
+            pmap=pmap,
+            cmap=cmap,
+            term=term,
+            temp_dir=temp_dir,
+            no_expand_macros=not expand_macros,
+            search_final=search_final,
+            no_pattern=no_pattern,
+            debugger=debugger,
+            proof_hint=proof_hint,
+        )
+
+        hints_bytes = self.__run_proof_hint_process(
+            args=args, check=check, pipe_stderr=pipe_stderr, logger=_LOGGER, exec_process=debugger
+        )
+
+        return hints_bytes.stdout
+
+    def __run_proof_hint_process(
+        self,
+        args: str | Iterable[str],
+        *,
+        check: bool = True,
+        input: str | None = None,
+        pipe_stdout: bool = True,
+        pipe_stderr: bool = False,
+        cwd: str | Path | None = None,
+        logger: Logger | None = None,
+        exec_process: bool = False,
+    ) -> CompletedProcess:
+
+        if cwd is not None:
+            cwd = Path(cwd)
+            check_dir_path(cwd)
+
+        if type(args) is str:
+            command = args
+        else:
+            args = tuple(args)
+            command = join(args)
+
+        if not logger:
+            logger = _LOGGER
+
+        proc_stdout = PIPE if pipe_stdout else None
+        proc_stderr = PIPE if pipe_stderr else None
+
+        logger.info(f'Running: {command}')
+
+        if exec_process:
+            stdout.flush()
+            stderr.flush()
+            if type(args) is str:
+                args = split(args)
+            argslist = list(args)
+            execvp(argslist[0], argslist)
+
+        start_time = time()
+
+        res = run(args, input=input, cwd=cwd, stdout=proc_stdout, stderr=proc_stderr, text=False)
+
+        delta_time = time() - start_time
+        logger.info(f'Completed in {delta_time:.3f}s with status {res.returncode}: {command}')
+
+        if check:
+            res.check_returncode()
+
+        return res
+
     def run(
         self,
         pgm: Pattern,
@@ -236,6 +338,7 @@ def _krun(
         search_final=search_final,
         no_pattern=no_pattern,
         debugger=debugger,
+        proof_hint=False,
     )
 
     if bug_report is not None:
@@ -265,6 +368,7 @@ def _build_arg_list(
     search_final: bool,
     no_pattern: bool,
     debugger: bool,
+    proof_hint: bool,
 ) -> list[str]:
     args = [command]
     if input_file:
@@ -293,6 +397,8 @@ def _build_arg_list(
         args += ['--no-pattern']
     if debugger:
         args += ['--debugger']
+    if proof_hint:
+        args += ['--proof-hint']
     return args
 
 
diff --git a/pyk/src/tests/integration/test_krun_proof_hints.py b/pyk/src/tests/integration/test_krun_proof_hints.py
new file mode 100644
index 00000000000..5059673199e
--- /dev/null
+++ b/pyk/src/tests/integration/test_krun_proof_hints.py
@@ -0,0 +1,87 @@
+from __future__ import annotations
+
+from typing import TYPE_CHECKING
+
+import pyk.kllvm.hints.prooftrace as prooftrace
+from pyk.kore.parser import KoreParser
+from pyk.testing import KRunTest, ProofTraceTest
+
+if TYPE_CHECKING:
+    from pyk.ktool.krun import KRun
+
+
+class Test0Decrement(KRunTest, ProofTraceTest):
+    KOMPILE_DEFINITION = """
+        module DECREMENT-SYNTAX
+            syntax Nat ::= "0" | s(Nat)
+        endmodule
+
+        module DECREMENT
+            imports DECREMENT-SYNTAX
+            rule [decrement] : s(N:Nat) => N
+        endmodule
+    """
+
+    KOMPILE_MAIN_MODULE = 'DECREMENT'
+    KOMPILE_BACKEND = 'llvm'
+    KOMPILE_ARGS = {'llvm_proof_hint_instrumentation': True}
+
+    HINTS_INPUT_KORE = """
+        LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\\dv{SortKConfigVar{}}("$PGM")),inj{SortNat{}, SortKItem{}}(Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()))))
+    """
+
+    HINTS_OUTPUT = """version: 11
+hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
+  function: Lbl'UndsPipe'-'-GT-Unds'{} ()
+  arg: kore[\\dv{SortKConfigVar{}}("$PGM")]
+  arg: kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()]
+hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
+hook: MAP.unit Lbl'Stop'Map{} ()
+  function: Lbl'Stop'Map{} ()
+hook result: kore[Lbl'Stop'Map{}()]
+hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
+  function: Lbl'Unds'Map'Unds'{} ()
+  arg: kore[Lbl'Stop'Map{}()]
+  arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
+hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
+function: LblinitGeneratedTopCell{} ()
+rule: 99 1
+  VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
+function: LblinitKCell{} (0)
+rule: 100 1
+  VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
+function: Lblproject'Coln'KItem{} (0:0)
+  hook: MAP.lookup LblMap'Coln'lookup{} (0:0:0:0)
+    function: LblMap'Coln'lookup{} (0:0:0:0)
+    arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
+    arg: kore[\\dv{SortKConfigVar{}}("$PGM")]
+  hook result: kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()]
+rule: 139 1
+  VarK = kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()]
+function: LblinitGeneratedCounterCell{} (1)
+rule: 98 0
+config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}(),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\\dv{SortInt{}}("0")))]
+config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}(),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\\dv{SortInt{}}("0")))]
+"""
+
+    def test_parse_proof_hint_0_decrement(self, krun: KRun, header: prooftrace.KoreHeader) -> None:
+        pgm = KoreParser(self.HINTS_INPUT_KORE).pattern()
+
+        hints = krun.run_proof_hint(
+            pgm,
+            parser='cat',
+            term=True,
+            proof_hint=True,
+        )
+
+        pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
+        assert pt is not None
+
+        # 11 initialization events
+        assert len(pt.pre_trace) == 11
+
+        # 1 post-initial-configuration event
+        assert len(pt.trace) == 1
+
+        # Check if the proof trace is correct
+        assert str(pt) == self.HINTS_OUTPUT
diff --git a/pyk/src/tests/unit/ktool/test_krun.py b/pyk/src/tests/unit/ktool/test_krun.py
index 8fa6d18b0a2..69ff022e7f2 100644
--- a/pyk/src/tests/unit/ktool/test_krun.py
+++ b/pyk/src/tests/unit/ktool/test_krun.py
@@ -23,6 +23,7 @@
         ('search_final', False),
         ('no_pattern', False),
         ('debugger', False),
+        ('proof_hint', False),
     ]
 )
 
@@ -40,6 +41,7 @@
     'search_final': (True, ['--search-final']),
     'no_pattern': (True, ['--no-pattern']),
     'debugger': (True, ['--debugger']),
+    'proof_hint': (True, ['--proof-hint']),
 }