diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 78b43dad372..4d8559f9875 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -184,6 +184,15 @@ void SetDefaults::setDefaultsPre(Options& opts)
                      options::UnsatCoresMode::SAT_PROOF,
                      "enabling proofs");
     }
+    if (opts.proof.proofFormatMode == options::ProofFormatMode::ALETHE
+        && opts.proof.proofGranularityMode
+               < options::ProofGranularityMode::THEORY_REWRITE)
+    {
+      SET_AND_NOTIFY(Proof,
+                     proofGranularityMode,
+                     options::ProofGranularityMode::THEORY_REWRITE,
+                     "Alethe requires granularity at least theory-rewrite");
+    }
   }
   if (!opts.smt.produceProofs)
   {