diff --git a/k-distribution/tests/regression-new/proof-instrumentation/.gitignore b/k-distribution/tests/regression-new/proof-instrumentation/.gitignore
new file mode 100644
index 00000000000..c75c8d9c4ad
--- /dev/null
+++ b/k-distribution/tests/regression-new/proof-instrumentation/.gitignore
@@ -0,0 +1 @@
+out.hint
diff --git a/k-distribution/tests/regression-new/proof-instrumentation/Makefile b/k-distribution/tests/regression-new/proof-instrumentation/Makefile
new file mode 100644
index 00000000000..ea956049d40
--- /dev/null
+++ b/k-distribution/tests/regression-new/proof-instrumentation/Makefile
@@ -0,0 +1,22 @@
+DEF=test
+KOMPILE_BACKEND=llvm
+KOMPILE_FLAGS+=--gen-glr-bison-parser --llvm-proof-hint-instrumentation
+LLVM_KRUN_FLAGS=-d ./test-kompiled --proof-hints
+
+check: out.hint
+	head -c4 out.hint | diff - <(echo -n 'HINT')
+
+out.hint: test.kore
+	rm -f $@
+	$(LLVM_KRUN) $(LLVM_KRUN_FLAGS) \
+		-c PGM $< Foo korefile -o $@
+
+test.kore: test.in kompile
+	./test-kompiled/parser_PGM $< > $@
+
+include ../../../include/kframework/ktest.mak
+
+clean:
+	rm -rf out.hint test.kore $(KOMPILED_DIR) .depend-tmp .depend .kompile-* .krun-* .kprove-* kore-exec.tar.gz
+
+update-results: CHECK=> test.out
diff --git a/k-distribution/tests/regression-new/proof-instrumentation/test.in b/k-distribution/tests/regression-new/proof-instrumentation/test.in
new file mode 100644
index 00000000000..eb28ef4401b
--- /dev/null
+++ b/k-distribution/tests/regression-new/proof-instrumentation/test.in
@@ -0,0 +1 @@
+foo()
diff --git a/k-distribution/tests/regression-new/proof-instrumentation/test.k b/k-distribution/tests/regression-new/proof-instrumentation/test.k
new file mode 100644
index 00000000000..d1ceb04f3d2
--- /dev/null
+++ b/k-distribution/tests/regression-new/proof-instrumentation/test.k
@@ -0,0 +1,9 @@
+// Copyright (c) K Team. All Rights Reserved.
+module TEST-SYNTAX
+  syntax Foo ::= foo() | bar()
+endmodule
+
+module TEST
+  imports TEST-SYNTAX
+  rule foo() => bar()
+endmodule
diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java
index 3d0ad8fa45f..d2dae356c3a 100644
--- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java
+++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java
@@ -124,6 +124,10 @@ private void llvmKompile(String type, String executable) {
       args.add(files.resolveKompiled("dt").getCanonicalPath());
       args.add(type);
 
+      if (options.enableProofHints) {
+        args.add("--proof-hint-instrumentation");
+      }
+
       // Arguments after this point are passed on to Clang.
       args.add("--");
 
diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java
index 5a1ea131b5a..9a7732d2572 100644
--- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java
+++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java
@@ -100,4 +100,10 @@ public List<String> convert(String str) {
       descriptionKey = "file",
       hidden = true)
   public String llvmKompileOutput = null;
+
+  @Parameter(
+      names = "--llvm-proof-hint-instrumentation",
+      description = "Emit proof hint instrumentation code into the generated interpreter",
+      hidden = true)
+  public boolean enableProofHints;
 }