diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,5 @@
+# 0.9 -- 2026-01-29
+
 # 0.8 -- 2025-11-09
 
 * We now support running simulations with custom users state.
diff --git a/crux.cabal b/crux.cabal
--- a/crux.cabal
+++ b/crux.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          crux
-Version:       0.8.0.0
+Version:       0.9
 Copyright:     (c) Galois, Inc. 2018-2022
 Author:        sweirich@galois.com
 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com
diff --git a/src/Crux/Model.hs b/src/Crux/Model.hs
--- a/src/Crux/Model.hs
+++ b/src/Crux/Model.hs
@@ -1,6 +1,7 @@
 -- | This file is almost exactly the same as crucible-c/src/Model.hs
 
 {-# Language DataKinds #-}
+{-# Language OverloadedStrings #-}
 {-# Language PolyKinds #-}
 {-# Language Rank2Types #-}
 {-# Language TypeFamilies #-}
@@ -19,6 +20,8 @@
 import qualified Numeric as N
 import           LibBF (BigFloat)
 import qualified LibBF as BF
+import qualified Prettyprinter as PP
+import           Prettyprinter (Doc)
 
 import           Lang.Crucible.Types
 
@@ -69,9 +72,13 @@
                                                -- NB, 53 bits of precision for double
    | otherwise        = BF.bfToString 16 (BF.showFree (Just 53) <> BF.addPrefix) x
 
+showBoolLiteral :: Bool -> String
+showBoolLiteral b = if b then "true" else "false"
+
 valsJS :: BaseTypeRepr ty -> Vals ty -> IO [JS]
 valsJS ty (Vals xs) =
   let showEnt = case ty of
+        -- NOTE: Keep these cases in sync with those in 'prettyVals'.
         BaseBVRepr n -> showBVEnt n
         BaseFloatRepr (FloatingPointPrecisionRepr eb sb)
           | Just Refl <- testEquality eb (knownNat @8)
@@ -82,6 +89,7 @@
           , Just Refl <- testEquality sb (knownNat @53)
           -> showEnt' showDoubleLiteral (64 :: Int)
         BaseRealRepr -> showEnt' (show . toDouble) (knownNat @64)
+        BaseBoolRepr -> showBoolEnt
         _ -> error ("Type not implemented: " ++ show ty)
 
   in mapM showEnt xs
@@ -109,6 +117,82 @@
       , "bits"         ~> jsStr (show n)
       ]
 
+  showBoolEnt :: Entry Bool -> IO JS
+  showBoolEnt e = do
+    do l <- fromMaybe jsNull <$> jsLoc (entryLoc e)
+       pure $ jsObj
+         [ "name" ~> jsStr (entryName e)
+         , "loc"  ~> l
+         , "val"  ~> jsStr (showBoolLiteral (entryValue e))
+         ]
+
 modelJS :: ModelView -> IO JS
 modelJS m =
   jsList . concat <$> sequence (MapF.foldrWithKey (\k v xs -> valsJS k v : xs) [] (modelVals m))
+
+-- Pretty-print all entries in a model for a given base type.
+prettyVals :: BaseTypeRepr ty -> Vals ty -> [Doc ann]
+prettyVals ty (Vals xs) =
+  let ppEnt = case ty of
+        -- NOTE: Keep these cases in sync with those in 'valsJS'.
+        BaseBVRepr n -> prettyBVEnt n
+
+        BaseFloatRepr (FloatingPointPrecisionRepr eb sb)
+          | Just Refl <- testEquality eb (knownNat @8)
+          , Just Refl <- testEquality sb (knownNat @24)
+          -> prettyEnt' showFloatLiteral
+
+        BaseFloatRepr (FloatingPointPrecisionRepr eb sb)
+          | Just Refl <- testEquality eb (knownNat @11)
+          , Just Refl <- testEquality sb (knownNat @53)
+          -> prettyEnt' showDoubleLiteral
+
+        BaseRealRepr ->
+          -- same semantics as valsJS: print reals via toDouble
+          prettyEnt' (show . toDouble)
+
+        BaseBoolRepr ->
+          prettyEnt' showBoolLiteral
+
+        _ ->
+          error ("Type not implemented: " ++ show ty)
+  in
+    map ppEnt xs
+
+-- Generic entry printer for "simple" values.
+prettyEnt' :: (a -> String) -> Entry a -> Doc ann
+prettyEnt' repr e =
+  PP.hsep
+    [ PP.pretty (entryName e)
+    , "="
+    , PP.pretty (repr (entryValue e))
+    ]
+
+-- Bitvector entries: signed, unsigned, decimal on a single line.
+prettyBVEnt :: (1 <= w) => NatRepr w -> Entry (BV w) -> Doc ann
+prettyBVEnt n e =
+  let v   = entryValue e
+      sg  = showBVLiteralSigned   n v
+      un  = showBVLiteralUnsigned n v
+      dec = showBVLiteralDecimal  n v
+  in
+    PP.hsep
+      [ PP.pretty (entryName e)
+      , "="
+      , PP.pretty sg
+      , "(signed),"
+      , PP.pretty un
+      , "(unsigned),"
+      , PP.pretty dec
+      , "(decimal)"
+      ]
+
+-- Human-readable model as a Prettyprinter 'Doc'.
+prettyModel :: ModelView -> Doc ann
+prettyModel m =
+  PP.vsep
+    (MapF.foldrWithKey
+       (\ty vals docs -> prettyVals ty vals ++ docs)
+       []
+       (modelVals m)
+    )