diff --git a/crucible-debug/src/Lang/Crucible/Debug.hs b/crucible-debug/src/Lang/Crucible/Debug.hs
index 0890404a2..ad4722c97 100644
--- a/crucible-debug/src/Lang/Crucible/Debug.hs
+++ b/crucible-debug/src/Lang/Crucible/Debug.hs
@@ -51,6 +51,7 @@ module Lang.Crucible.Debug
   , Trace.Trace
   , Trace.TraceEntry(..)
   , Trace.latest
+  , IntrinsicPrinters(..)
   ) where
 
 import Control.Applicative qualified as Applicative
@@ -90,7 +91,7 @@ import Lang.Crucible.Debug.Style qualified as Style
 import Lang.Crucible.Debug.Style (StyleT)
 import Lang.Crucible.Debug.Trace qualified as Trace
 import Lang.Crucible.FunctionHandle qualified as C
-import Lang.Crucible.Pretty (IntrinsicPrinters (..))
+import Lang.Crucible.Pretty (IntrinsicPrinters(..))
 import Lang.Crucible.Simulator.CallFrame qualified as C
 import Lang.Crucible.Simulator.EvalStmt qualified as C
 import Lang.Crucible.Simulator.ExecutionTree qualified as C
diff --git a/crux-llvm/CHANGELOG.md b/crux-llvm/CHANGELOG.md
index 3995101c1..3c7900200 100644
--- a/crux-llvm/CHANGELOG.md
+++ b/crux-llvm/CHANGELOG.md
@@ -1,6 +1,7 @@
 # next -- TBA
 
 * Add support for the Bitwuzla SMT solver in the test suite.
+* Add `--debug` option for starting the Crucible debugger.
 
 # 0.9 -- 2024-08-30
 
diff --git a/crux-llvm/README.md b/crux-llvm/README.md
index 55ec50291..3dd05c5b3 100644
--- a/crux-llvm/README.md
+++ b/crux-llvm/README.md
@@ -406,6 +406,8 @@ In addition, the following flags can optionally be provided:
   a symbolic filesystem to use during symbolic execution.  See the Symbolic I/O
   documentation for the format of this directory. [Experimental]
 
+* `--debug`: Start the Crucible debugger.
+
 # Environment Variables
 
 The following environment variables are supported:
diff --git a/crux-mir/CHANGELOG.md b/crux-mir/CHANGELOG.md
index cdd42715b..0f6cbc6fb 100644
--- a/crux-mir/CHANGELOG.md
+++ b/crux-mir/CHANGELOG.md
@@ -1,3 +1,7 @@
+# next -- TBA
+
+* Add `--debug` option for starting the Crucible debugger.
+
 # 0.9 -- 2024-08-30
 
 * Add support for GHC 9.8
diff --git a/crux/CHANGELOG.md b/crux/CHANGELOG.md
index e13c0f353..ab55f6ff1 100644
--- a/crux/CHANGELOG.md
+++ b/crux/CHANGELOG.md
@@ -1,6 +1,9 @@
 # next -- TBA
 
 * Add support for the Bitwuzla SMT solver.
+* Add `--debug` option for starting the Crucible debugger.
+* For the sake of the `--debug` flag, Crux now depends on the
+  `crucible-{debug,syntax}` packages.
 
 # 0.7.1 -- 2024-08-30
 
diff --git a/crux/crux.cabal b/crux/crux.cabal
index fc4b28f5c..2eb767199 100644
--- a/crux/crux.cabal
+++ b/crux/crux.cabal
@@ -34,6 +34,8 @@ library
     containers,
     contravariant >= 1.5 && < 1.6,
     crucible,
+    crucible-debug,
+    crucible-syntax,
     directory,
     filepath,
     generic-lens,
diff --git a/crux/src/Crux.hs b/crux/src/Crux.hs
index da722c634..fd6c26a08 100644
--- a/crux/src/Crux.hs
+++ b/crux/src/Crux.hs
@@ -28,6 +28,7 @@ module Crux
   , module Crux.Log
   ) where
 
+import qualified Control.Applicative as Applicative
 import qualified Control.Exception as Ex
 import           Control.Lens
 import           Control.Monad ( unless, void, when )
@@ -53,6 +54,7 @@ import           System.FilePath ((</>))
 import           System.IO ( Handle, hPutStr, stdout, stderr )
 
 import           Data.Parameterized.Classes
+import qualified Data.Parameterized.Map as MapF
 import           Data.Parameterized.Nonce (newIONonceGenerator, NonceGenerator)
 import           Data.Parameterized.Some ( Some(..) )
 
@@ -60,6 +62,7 @@ import           Lang.Crucible.Backend
 import           Lang.Crucible.Backend.Online
 import qualified Lang.Crucible.Backend.Simple as CBS
 import           Lang.Crucible.CFG.Extension
+import qualified Lang.Crucible.Debug as Debug
 import           Lang.Crucible.Simulator
 import           Lang.Crucible.Simulator.BoundedExec
 import           Lang.Crucible.Simulator.BoundedRecursion
@@ -67,6 +70,7 @@ import           Lang.Crucible.Simulator.PathSatisfiability
 import           Lang.Crucible.Simulator.PathSplitting
 import           Lang.Crucible.Simulator.PositionTracking
 import           Lang.Crucible.Simulator.Profiling
+import qualified Lang.Crucible.Syntax.Concrete as Syn
 import           Lang.Crucible.Types
 
 
@@ -675,14 +679,38 @@ doSimWithResults cruxOpts simCallback bak execFeatures profInfo monline goalProv
     RunnableStateWithExtensions initSt exts <- setup bak monline
     explainFailure <- onError bak
 
+    -- This can't be initialized with the rest of the execution features,
+    -- because it is not a 'GenericExecutionFeature'.
+    --
+    -- Ideally, we would use language-extension-specific command extensions
+    -- (e.g., LLVM commands for Crux-LLVM) and parser hooks, but that would
+    -- require some refactoring to pass those in...
+    let debugging = debug cruxOpts
+    debugger <-
+      if debugging
+      then do
+        let ?parserHooks = Syn.ParserHooks Applicative.empty Applicative.empty
+        let cExts = Debug.voidExts
+        inps <- Debug.defaultDebuggerInputs cExts
+        dbg <-
+          Debug.debugger
+            cExts
+            Debug.voidImpl
+            (Debug.IntrinsicPrinters MapF.empty)
+            inps
+            Debug.defaultDebuggerOutputs
+            UnitRepr
+        pure [dbg]
+      else pure []
+
     -- execute the simulator
     case pathStrategy cruxOpts of
       AlwaysMergePaths ->
-        do res <- executeCrucible (map genericToExecutionFeature execFeatures ++ exts) initSt
+        do res <- executeCrucible (map genericToExecutionFeature execFeatures ++ exts ++ debugger) initSt
            void $ resultCont compRef glsRef frm explainFailure (Result res)
       SplitAndExploreDepthFirst ->
         do (i,ws) <- executeCrucibleDFSPaths
-                         (map genericToExecutionFeature execFeatures ++ exts)
+                         (map genericToExecutionFeature execFeatures ++ exts ++ debugger)
                          initSt
                          (resultCont compRef glsRef frm explainFailure . Result)
            sayCrux (Log.TotalPathsExplored i)
diff --git a/crux/src/Crux/Config/Common.hs b/crux/src/Crux/Config/Common.hs
index 19ebf2e43..4b252295b 100644
--- a/crux/src/Crux/Config/Common.hs
+++ b/crux/src/Crux/Config/Common.hs
@@ -205,6 +205,9 @@ data CruxOptions = CruxOptions
   , outputOptions            :: OutputOptions
     -- ^ Output options grouped together for easy transfer to the logger
 
+  , debug                    :: Bool
+    -- ^ Drop into the Crucible debugger before simulation begins
+
   }
   deriving (Generic)
 
@@ -364,6 +367,10 @@ cruxOptions = Config
 
           onlineProblemFeatures <- pure noFeatures
 
+          debug <-
+            section "debug" yesOrNoSpec False
+            "Drop into the Crucible debugger before simulation begins"
+
           pure CruxOptions
             { outputOptions = OutputOptions
               { colorOptions = ColorOptions
@@ -525,6 +532,10 @@ cruxOptions = Config
          ++ " i.e. one of [real|ieee|uninterpreted|default]. "
          ++ "Default representation is solver specific: [cvc4|yices]=>real, z3=>ieee.")
         $ ReqArg "FPREP" $ \v opts -> Right opts { floatMode = map toLower v }
+
+      , Option [] ["debug"]
+        "Drop into the Crucible debugger before simulation begins"
+        $ NoArg $ \opts -> Right opts { debug = True }
       ]
   }