diff --git a/k-frontend/src/main/java/org/kframework/kompile/Kompile.java b/k-frontend/src/main/java/org/kframework/kompile/Kompile.java
index 7e225024f8e..06bd9b6fb15 100644
--- a/k-frontend/src/main/java/org/kframework/kompile/Kompile.java
+++ b/k-frontend/src/main/java/org/kframework/kompile/Kompile.java
@@ -539,7 +539,7 @@ public void definitionChecks(Set<Module> modules) {
   }
 
   // Extra checks just for the prover specification.
-  public void proverChecksX(Module specModule, Module mainDefModule) {
+  public void proverChecksX(Module specModule, Module mainDefModule, boolean allowRules) {
     // check rogue syntax in spec module
     Set<Sentence> toCheck = mutable(specModule.sentences().$minus$minus(mainDefModule.sentences()));
     for (Sentence s : toCheck)
@@ -558,7 +558,7 @@ public void proverChecksX(Module specModule, Module mainDefModule) {
               if (m.name().equals(mainDefModule.name())
                   || mainDefModule.importedModuleNames().contains(m.name())) return s;
               if (!(s instanceof Claim || s.isSyntax())) {
-                if (s instanceof Rule && !s.att().contains(Att.SIMPLIFICATION()))
+                if (s instanceof Rule && !allowRules && !s.att().contains(Att.SIMPLIFICATION()))
                   errors.add(
                       KEMException.compilerError(
                           "Only claims and simplification rules are allowed in proof modules.", s));
diff --git a/k-frontend/src/main/java/org/kframework/kprove/KProveOptions.java b/k-frontend/src/main/java/org/kframework/kprove/KProveOptions.java
index e6f6d8f8696..6a2ee9945d0 100644
--- a/k-frontend/src/main/java/org/kframework/kprove/KProveOptions.java
+++ b/k-frontend/src/main/java/org/kframework/kprove/KProveOptions.java
@@ -113,4 +113,10 @@ public synchronized File specFile(FileUtil files) {
       description = "Allow functional claims to be printed in kore format. Use with --dry-run.",
       hidden = true)
   public boolean allowFuncClaims = false;
+
+  @Parameter(
+      names = "--allow-rules",
+      description = "Allow new rules to be introduced in proof modules. Use with --dry-run.",
+      hidden = true)
+  public boolean allowRules = false;
 }
diff --git a/k-frontend/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java b/k-frontend/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java
index 17a1eca63bd..1535b3f534c 100644
--- a/k-frontend/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java
+++ b/k-frontend/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java
@@ -63,7 +63,8 @@ public Tuple2<Definition, Module> build(File specFile, String specModuleName) {
     Definition parsedDefinition = compiledDefinition.getParsedDefinition();
     Module specModule = getModule(specModuleNameUpdated, modulesMap, parsedDefinition);
     specModule = filter(specModule);
-    kompile.proverChecksX(specModule, modulesMap.get(defModuleNameUpdated));
+    kompile.proverChecksX(
+        specModule, modulesMap.get(defModuleNameUpdated), proveOptions.allowRules);
     kompile.structuralChecks(
         immutable(modules), specModule, Option.empty(), backend.excludedModuleTags());
     specModule =
diff --git a/pyk/src/pyk/ktool/kprove.py b/pyk/src/pyk/ktool/kprove.py
index a65a474dbc1..b5b9134a5dc 100644
--- a/pyk/src/pyk/ktool/kprove.py
+++ b/pyk/src/pyk/ktool/kprove.py
@@ -274,7 +274,7 @@ def parse_modules(
                 temp_dir=self.use_directory,
                 dry_run=True,
                 type_inference_mode=type_inference_mode,
-                args=['--emit-json-spec', ntf.name],
+                args=['--emit-json-spec', ntf.name, '--allow-rules'],
             )
             json_data = json.loads(Path(ntf.name).read_text())
 
diff --git a/pyk/src/tests/integration/test-data/k-files/looping-spec.k b/pyk/src/tests/integration/test-data/k-files/looping-spec.k
index 7dea593426b..1a190b9cded 100644
--- a/pyk/src/tests/integration/test-data/k-files/looping-spec.k
+++ b/pyk/src/tests/integration/test-data/k-files/looping-spec.k
@@ -3,6 +3,8 @@ requires "imp-verification.k"
 module LOOPING-SPEC
     imports IMP-VERIFICATION
 
+    rule [if-true-true]: <k> if (true && true)  S else _ => S ... </k> [priority(80)]
+
     claim <k> while ( 1 <= $n ) {
                 $s = $s + $n ;
                 $n = $n + -1 ;