diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,9 @@
+# 0.13 -- 2026-09-10
+
+* Add support for GHC 9.12 (at 9.12.2) and bump from 9.10.1 to 9.10.3.
+* Support LLVM 22.
+* **BREAKING**: `explainFailure` now takes a `FloatModeRepr` argument.
+
 # 0.12 -- 2026-01-29
 
 # 0.11 -- 2025-11-09
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -50,7 +50,7 @@
 and `cabal` version 3.10. We recommend Yices 2.6.x, and Z3
 4.8.x. Technically, only one of Yices or Z3 is required, and CVC4 is
 also supported. However, in practice, having both tends to be
-convenient. Finally, LLVM versions from 3.6 through 21 are likely to
+convenient. Finally, LLVM versions from 3.6 through 22 are likely to
 work well, and any failures with versions in that range should be
 [reported as bugs](https://github.com/GaloisInc/crucible/issues).
 
diff --git a/crux-llvm.cabal b/crux-llvm.cabal
--- a/crux-llvm.cabal
+++ b/crux-llvm.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          crux-llvm
-Version:       0.12
+Version:       0.13
 Author:        Galois Inc.
 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com
 Copyright:     (c) Galois, Inc 2014-2022
@@ -55,7 +55,7 @@
                -Wincomplete-uni-patterns
   ghc-prof-options: -O2
   default-language: Haskell2010
-  build-depends:    base >= 4.8 && < 4.21
+  build-depends:    base >= 4.8 && < 4.22
                   , bytestring
                   , containers
                   , crucible
@@ -64,7 +64,7 @@
                   , crux
                   , directory
                   , filepath
-                  , lens
+                  , microlens
                   , process
                   , text
                   , what4
@@ -88,7 +88,6 @@
   ghc-options:
     -Wall
     -Werror=ambiguous-fields
-    -Werror=compat-unqualified-imports
     -Werror=deferred-type-errors
     -Werror=deprecated-flags
     -Werror=deprecations
@@ -160,6 +159,10 @@
       -Werror=deprecated-type-abstractions
       -Werror=incomplete-record-selectors
 
+  if impl(ghc < 9.12)
+    ghc-options:
+      -Werror=compat-unqualified-imports
+
 common testdefs
   build-depends: tasty            >= 0.10
                , tasty-hunit      >= 0.10
@@ -190,6 +193,7 @@
     logict,
     llvm-pretty,
     llvm-pretty-bc-parser >= 0.5,
+    microlens-mtl,
     mtl,
     parameterized-utils,
     prettyprinter >= 1.7.0
@@ -223,6 +227,7 @@
     aeson,
     crux-llvm,
     lumberjack,
+    microlens-th,
     websockets >= 0.12
 
   main-is: Main.hs
diff --git a/for-ide/Main.hs b/for-ide/Main.hs
--- a/for-ide/Main.hs
+++ b/for-ide/Main.hs
@@ -4,7 +4,6 @@
 
 module Main (main) where
 
-import Control.Lens (makeLenses, set, view)
 import Crux (OutputConfig)
 import qualified Crux
 import Crux.Config.Common (OutputOptions)
@@ -16,6 +15,9 @@
   )
 import qualified Data.Aeson as JSON
 import Data.Text as Text (Text, unpack)
+import Lens.Micro (set)
+import Lens.Micro.Extras (view)
+import Lens.Micro.TH (makeLenses)
 import qualified Lumberjack as LJ
 import qualified Network.WebSockets as WS
 import Paths_crux_llvm (version)
diff --git a/src/Crux/LLVM/Config.hs b/src/Crux/LLVM/Config.hs
--- a/src/Crux/LLVM/Config.hs
+++ b/src/Crux/LLVM/Config.hs
@@ -9,6 +9,7 @@
 import           Control.Exception ( Exception, displayException, throwIO )
 import           Control.Monad ( guard )
 import           Control.Monad.State ( liftIO, MonadIO )
+import           Data.List (intercalate)
 import qualified Data.Text as Text
 import           System.Directory ( doesDirectoryExist )
 import           System.Environment ( getExecutablePath )
@@ -46,7 +47,7 @@
 ppCError err = case err of
     NoFiles                -> "crux-llvm requires at least one input file."
     EnvError msg           -> msg
-    BadFun fnName isMain   -> unlines $
+    BadFun fnName isMain   -> ofLines $
                                 [ "The '" ++ fnName ++ "' function should have no arguments"] ++
                                 [ "Enable `supply-main-arguments` to relax this restriction"
                                 | isMain
@@ -54,14 +55,16 @@
     MissingFun x           -> "Cannot find code for " ++ show x
     LLVMParseError e       -> LLVM.formatError e
     ClangError n sout serr ->
-      unlines $ [ "`clang` compilation failed."
+      ofLines $ [ "`clang` compilation failed."
                 , "*** Exit code: " ++ show n
                 , "*** Standard out:"
                 ] ++
                 [ "   " ++ l | l <- lines sout ] ++
                 [ "*** Standard error:" ] ++
                 [ "   " ++ l | l <- lines serr ]
-
+  where
+    -- Contrast with `Prelude.unlines`, which appends a trailing newline
+    ofLines = intercalate "\n"
 
 throwCError :: MonadIO m => CError -> m b
 throwCError e = liftIO (throwIO e)
diff --git a/src/Crux/LLVM/Simulate.hs b/src/Crux/LLVM/Simulate.hs
--- a/src/Crux/LLVM/Simulate.hs
+++ b/src/Crux/LLVM/Simulate.hs
@@ -16,21 +16,23 @@
 
 module Crux.LLVM.Simulate where
 
-import qualified Control.Lens as Lens
 import Control.Monad (unless)
-import Data.String (fromString)
-import qualified Data.Map.Strict as Map
+import Control.Monad.IO.Class (liftIO)
 import Data.IORef
 import qualified Data.List as List
+import qualified Data.Map.Strict as Map
 import Data.Maybe ( fromMaybe )
 import qualified Data.Parameterized.Map as MapF
 import Data.Sequence (Seq)
+import Data.String (fromString)
 import qualified Data.Traversable as T
-import Control.Lens ((&), (%~), (%=), (^.), use, view)
-import Control.Monad.IO.Class (liftIO)
 import Data.Text as Text (Text, pack)
 import Data.Void (Void)
 import GHC.Exts ( proxy# )
+import qualified Lens.Micro as Lens
+import Lens.Micro ((&), (%~), (^.))
+import Lens.Micro.Extras (view)
+import Lens.Micro.Mtl ((%=), use)
 
 import System.IO (stdout)
 
@@ -193,7 +195,7 @@
   LLVMOptions ->
   Crux.SimulatorCallbacks msgs st Crux.Types.CruxSimulationResult
 simulateLLVMFile llvm_file llvmOpts =
-  Crux.SimulatorCallbacks $
+  Crux.SimulatorCallbacks $ \fm ->
     do bbMapRef <- newIORef (Map.empty :: LLVMAnnMap sym)
        let ?recordLLVMAnnotation =
              \callStack an bb ->
@@ -205,7 +207,7 @@
                  do halloc <- newHandleAllocator
                     setupFileSim halloc llvm_file llvmOpts bak maybeOnline
            , Crux.onErrorHook =
-               \bak -> return (explainFailure (backendGetSym bak) bbMapRef)
+               \bak -> return (explainFailure (backendGetSym bak) fm bbMapRef)
            , Crux.resultHook = \_sym result -> return result
            }
 
@@ -424,13 +426,14 @@
 detailLimit = 10
 
 explainFailure :: IsSymInterface sym
-               => sym ~ WEB.ExprBuilder t st fs
+               => sym ~ WEB.ExprBuilder t st (WEB.Flags fm)
                => sym
+               -> WEB.FloatModeRepr fm
                -> IORef (LLVMAnnMap sym)
                -> Crux.Explainer sym t ann
-explainFailure sym bbMapRef evalFn gl =
+explainFailure sym fm bbMapRef evalFn gl =
   do bb <- readIORef bbMapRef
-     ex <- explainCex sym bb evalFn >>= \f -> f (gl ^. labeledPred)
+     ex <- explainCex sym fm bb evalFn >>= \f -> f (gl ^. labeledPred)
      let details =
            case ex of
              NoExplanation -> mempty
diff --git a/test/Test.hs b/test/Test.hs
--- a/test/Test.hs
+++ b/test/Test.hs
@@ -6,7 +6,6 @@
 module Main (main) where
 
 import           Control.Exception ( SomeException, catches, try, Handler(..), IOException )
-import           Control.Lens ( (^?), _Right )
 import           Control.Monad ( unless, when )
 import           Data.Bifunctor ( first )
 import qualified Data.ByteString.Lazy as BSIO
@@ -18,6 +17,7 @@
 import qualified Data.Version as Version
 import           Data.Versions ( Versioning, versioning, prettyV, major )
 import qualified GHC.IO.Exception as GE
+import           Lens.Micro ((^?), _Right)
 import           Numeric.Natural
 import           System.Environment ( withArgs, lookupEnv )
 import           System.Exit ( ExitCode(..) )