diff --git a/src/Pate/Memory/MemTrace.hs b/src/Pate/Memory/MemTrace.hs
index 115d23b5..c92802d6 100644
--- a/src/Pate/Memory/MemTrace.hs
+++ b/src/Pate/Memory/MemTrace.hs
@@ -109,7 +109,7 @@ import Data.Macaw.Memory
            , MemWord, memWordToUnsigned, segmentFlags
            , Memory, emptyMemory, memWord, segoffSegment
            , segoffAddr, readWord8, readWord16be, readWord16le
-           , readWord32le, readWord32be, readWord64le, readWord64be, MemAddr, asSegmentOff
+           , readWord32le, readWord32be, readWord64le, readWord64be, MemAddr (..), asSegmentOff
            )
 import qualified Data.Macaw.Memory.Permissions as MMP
 import Data.Macaw.Symbolic.Backend (MacawEvalStmtFunc, MacawArchEvalFn(..))
@@ -154,11 +154,15 @@ import qualified Pate.ExprMappable as PEM
 import           What4.ExprHelpers ( integerToNat )
 import qualified What4.ExprHelpers as WEH
 import qualified Pate.Memory as PM
-import Data.Macaw.CFG (ArchSegmentOff, RegisterInfo, ip_reg, MemAddr (MemAddr))
+import Data.Macaw.CFG (ArchSegmentOff, RegisterInfo, ip_reg)
 import qualified Pate.SimulatorRegisters as PSr
 import Data.Data (Typeable, eqT)
 import Data.Maybe (mapMaybe)
 import qualified Data.Parameterized.TraversableF as TF
+import qualified What4.JSON as W4S
+import qualified Data.Aeson as JSON
+import What4.JSON ((.=), (.==), (.=~))
+import qualified Pate.Pointer as Ptr
 
 ------
 -- * Undefined pointers
@@ -189,6 +193,11 @@ data UndefinedPtrOps sym =
 -- Needed since SymBV is a type alias
 newtype SymBV' sym w = SymBV' { unSymBV :: SymBV sym w }
 
+instance W4S.SerializableExprs sym => W4S.W4Serializable sym (SymBV' sym w) where
+  w4Serialize (SymBV' bv) = W4S.w4SerializeF bv
+
+instance W4S.SerializableExprs sym => W4S.W4SerializableF sym (SymBV' sym)
+
 instance OrdF (SymExpr sym) => TestEquality (SymBV' sym) where
   testEquality a b = case compareF a b of
     EQF -> Just Refl
@@ -620,6 +629,10 @@ data MemOpCondition sym
   = Unconditional
   | Conditional (Pred sym)
 
+instance W4S.SerializableExprs sym => W4S.W4Serializable sym (MemOpCondition sym) where
+  w4Serialize = \case
+    Unconditional -> W4S.w4SerializeString ("unconditional" :: String)
+    Conditional p -> W4S.object ["condition" .== p]
 
 deriving instance Show (Pred sym) => Show (MemOpCondition sym)
 
@@ -628,6 +641,8 @@ data MemOpDirection =
   | Write
   deriving (Eq, Ord, Show)
 
+instance W4S.W4Serializable sym MemOpDirection where
+  w4Serialize = W4S.w4SerializeString
 
 data MemOp sym ptrW where
   MemOp ::
@@ -731,6 +746,10 @@ instance OrdF (SymExpr sym) => Ord (MemOp sym ptrW) where
 data RegOp sym arch =
   RegOp (MapF.MapF (ArchReg arch) (PSr.MacawRegEntry sym))
 
+instance (W4S.W4SerializableFC (ArchReg arch), W4S.SerializableExprs sym)
+  => W4S.W4Serializable sym (RegOp sym arch) where
+  w4Serialize (RegOp m) = W4S.object ["reg_op" .= m]
+
 instance PEM.ExprMappable sym (RegOp sym arch) where
   mapExpr sym f (RegOp m) = (RegOp . PEM.unExprMapFElems) <$> PEM.mapExpr sym f (PEM.ExprMapFElems m)
 
@@ -744,6 +763,38 @@ instance PEM.ExprMappable sym (TraceEvent sym arch) where
     RegOpEvent i rop -> RegOpEvent <$> PEM.mapExpr sym f i <*> PEM.mapExpr sym f rop
     TraceMemEvent i mop -> TraceMemEvent <$> PEM.mapExpr sym f i <*> PEM.mapExpr sym f mop
 
+instance W4S.W4Serializable sym  (MemAddr w) where
+  w4Serialize addr = do
+    base_json <- return $ JSON.toJSON (addrBase addr)
+    off_json <- return $ JSON.toJSON (show (addrOffset addr))
+    return $ JSON.object ["base" JSON..= base_json, "offset" JSON..= off_json]
+
+instance W4S.W4Serializable sym  (MemSegmentOff w) where
+  w4Serialize segOff = W4S.w4Serialize $ segoffAddr segOff
+
+instance (W4S.W4SerializableFC (ArchReg arch), W4S.SerializableExprs sym)
+  => W4S.W4Serializable sym (TraceEvent sym arch) where
+    w4Serialize = \case
+      RegOpEvent i rop -> W4S.object ["instruction" .= i, "register_op" .= rop]
+      TraceMemEvent i mop -> W4S.object ["instruction" .= i, "memory_op" .= mop]
+
+instance W4S.SerializableExprs sym => W4S.W4Serializable sym (MemEvent sym ptrW) where
+  w4Serialize = \case
+    MemOpEvent mop -> W4S.object ["mem_op" .= mop]
+    SyscallEvent i r0 -> W4S.object ["syscall" .= i, "r0" .== r0]
+    ExternalCallEvent nm bvs -> W4S.object ["external_call" .= nm, "args" .= bvs]
+
+instance W4S.SerializableExprs sym => W4S.W4Serializable sym (MemOp sym ptrW) where
+  w4Serialize (MemOp addr dir cond n val end) =
+    W4S.object
+      [ "addr" .= Ptr.fromLLVMPointer addr
+      , "direction" .= dir
+      , "condition" .= cond
+      , "size" .= n
+      , "value" .= Ptr.fromLLVMPointer val
+      , "endianness" .=~ end
+      ]
+
 data MemEvent sym ptrW where
   MemOpEvent :: MemOp sym ptrW -> MemEvent sym ptrW
   SyscallEvent :: forall sym ptrW w.
diff --git a/src/Pate/PatchPair.hs b/src/Pate/PatchPair.hs
index 0e3c282f..6b92ce43 100644
--- a/src/Pate/PatchPair.hs
+++ b/src/Pate/PatchPair.hs
@@ -68,6 +68,7 @@ module Pate.PatchPair (
   , asSingleton
   , zip
   , jsonPatchPair
+  , w4SerializePair
   ) where
 
 import           Prelude hiding (zip)
@@ -92,6 +93,8 @@ import qualified Pate.ExprMappable as PEM
 import Data.Parameterized (Some(..))
 import Control.Monad.Identity
 import Pate.TraceTree
+import qualified What4.JSON as W4S
+import What4.JSON
 
 -- | A pair of values indexed based on which binary they are associated with (either the
 --   original binary or the patched binary).
@@ -519,4 +522,20 @@ jsonPatchPair f ppair = case ppair of
 
 
 instance (forall bin. JSON.ToJSON (tp bin)) => JSON.ToJSON (PatchPair tp) where
-  toJSON p = jsonPatchPair (JSON.toJSON) p
\ No newline at end of file
+  toJSON p = jsonPatchPair (JSON.toJSON) p
+
+w4SerializePair :: PatchPair f -> (forall bin. f bin -> W4S.W4S sym JSON.Value) -> W4S.W4S sym JSON.Value
+w4SerializePair ppair f = case ppair of
+    PatchPair o p -> do
+      o_v <- f o
+      p_v <- f p
+      return $ JSON.object ["original" JSON..= o_v, "patched" JSON..= p_v]
+    PatchPairOriginal o -> do
+      o_v <- f o
+      return $ JSON.object ["original" JSON..= o_v]
+    PatchPairPatched p -> do
+      p_v <- f p
+      return $ JSON.object ["patched" JSON..= p_v]
+
+instance W4S.W4SerializableF sym f => W4S.W4Serializable sym (PatchPair f) where
+  w4Serialize ppair = w4SerializePair ppair w4SerializeF
\ No newline at end of file
diff --git a/src/Pate/SimulatorRegisters.hs b/src/Pate/SimulatorRegisters.hs
index aaa41f85..1173fbf7 100644
--- a/src/Pate/SimulatorRegisters.hs
+++ b/src/Pate/SimulatorRegisters.hs
@@ -8,6 +8,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE OverloadedStrings #-}
 
 module Pate.SimulatorRegisters (
   CrucBaseTypes,
diff --git a/src/Pate/Verification/StrongestPosts/CounterExample.hs b/src/Pate/Verification/StrongestPosts/CounterExample.hs
index 6bfaaeae..5f9076c2 100644
--- a/src/Pate/Verification/StrongestPosts/CounterExample.hs
+++ b/src/Pate/Verification/StrongestPosts/CounterExample.hs
@@ -11,6 +11,7 @@
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
 
 module Pate.Verification.StrongestPosts.CounterExample
   ( TotalityCounterexample(..)
@@ -61,6 +62,8 @@ import qualified What4.Concrete as W4
 import Data.Functor.Const
 import qualified Data.Parameterized.Map as MapF
 import Data.Maybe (mapMaybe)
+import qualified What4.JSON as W4S
+import What4.JSON
 
 -- | A totality counterexample represents a potential control-flow situation that represents
 --   desynchronization of the original and patched program. The first tuple represents
@@ -216,9 +219,17 @@ groundMuxTree sym evalFn = MT.collapseMuxTree sym ite
 data TraceEvents sym arch =
   TraceEvents (PPa.PatchPairC (MT.RegOp sym arch, [TraceEventGroup sym arch]))
 
+instance (PA.ValidArch arch, PSo.ValidSym sym) => W4S.W4Serializable sym (TraceEvents sym arch) where
+  w4Serialize (TraceEvents p) = PPa.w4SerializePair p $ \(Const (rop, evs)) ->
+    W4S.object [ "initial_regs" .= rop, "events" .= evs]
+
 data TraceEventGroup sym arch =
   TraceEventGroup (Maybe (MM.ArchSegmentOff arch)) [MT.TraceEvent sym arch]
 
+instance (PA.ValidArch arch, PSo.ValidSym sym) => W4S.W4Serializable sym (TraceEventGroup sym arch) where
+  w4Serialize (TraceEventGroup mi evs) =
+    W4S.object [ "instruction_addr" .= mi, "events" .= evs]
+
 ppRegOp :: forall sym arch ann. (PA.ValidArch arch, PSo.ValidSym sym) => MT.RegOp sym arch -> [PP.Doc ann]
 ppRegOp (MT.RegOp m) = mapMaybe (\(MapF.Pair r v) -> 
   case PA.displayRegister r of
@@ -260,6 +271,7 @@ instance (PSo.ValidSym sym, PA.ValidArch arch) => IsTraceNode '(sym,arch) "trace
       "Event Trace:" PP.<+> PPa.ppPatchPair' (\(Const (_init_regs, s)) -> 
         ppTraceEventSummary s) evs))
     [Summary, Simplified]
+  jsonNode () v = W4S.w4ToJSON @sym v
 
 ppTraceEventSummary ::
   forall sym arch a.
diff --git a/src/What4/JSON.hs b/src/What4/JSON.hs
index d05725b5..bd0a354e 100644
--- a/src/What4/JSON.hs
+++ b/src/What4/JSON.hs
@@ -15,6 +15,7 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE LambdaCase #-}
 
 module What4.JSON 
   ( W4S
@@ -23,27 +24,25 @@ module What4.JSON
   , W4SerializableFC
   , SerializableExprs
   , w4ToJSON
+  , object
+  , w4SerializeString
+  , (.=)
+  , (.==)
+  , (.=~)
   ) where
 
-import           Control.Monad.Except (ExceptT, MonadError)
-import           Control.Monad.Reader (ReaderT, MonadReader)
-import           Control.Monad.IO.Class (MonadIO)
-import           Control.Monad.State (StateT, MonadState (..), State, modify, evalState, runState)
+import           Control.Monad.State (MonadState (..), State, modify, evalState, runState)
 
-import           Data.Map.Ordered (OMap)
 import qualified Data.Map.Ordered as OMap
 import           Data.Map (Map)
 import           Data.Text (Text)
-import qualified Data.Text as Text
 import           Data.Data (Proxy(..), Typeable)
 import qualified Data.Aeson as JSON
-import           Data.Aeson ( (.=) )
 
 import           Data.Parameterized.Some (Some(..))
 
 import qualified What4.Interface as W4
 
-import           What4.Serialize.Parser (SomeSymFn(..))
 import qualified What4.Serialize.Printer as W4S
 import qualified What4.Serialize.Parser as W4D
 import qualified What4.Expr.Builder as W4B
@@ -56,6 +55,12 @@ import qualified Data.Text as T
 import GHC.IO (catch, evaluate, unsafePerformIO)
 import GHC.IO.Exception (IOException)
 import Control.DeepSeq (force)
+import Data.Parameterized.Map (MapF)
+import qualified Data.Parameterized.Map as MapF
+import Data.Kind
+import qualified Lang.Crucible.Utils.MuxTree as MT
+import qualified Data.Parameterized.Context as Ctx
+import qualified Data.Parameterized.TraversableFC as TFC
 
 
 
@@ -67,11 +72,13 @@ newtype W4S sym a = W4S (State (ExprCache sym) a)
 class W4Serializable sym a where
   w4Serialize :: a -> W4S sym JSON.Value
 
+w4SerializeString :: Show a => a -> W4S sym JSON.Value
+w4SerializeString s = return $ JSON.String (T.pack (show s))
 
-w4ToJSON :: forall sym a. W4Serializable sym a => a -> JSON.Value
+w4ToJSON :: forall sym a. SerializableExprs sym => W4Serializable sym a => a -> JSON.Value
 w4ToJSON a = let W4S f = w4Serialize @sym a in evalState f (ExprCache Map.empty)
 
-class W4SerializableF sym f where
+class W4SerializableF sym (f :: k -> Type) where
   withSerializable :: Proxy sym -> p f -> q tp -> (W4Serializable sym (f tp) => a) -> a
 
   default withSerializable :: W4Serializable sym (f tp) => Proxy sym -> p f -> q tp -> (W4Serializable sym (f tp) => a) -> a
@@ -114,9 +121,9 @@ instance sym ~ W4B.ExprBuilder t fs scope => W4Serializable sym (W4B.Expr t tp)
               let var_env = map (\(Some bv, t) -> (show (W4B.bvarName bv), t)) $ OMap.toAscList $ W4S.resFreeVarEnv result
               let fn_env = map (\(W4S.SomeExprSymFn fn, t) -> (show (W4B.symFnName fn), t)) $ OMap.toAscList $ W4S.resSymFnEnv result
               let sexpr = W4S.resSExpr result
-              return $ JSON.object [ "symbolic" .= JSON.String (W4D.printSExpr mempty sexpr), "vars" .= var_env, "fns" .= fn_env ]
+              return $ JSON.object [ "symbolic" JSON..= JSON.String (W4D.printSExpr mempty sexpr), "vars" JSON..= var_env, "fns" JSON..= fn_env ]
             case mv of
-              Left er -> return $ JSON.object [ "symbolic_serialize_err" .= er]
+              Left er -> return $ JSON.object [ "symbolic_serialize_err" JSON..= er]
               Right v -> return v
         modify $ \(ExprCache s') -> ExprCache (Map.insert (Some e) v s')
         return v
@@ -129,35 +136,74 @@ instance W4SerializableF sym x => W4Serializable sym (Some x) where
   w4Serialize (Some x) = w4SerializeF x
 
 instance (W4Serializable sym x, W4Serializable sym y) => W4Serializable sym (x, y) where
-  w4Serialize (x,y) = do
-    x_v <- w4Serialize x
-    y_v <- w4Serialize y
-    return $ JSON.object [ "fst" .= x_v, "snd" .= y_v]
+  w4Serialize (x,y) = object [ "fst" .= x, "snd" .= y]
+
+instance (W4Serializable sym x) => W4Serializable sym [x] where
+  w4Serialize xs = do
+    xs_json <- mapM w4Serialize xs
+    return $ JSON.toJSON xs_json
+
+instance W4Serializable sym JSON.Value where
+  w4Serialize = return
 
 instance (W4Serializable sym x, W4Serializable sym y) => W4Serializable sym (Map x y) where
   w4Serialize x = do
-    objs <- forM (Map.toList x) $ \(k, v) -> do
-      k_v <- w4Serialize k
-      v_v <- w4Serialize v
-      return $ JSON.object [ "key" .= k_v, "val" .= v_v]
-    return $ JSON.object [ "map" .= objs ]
+    objs <- forM (Map.toList x) $ \(k, v) -> object [ "key" .= k, "val" .= v]
+    object [ "map" .= objs ]
 
 type SerializableExprs sym = W4SerializableF sym (W4.SymExpr sym)
 
 instance (SerializableExprs sym, W4Serializable sym x) => W4Serializable sym (W4P.PredMap sym x k) where
   w4Serialize x = do
-    objs <- forM (W4P.toList x) $ \(k,p) -> do
-      k_v <- w4Serialize k
-      p_v <- w4SerializeF p
-      return $ JSON.object [ "val" .= k_v, "pred" .= p_v]
-    let (repr :: String) = case typeRepr x of
+    objs <- forM (W4P.toList x) $ \(k,p) -> object [ "val" .= k, "pred" .== p]
+    let (repr :: Text) = case typeRepr x of
           W4P.PredConjRepr -> "conj"
           W4P.PredDisjRepr -> "disj"
-    return $ JSON.object [ "predmap" .= objs, "kind" .= repr ]
+    object [ "predmap" .= objs, "kind" .= repr ]
 
 instance W4Serializable sym Integer where
   w4Serialize i = return $ JSON.toJSON i
 
-instance W4Serializable sym String where
+instance W4Serializable sym Text where
   w4Serialize i = return $ JSON.toJSON i
 
+instance W4Serializable sym a => W4Serializable sym (Maybe a) where
+  w4Serialize = \case
+    Just a -> w4Serialize a
+    Nothing -> return $ JSON.Null
+
+instance W4Serializable sym (W4.NatRepr n) where
+  w4Serialize nr = w4Serialize $ W4.intValue nr
+
+instance (W4SerializableF sym x, W4SerializableF sym y) => W4Serializable sym (MapF x y) where
+  w4Serialize x = do
+    objs <- forM (MapF.toList x) $ \(MapF.Pair k v) -> object [ "key" .== k, "val" .== v]
+    object [ "map" .= objs ]
+
+instance (W4Serializable sym tp, SerializableExprs sym) => W4Serializable sym (MT.MuxTree sym tp) where
+  w4Serialize mt = case MT.viewMuxTree mt of
+    [] -> error "Serialize: Invalid Muxtree"
+    [(e,_)] -> w4Serialize e
+    es -> do
+      body <- forM es $ \(e,p) ->
+        object [ "val" .= e, "pred" .== p]
+      object ["muxtree" .= body]
+
+instance W4SerializableF sym f => W4Serializable sym (Ctx.Assignment f ctx) where
+  w4Serialize x = w4Serialize $ TFC.toListFC Some x
+
+data W4KeyValue sym = forall a. W4Serializable sym a => W4KeyValue JSON.Key a
+
+(.=) :: W4Serializable sym v => JSON.Key -> v -> W4KeyValue sym
+(.=) = W4KeyValue
+
+(.==) :: forall sym v tp. W4SerializableF sym v => JSON.Key -> v tp -> W4KeyValue sym
+(.==) = \k v -> withSerializable (Proxy @sym) (Proxy @v) (Proxy @tp) $ W4KeyValue k v
+
+(.=~) :: Show v => JSON.Key -> v -> W4KeyValue sym
+(.=~) = \k v -> W4KeyValue k (T.pack (show v))
+
+object :: [W4KeyValue sym] -> W4S sym JSON.Value
+object kvs = fmap JSON.object $ forM kvs $ \(W4KeyValue k v) -> do
+    v_json <- w4Serialize v
+    return $ k JSON..= v_json
\ No newline at end of file