diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,22 @@
 # Revision history for typed-protocols
 
+## 1.1.0.0 -- 05.08.2025
+
+### Breaking changes
+
+* Annotated codecs which allow to retain original bytes received from the network.
+  The `Codec` type evolved into a new `CodecF` data type, and two type aliases
+  `AnnotatedCodec`, `Codec`.
+* `prop_codec` properties moved to `typed-protocols:codec-properties` library
+  (`Network.TypedProtocol.Codec.Properties` module).  They now return the
+  `QuickCheck`'s `Property` rather than a `Bool`.
+
+### Non-breaking changes
+
+## 1.0.0.0
+
+* Hackage release.
+
 ## 0.3.0.0
 
 * `AnyMessageWithAgency` pattern synonym is exported as a constructor of `AnyMessage`.
diff --git a/cborg/Network/TypedProtocol/Codec/CBOR.hs b/cborg/Network/TypedProtocol/Codec/CBOR.hs
--- a/cborg/Network/TypedProtocol/Codec/CBOR.hs
+++ b/cborg/Network/TypedProtocol/Codec/CBOR.hs
@@ -25,10 +25,10 @@
 import Network.TypedProtocol.Core
 
 
--- | Construct a 'Codec' for a CBOR based serialisation format, using strict
+-- | Construct a 'CodecF' for a CBOR based serialisation format, using strict
 -- 'BS.ByteString's.
 --
--- This is an adaptor between the @cborg@ library and the 'Codec' abstraction.
+-- This is an adaptor between the @cborg@ library and the 'CodecF' abstraction.
 --
 -- It takes encode and decode functions for the protocol messages that use the
 -- CBOR library encoder and decoder.
@@ -38,7 +38,7 @@
 -- natively produces chunks).
 --
 mkCodecCborStrictBS
-  :: forall ps m. MonadST m
+  :: forall ps m f. MonadST m
 
   => (forall (st :: ps) (st' :: ps).
              StateTokenI st
@@ -49,10 +49,10 @@
   -> (forall (st :: ps) s.
              ActiveState st
           => StateToken st
-          -> CBOR.Decoder s (SomeMessage st))
+          -> CBOR.Decoder s (f st))
   -- ^ cbor decoder
 
-  -> Codec ps CBOR.DeserialiseFailure m BS.ByteString
+  -> CodecF ps CBOR.DeserialiseFailure m f BS.ByteString
 mkCodecCborStrictBS cborMsgEncode cborMsgDecode =
     Codec {
       encode = \msg  -> convertCborEncoder cborMsgEncode msg,
@@ -65,11 +65,12 @@
       . cborEncode
 
     convertCborDecoder
-      :: (forall s. CBOR.Decoder s a)
-      -> m (DecodeStep BS.ByteString CBOR.DeserialiseFailure m a)
+      :: (forall s. CBOR.Decoder s (f a))
+      -> m (DecodeStep BS.ByteString CBOR.DeserialiseFailure m (f a))
     convertCborDecoder cborDecode =
         convertCborDecoderBS cborDecode stToIO
 
+
 convertCborDecoderBS
   :: forall s m a. Functor m
   => CBOR.Decoder s a
@@ -89,16 +90,16 @@
     go (CBOR.Partial k)        = DecodePartial (fmap go . liftST . k)
 
 
--- | Construct a 'Codec' for a CBOR based serialisation format, using lazy
+-- | Construct a 'CodecF' for a CBOR based serialisation format, using lazy
 -- 'BS.ByteString's.
 --
--- This is an adaptor between the @cborg@ library and the 'Codec' abstraction.
+-- This is an adaptor between the @cborg@ library and the 'CodecF' abstraction.
 --
 -- It takes encode and decode functions for the protocol messages that use the
 -- CBOR library encoder and decoder.
 --
 mkCodecCborLazyBS
-  :: forall ps m. MonadST m
+  :: forall ps m f. MonadST m
 
   => (forall (st :: ps) (st' :: ps).
              StateTokenI st
@@ -109,10 +110,10 @@
   -> (forall (st :: ps) s.
              ActiveState st
           => StateToken st
-          -> CBOR.Decoder s (SomeMessage st))
+          -> CBOR.Decoder s (f st))
   -- ^ cbor decoder
 
-  -> Codec ps CBOR.DeserialiseFailure m LBS.ByteString
+  -> CodecF ps CBOR.DeserialiseFailure m f LBS.ByteString
 mkCodecCborLazyBS  cborMsgEncode cborMsgDecode =
     Codec {
       encode = \msg  -> convertCborEncoder cborMsgEncode msg,
@@ -126,10 +127,11 @@
       . cborEncode
 
     convertCborDecoder
-      :: (forall s. CBOR.Decoder s a)
-      -> m (DecodeStep LBS.ByteString CBOR.DeserialiseFailure m a)
+      :: (forall s. CBOR.Decoder s (f a))
+      -> m (DecodeStep LBS.ByteString CBOR.DeserialiseFailure m (f a))
     convertCborDecoder cborDecode =
         convertCborDecoderLBS cborDecode stToIO
+
 
 convertCborDecoderLBS
   :: forall s m a. Monad m
diff --git a/examples/Network/TypedProtocol/ReqResp/Codec.hs b/examples/Network/TypedProtocol/ReqResp/Codec.hs
--- a/examples/Network/TypedProtocol/ReqResp/Codec.hs
+++ b/examples/Network/TypedProtocol/ReqResp/Codec.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE BlockArguments #-}
+
 module Network.TypedProtocol.ReqResp.Codec where
 
 import Network.TypedProtocol.Codec
@@ -41,6 +43,68 @@
 
           (_       , _     ) -> DecodeFail failure
             where failure = CodecFailure ("unexpected server message: " ++ str)
+
+
+data WithBytes a = WithBytes {
+    bytes   :: String,
+    message :: a
+  }
+  deriving (Show, Eq)
+
+mkWithBytes :: Show a => a -> WithBytes a
+mkWithBytes message = WithBytes { bytes = show message, message }
+
+
+anncodecReqResp ::
+    forall req resp m
+  .  (Monad m, Show req, Show resp, Read req, Read resp)
+  => AnnotatedCodec (ReqResp (WithBytes req) (WithBytes resp)) CodecFailure m String
+anncodecReqResp =
+      Codec{encode, decode}
+  where
+    encode :: forall req' resp'
+                     (st  :: ReqResp (WithBytes req') (WithBytes resp'))
+                     (st' :: ReqResp (WithBytes req') (WithBytes resp'))
+           .  ( Show req'
+              , Show resp'
+              )
+           => Message (ReqResp (WithBytes req') (WithBytes resp')) st st'
+           -> String
+    -- NOTE: we're not using 'Show (Message ...)' instance.  If `req ~ Int`,
+    -- then negative numbers will be surrounded with braces (e.g. @"(-1)"@) and
+    -- the `Read` type class doesn't have a way to see that brackets were consumed
+    -- from the input string.
+    encode (MsgReq WithBytes { message })
+      = "MsgReq " ++ show message ++ "\n"
+    encode (MsgResp WithBytes { message })
+      = "MsgResp " ++ show message ++ "\n"
+    encode MsgDone
+      = "MsgDone" ++ "\n"
+
+    decode :: forall req' resp' m'
+                     (st :: ReqResp (WithBytes req') (WithBytes resp'))
+           .  (Monad m', Read req', Read resp', ActiveState st)
+           => StateToken st
+           -> m' (DecodeStep String CodecFailure m' (Annotator String st))
+    decode stok =
+      decodeTerminatedFrame '\n' $ \str trailing ->
+        case (stok, break (==' ') str) of
+          (SingIdle, ("MsgReq", str'))
+             | Just req <- readMaybe @req' str'
+            -> DecodeDone (Annotator \str'' ->
+                           let used = init $ drop 7 str'' in
+                           SomeMessage (MsgReq (WithBytes used req))) trailing
+          (SingIdle, ("MsgDone", ""))
+            -> DecodeDone (Annotator \_str'' -> SomeMessage MsgDone) trailing
+          (SingBusy, ("MsgResp", str'))
+            | Just resp <- readMaybe @resp' str'
+            -> DecodeDone (Annotator \str'' ->
+                           let used = init $ drop 8 str'' in
+                           SomeMessage (MsgResp (WithBytes used resp))) trailing
+
+          (_       , _     ) -> DecodeFail failure
+            where failure = CodecFailure ("unexpected server message: " ++ str)
+
 
 
 codecReqRespId ::
diff --git a/properties/Network/TypedProtocol/Codec/Properties.hs b/properties/Network/TypedProtocol/Codec/Properties.hs
new file mode 100644
--- /dev/null
+++ b/properties/Network/TypedProtocol/Codec/Properties.hs
@@ -0,0 +1,569 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+
+module Network.TypedProtocol.Codec.Properties
+  ( -- * Codec Properties
+    prop_codecM
+  , prop_codec
+  , prop_codec_splitsM
+  , prop_codec_splits
+  , prop_codec_binary_compatM
+  , prop_codec_binary_compat
+  , prop_codecs_compatM
+  , prop_codecs_compat
+    -- ** AnnotatedCodec Properties
+  , prop_anncodecM
+  , prop_anncodec
+  , prop_anncodec_splitsM
+  , prop_anncodec_splits
+  , prop_anncodec_binary_compatM
+  , prop_anncodec_binary_compat
+  , prop_anncodecs_compatM
+  , prop_anncodecs_compat
+    -- ** CodecF Properties
+  , prop_codecFM
+  , prop_codecF
+  , prop_codecF_splitsM
+  , prop_codecF_splits
+  , prop_codecF_binary_compatM
+  , prop_codecF_binary_compat
+  , prop_codecsF_compatM
+  , prop_codecsF_compat
+    -- * Re-exports
+  , AnyMessage (..)
+  , SomeState (..)
+  ) where
+
+import Network.TypedProtocol.Codec
+import Network.TypedProtocol.Core
+
+import Test.QuickCheck
+
+
+-- | The 'CodecF' round-trip property: decode after encode gives the same
+-- message. Every codec must satisfy this property.
+--
+prop_codecFM
+  :: forall ps failure m f bytes.
+     ( Monad m
+     , Eq (AnyMessage ps)
+     , Show (AnyMessage ps)
+     , Show failure
+     )
+  => (forall (st :: ps). f st -> bytes -> SomeMessage st)
+  -- ^ extract message from the functor
+  -> CodecF ps failure m f bytes
+  -- ^ annotated codec
+  -> AnyMessage ps
+  -- ^ some message
+  -> m Property
+prop_codecFM runF Codec {encode, decode} (AnyMessage (msg :: Message ps st st')) = do
+    let bytes = encode msg
+    r <- decode stateToken >>= runDecoder [bytes]
+    return $ case r :: Either failure (f st) of
+      Right f -> case runF f bytes of
+        SomeMessage msg' ->
+          AnyMessage msg' === AnyMessage msg
+      Left err -> counterexample (show err) False
+
+
+-- | The 'Codec' round-trip property: decode after encode gives the same
+-- message. Every codec must satisfy this property.
+--
+prop_codecM
+  :: forall ps failure m bytes.
+     ( Monad m
+     , Eq (AnyMessage ps)
+     , Show (AnyMessage ps)
+     , Show failure
+     )
+  => Codec ps failure m bytes
+  -- ^ codec
+  -> AnyMessage ps
+  -- ^ some message
+  -> m Property
+  -- ^ returns 'True' iff round trip returns the exact same message
+prop_codecM = prop_codecFM const
+
+-- | The 'Codec' round-trip property: decode after encode gives the same
+-- message. Every codec must satisfy this property.
+--
+prop_anncodecM
+  :: forall ps failure m bytes.
+     ( Monad m
+     , Eq (AnyMessage ps)
+     , Show (AnyMessage ps)
+     , Show failure
+     )
+  => AnnotatedCodec ps failure m bytes
+  -- ^ annotated codec
+  -> AnyMessage ps
+  -- ^ some message
+  -> m Property
+prop_anncodecM = prop_codecFM runAnnotator
+
+
+-- | The 'CodecF' round-trip property in a pure monad.
+--
+prop_codecF
+  :: forall ps failure m f bytes.
+     ( Monad m
+     , Eq (AnyMessage ps)
+     , Show (AnyMessage ps)
+     , Show failure
+     )
+  => (forall (st :: ps). f st -> bytes -> SomeMessage st)
+  -> (forall a. m a -> a)
+  -> CodecF ps failure m f bytes
+  -> AnyMessage ps
+  -> Property
+prop_codecF runF runM codec msg = runM (prop_codecFM runF codec msg)
+
+-- | The 'Codec' round-trip property in a pure monad.
+--
+prop_codec
+  :: forall ps failure m bytes.
+     ( Monad m
+     , Eq (AnyMessage ps)
+     , Show (AnyMessage ps)
+     , Show failure
+     )
+  => (forall a. m a -> a)
+  -> Codec ps failure m bytes
+  -> AnyMessage ps
+  -> Property
+prop_codec = prop_codecF const
+
+
+-- | The 'Codec' round-trip property in a pure monad.
+--
+-- NOTE: when a message is annotated with bytes (e.g. `WithBytes` in
+-- `Network.TypedProtocol.ReqResp.Codec.anncodecReqResp`), this property will
+-- assess that the decoded bytes are equal to the supplied bytes with
+-- `msg :: AnyMessage ps`.  It is important to use the bytes in `WithBytes` when
+-- encoding the `msg`.  Verifying this property is especially important if the
+-- bytes are used to check a cryptographic signature, when the exact same bytes
+-- received from the network must be used.
+--
+prop_anncodec
+  :: forall ps failure m bytes.
+    ( Monad m
+    , Eq (AnyMessage ps)
+    , Show (AnyMessage ps)
+    , Show failure
+    )
+  => (forall a. m a -> a)
+  -> AnnotatedCodec ps failure m bytes
+  -> AnyMessage ps
+  -> Property
+prop_anncodec = prop_codecF runAnnotator
+
+
+-- | A more general version of 'prop_codec_splitsM' for 'CodecF'.
+--
+prop_codecF_splitsM
+  :: forall ps failure m f bytes.
+     ( Monad m
+     , Eq (AnyMessage ps)
+     , Show (AnyMessage ps)
+     , Show failure
+     , Monoid bytes
+     )
+  => (forall (st :: ps). f st -> bytes -> SomeMessage st)
+  -> (bytes -> [[bytes]])
+  -- ^ alternative re-chunkings of serialised form
+  -> CodecF ps failure m f bytes
+  -> AnyMessage ps
+  -> m Property
+prop_codecF_splitsM runF splits
+                    Codec {encode, decode} (AnyMessage (msg :: Message ps st st')) = do
+    property . foldMap Every <$> sequence
+      [ do r <- decode stateToken >>= runDecoder bytes'
+           case r :: Either failure (f st) of
+             Right f -> case runF f (mconcat bytes') of
+               SomeMessage msg' ->
+                 return $! AnyMessage msg' === AnyMessage msg
+             Left err -> return $ counterexample (show err) False
+
+      | let bytes = encode msg
+      , bytes' <- splits bytes ]
+
+
+-- | A variant on the codec round-trip property: given the encoding of a
+-- message, check that decode always gives the same result irrespective
+-- of how the chunks of input are fed to the incremental decoder.
+--
+-- This property guards against boundary errors in incremental decoders.
+-- It is not necessary to check this for every message type, just for each
+-- generic codec construction. For example given some binary serialisation
+-- library one would write a generic adaptor to the codec interface. This
+-- adaptor has to deal with the incremental decoding and this is what needs
+-- to be checked.
+--
+prop_codec_splitsM
+  :: forall ps failure m bytes.
+     ( Monad m
+     , Eq (AnyMessage ps)
+     , Show (AnyMessage ps)
+     , Show failure
+     , Monoid bytes
+     )
+  => (bytes -> [[bytes]])
+  -- ^ alternative re-chunkings of serialised form
+  -> Codec ps failure m bytes
+  -> AnyMessage ps
+  -> m Property
+prop_codec_splitsM = prop_codecF_splitsM const
+
+-- | A variant of 'prop_codec_splitsM' for 'AnnotatedCodec'.
+--
+prop_anncodec_splitsM
+  :: forall ps failure m bytes.
+     ( Monad m
+     , Eq (AnyMessage ps)
+     , Show (AnyMessage ps)
+     , Show failure
+     , Monoid bytes
+     )
+  => (bytes -> [[bytes]])
+  -- ^ alternative re-chunkings of serialised form
+  -> AnnotatedCodec ps failure m bytes
+  -> AnyMessage ps
+  -> m Property
+prop_anncodec_splitsM = prop_codecF_splitsM runAnnotator
+
+
+-- | A more general version of 'prop_codec_splits' for 'CodecF'.
+--
+prop_codecF_splits
+  :: forall ps failure m f bytes.
+     ( Monad m
+     , Eq (AnyMessage ps)
+     , Show (AnyMessage ps)
+     , Show failure
+     , Monoid bytes
+     )
+  => (forall (st :: ps). f st -> bytes -> SomeMessage st)
+  -> (bytes -> [[bytes]])
+  -- ^ alternative re-chunkings of serialised form
+  -> (forall a. m a -> a)
+  -> CodecF ps failure m f bytes
+  -> AnyMessage ps
+  -> Property
+prop_codecF_splits runF splits runM codec msg =
+    runM $ prop_codecF_splitsM runF splits codec msg
+
+-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@.
+--
+prop_codec_splits
+  :: forall ps failure m bytes.
+     ( Monad m
+     , Eq (AnyMessage ps)
+     , Show (AnyMessage ps)
+     , Show failure
+     , Monoid bytes
+     )
+  => (bytes -> [[bytes]])
+  -- ^ alternative re-chunkings of serialised form
+  -> (forall a. m a -> a)
+  -> Codec ps failure m bytes
+  -> AnyMessage ps
+  -> Property
+prop_codec_splits = prop_codecF_splits const
+
+-- | Like 'prop_codec_splits' but for 'AnnotatorCodec'.
+prop_anncodec_splits
+  :: forall ps failure m bytes.
+     ( Monad m
+     , Eq (AnyMessage ps)
+     , Show (AnyMessage ps)
+     , Show failure
+     , Monoid bytes
+     )
+  => (bytes -> [[bytes]])
+  -- ^ alternative re-chunkings of serialised form
+  -> (forall a. m a -> a)
+  -> AnnotatedCodec ps failure m bytes
+  -> AnyMessage ps
+  -> Property
+prop_anncodec_splits = prop_codecF_splits runAnnotator
+
+-- | A more general version of 'prop_codec_binary_compatM' for 'CodecF'.
+--
+prop_codecF_binary_compatM
+  :: forall psA psB failure m fA fB bytes.
+     ( Monad m
+     , Eq (AnyMessage psA)
+     , Show (AnyMessage psA)
+     , Show failure
+     )
+  => (forall (st :: psA). fA st -> bytes -> SomeMessage st)
+  -> (forall (st :: psB). fB st -> bytes -> SomeMessage st)
+  -> CodecF psA failure m fA bytes
+  -> CodecF psB failure m fB bytes
+  -> (forall (stA :: psA). ActiveState stA => StateToken stA -> SomeState psB)
+     -- ^ the states of A map directly to states of B.
+  -> AnyMessage psA
+  -> m Property
+prop_codecF_binary_compatM
+    runFA runFB codecA codecB stokEq
+    (AnyMessage (msgA :: Message psA stA stA')) =
+  let stokA :: StateToken stA
+      stokA = stateToken
+  in case stokEq stokA of
+    SomeState (stokB :: StateToken stB) -> do
+      -- 1.
+      let bytesA = encode codecA msgA
+      -- 2.
+      r1 <- decode codecB stokB >>= runDecoder [bytesA]
+      case r1 :: Either failure (fB stB) of
+        Left err   -> return $ counterexample (show err) False
+        Right fB ->
+          case runFB fB bytesA of
+            (SomeMessage msgB) -> do
+              -- 3.
+              let bytesB = encode codecB msgB
+              -- 4.
+              r2 <- decode codecA (stateToken :: StateToken stA) >>= runDecoder [bytesB]
+              case r2 :: Either failure (fA stA) of
+                Left err -> return $ counterexample (show err) False
+                Right fA ->
+                  case runFA fA bytesB of
+                    SomeMessage msgA' -> return $ AnyMessage msgA' === AnyMessage msgA
+
+-- | Binary compatibility of two protocols
+--
+-- We check the following property:
+--
+-- 1. Using codec A, we encode a message of protocol @psA@ to @bytes@.
+--
+-- 2. When we decode those @bytes@ using codec B, we get a message of protocol
+-- @ps@B.
+--
+-- 3. When we encode that message again using codec B, we get @bytes@.
+--
+-- 4. When we decode those @bytes@ using codec A, we get the original message
+-- again.
+prop_codec_binary_compatM
+  :: forall psA psB failure m bytes.
+     ( Monad m
+     , Eq (AnyMessage psA)
+     , Show (AnyMessage psA)
+     , Show failure
+     )
+  => Codec psA failure m bytes
+  -> Codec psB failure m bytes
+  -> (forall (stA :: psA). ActiveState stA => StateToken stA -> SomeState psB)
+     -- ^ the states of A map directly to states of B.
+  -> AnyMessage psA
+  -> m Property
+prop_codec_binary_compatM = prop_codecF_binary_compatM const const
+
+
+-- | A version of 'prop_codec_binary_compatM' for 'AnnotatedCodec'.
+--
+prop_anncodec_binary_compatM
+  :: forall psA psB failure m bytes.
+     ( Monad m
+     , Eq (AnyMessage psA)
+     , Show (AnyMessage psA)
+     , Show failure
+     )
+  => AnnotatedCodec psA failure m bytes
+  -> AnnotatedCodec psB failure m bytes
+  -> (forall (stA :: psA). ActiveState stA => StateToken stA -> SomeState psB)
+     -- ^ the states of A map directly to states of B.
+  -> AnyMessage psA
+  -> m Property
+prop_anncodec_binary_compatM = prop_codecF_binary_compatM runAnnotator runAnnotator
+
+
+-- | A more general version of 'prop_codec_binary_compat' for 'CodecF'.
+--
+prop_codecF_binary_compat
+  :: forall psA psB failure m fA fB bytes.
+     ( Monad m
+     , Eq (AnyMessage psA)
+     , Show (AnyMessage psA)
+     , Show failure
+     )
+  => (forall (st :: psA). fA st -> bytes -> SomeMessage st)
+  -> (forall (st :: psB). fB st -> bytes -> SomeMessage st)
+  -> (forall a. m a -> a)
+  -> CodecF psA failure m fA bytes
+  -> CodecF psB failure m fB bytes
+  -> (forall (stA :: psA). StateToken stA -> SomeState psB)
+     -- ^ the states of A map directly to states of B.
+  -> AnyMessage psA
+  -> Property
+prop_codecF_binary_compat runFA runFB runM codecA codecB stokEq msg =
+    runM $ prop_codecF_binary_compatM runFA runFB codecA codecB stokEq msg
+
+
+-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@.
+--
+prop_codec_binary_compat
+  :: forall psA psB failure m bytes.
+     ( Monad m
+     , Eq (AnyMessage psA)
+     , Show (AnyMessage psA)
+     , Show failure
+     )
+  => (forall a. m a -> a)
+  -> Codec psA failure m bytes
+  -> Codec psB failure m bytes
+  -> (forall (stA :: psA). StateToken stA -> SomeState psB)
+     -- ^ the states of A map directly to states of B.
+  -> AnyMessage psA
+  -> Property
+prop_codec_binary_compat =
+     prop_codecF_binary_compat const const
+
+-- | A 'prop_codec_binary_compat' version for 'AnnotatedCodec'.
+--
+prop_anncodec_binary_compat
+  :: forall psA psB failure m bytes.
+     ( Monad m
+     , Eq (AnyMessage psA)
+     , Show (AnyMessage psA)
+     , Show failure
+     )
+  => (forall a. m a -> a)
+  -> AnnotatedCodec psA failure m bytes
+  -> AnnotatedCodec psB failure m bytes
+  -> (forall (stA :: psA). StateToken stA -> SomeState psB)
+     -- ^ the states of A map directly to states of B.
+  -> AnyMessage psA
+  -> Property
+prop_anncodec_binary_compat runM codecA codecB stokEq msgA =
+     runM $ prop_anncodec_binary_compatM codecA codecB stokEq msgA
+
+
+-- | A more general version of 'prop_codecs_compatM' for 'CodecF'.
+--
+prop_codecsF_compatM
+  :: forall ps failure m f bytes.
+     ( Monad m
+     , Eq (AnyMessage ps)
+     , Show (AnyMessage ps)
+     , Show failure
+     , forall a. Monoid a => Monoid (m a)
+     )
+  => (forall (st :: ps). f st -> bytes -> SomeMessage st)
+  -> CodecF ps failure m f bytes
+  -- ^ first codec
+  -> CodecF ps failure m f bytes
+  -- ^ second codec
+  -> AnyMessage ps
+  -- ^ some message
+  -> m Property
+prop_codecsF_compatM runF codecA codecB
+                    (AnyMessage (msg :: Message ps st st')) =
+
+    property
+           <$> do let bytes = encode codecA msg
+                  r <- decode codecB (stateToken :: StateToken st) >>= runDecoder [bytes]
+                  case r :: Either failure (f st) of
+                    Right f -> case runF f bytes of
+                      SomeMessage msg' -> return $! Every $ AnyMessage msg' === AnyMessage msg
+                    Left err           -> return $! Every $ counterexample (show err) False
+
+           <>  do let bytes = encode codecB msg
+                  r <- decode codecA (stateToken :: StateToken st) >>= runDecoder [bytes]
+                  case r :: Either failure (f st) of
+                    Right f -> case runF f bytes of
+                      SomeMessage msg' -> return $! Every $ AnyMessage msg' === AnyMessage msg
+                    Left err           -> return $! Every $ counterexample (show err) False
+
+-- | Compatibility between two codecs of the same protocol.  Encode a message
+-- with one codec and decode it with the other one, then compare if the result
+-- is the same as initial message.
+--
+prop_codecs_compatM
+  :: forall ps failure m bytes.
+     ( Monad m
+     , Eq (AnyMessage ps)
+     , Show (AnyMessage ps)
+     , Show failure
+     , forall a. Monoid a => Monoid (m a)
+     )
+  => Codec ps failure m bytes
+  -- ^ first codec
+  -> Codec ps failure m bytes
+  -- ^ second codec
+  -> AnyMessage ps
+  -- ^ some message
+  -> m Property
+prop_codecs_compatM = prop_codecsF_compatM const
+
+-- | A version of 'prop_codec_compatM' for 'AnnotatedCodec'.
+--
+prop_anncodecs_compatM
+  :: forall ps failure m bytes.
+     ( Monad m
+     , Eq (AnyMessage ps)
+     , Show (AnyMessage ps)
+     , Show failure
+     , forall a. Monoid a => Monoid (m a)
+     )
+  => AnnotatedCodec ps failure m bytes
+  -- ^ first codec
+  -> AnnotatedCodec ps failure m bytes
+  -- ^ second codec
+  -> AnyMessage ps
+  -- ^ some message
+  -> m Property
+prop_anncodecs_compatM = prop_codecsF_compatM runAnnotator
+
+
+-- | A more general version of 'prop_codecs_compat' for 'CodecF'.
+--
+prop_codecsF_compat
+  :: forall ps failure m f bytes.
+     ( Monad m
+     , Eq (AnyMessage ps)
+     , Show (AnyMessage ps)
+     , Show failure
+     , forall a. Monoid a => Monoid (m a)
+     )
+  => (forall (st :: ps). f st -> bytes -> SomeMessage st)
+  -> (forall a. m a -> a)
+  -> CodecF ps failure m f bytes
+  -> CodecF ps failure m f bytes
+  -> AnyMessage ps
+  -> Property
+prop_codecsF_compat runF runM codecA codecB msg =
+    runM $ prop_codecsF_compatM runF codecA codecB msg
+
+-- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@.
+--
+prop_codecs_compat
+  :: forall ps failure m bytes.
+     ( Monad m
+     , Eq (AnyMessage ps)
+     , Show (AnyMessage ps)
+     , Show failure
+     , forall a. Monoid a => Monoid (m a)
+     )
+  => (forall a. m a -> a)
+  -> Codec ps failure m bytes
+  -> Codec ps failure m bytes
+  -> AnyMessage ps
+  -> Property
+prop_codecs_compat = prop_codecsF_compat const
+
+-- | A version of 'prop_codecs_compat' for 'AnnotatedCodec'.
+--
+prop_anncodecs_compat
+  :: forall ps failure m bytes.
+     ( Monad m
+     , Eq (AnyMessage ps)
+     , Show (AnyMessage ps)
+     , Show failure
+     , forall a. Monoid a => Monoid (m a)
+     )
+  => (forall a. m a -> a)
+  -> AnnotatedCodec ps failure m bytes
+  -> AnnotatedCodec ps failure m bytes
+  -> AnyMessage ps
+  -> Property
+prop_anncodecs_compat = prop_codecsF_compat runAnnotator
diff --git a/properties/Network/TypedProtocol/Stateful/Codec/Properties.hs b/properties/Network/TypedProtocol/Stateful/Codec/Properties.hs
new file mode 100644
--- /dev/null
+++ b/properties/Network/TypedProtocol/Stateful/Codec/Properties.hs
@@ -0,0 +1,150 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+
+module Network.TypedProtocol.Stateful.Codec.Properties
+  ( prop_codecM
+  , prop_codec
+  , prop_codec_splitsM
+  , prop_codec_splits
+  , prop_codecs_compatM
+  , prop_codecs_compat
+  ) where
+
+import Network.TypedProtocol.Core
+import Network.TypedProtocol.Stateful.Codec
+
+import Test.QuickCheck
+
+
+-- | The 'Codec' round-trip property: decode after encode gives the same
+-- message. Every codec must satisfy this property.
+--
+prop_codecM
+  :: forall ps failure f m bytes.
+     ( Monad m
+     , Eq (AnyMessage ps f)
+     , Show (AnyMessage ps f)
+     , Show failure
+     )
+  => Codec ps failure f m bytes
+  -> AnyMessage ps f
+  -> m Property
+prop_codecM Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do
+    r <- decode (stateToken :: StateToken st) f >>= runDecoder [encode f msg]
+    case r :: Either failure (SomeMessage st) of
+      Right (SomeMessage msg') -> return $ AnyMessage f msg' === a
+      Left err                 -> return $ counterexample (show err) False
+
+-- | The 'Codec' round-trip property in a pure monad.
+--
+prop_codec
+  :: forall ps failure f m bytes.
+     ( Monad m
+     , Eq (AnyMessage ps f)
+     , Show (AnyMessage ps f)
+     , Show failure
+     )
+  => (forall a. m a -> a)
+  -> Codec ps failure f m bytes
+  -> AnyMessage ps f
+  -> Property
+prop_codec runM codec msg =
+    runM (prop_codecM codec msg)
+
+
+-- | A variant on the codec round-trip property: given the encoding of a
+-- message, check that decode always gives the same result irrespective
+-- of how the chunks of input are fed to the incremental decoder.
+--
+-- This property guards against boundary errors in incremental decoders.
+-- It is not necessary to check this for every message type, just for each
+-- generic codec construction. For example given some binary serialisation
+-- library one would write a generic adaptor to the codec interface. This
+-- adaptor has to deal with the incremental decoding and this is what needs
+-- to be checked.
+--
+prop_codec_splitsM
+  :: forall ps failure f m bytes.
+     ( Monad m
+     , Eq (AnyMessage ps f)
+     , Show (AnyMessage ps f)
+     , Show failure
+     )
+  => (bytes -> [[bytes]])   -- ^ alternative re-chunkings of serialised form
+  -> Codec ps failure f m bytes
+  -> AnyMessage ps f
+  -> m Property
+prop_codec_splitsM splits
+                   Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do
+    property . foldMap Every <$> sequence
+      [ do r <- decode (stateToken :: StateToken st) f >>= runDecoder bytes'
+           case r :: Either failure (SomeMessage st) of
+             Right (SomeMessage msg') -> return $ AnyMessage f msg' === a
+             Left err                 -> return $ counterexample (show err) False
+
+      | let bytes = encode f msg
+      , bytes' <- splits bytes ]
+
+
+-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@.
+--
+prop_codec_splits
+  :: forall ps failure f m bytes.
+     ( Monad m
+     , Eq (AnyMessage ps f)
+     , Show (AnyMessage ps f)
+     , Show failure
+     )
+  => (bytes -> [[bytes]])
+  -> (forall a. m a -> a)
+  -> Codec ps failure f m bytes
+  -> AnyMessage ps f
+  -> Property
+prop_codec_splits splits runM codec msg =
+    runM $ prop_codec_splitsM splits codec msg
+
+
+-- | Compatibility between two codecs of the same protocol.  Encode a message
+-- with one codec and decode it with the other one, then compare if the result
+-- is the same as initial message.
+--
+prop_codecs_compatM
+  :: forall ps failure f m bytes.
+     ( Monad m
+     , Eq (AnyMessage ps f)
+     , Show (AnyMessage ps f)
+     , forall a. Monoid a => Monoid (m a)
+     , Show failure
+     )
+  => Codec ps failure f m bytes
+  -> Codec ps failure f m bytes
+  -> AnyMessage ps f
+  -> m Property
+prop_codecs_compatM codecA codecB
+                    a@(AnyMessage f (msg :: Message ps st st')) =
+    property
+      <$> do r <- decode codecB (stateToken :: StateToken st) f >>= runDecoder [encode codecA f msg]
+             case r :: Either failure (SomeMessage st) of
+               Right (SomeMessage msg') -> return $ Every $ AnyMessage f msg' === a
+               Left err                 -> return $ Every $ counterexample (show err) False
+      <> do r <- decode codecA (stateToken :: StateToken st) f >>= runDecoder [encode codecB f msg]
+            case r :: Either failure (SomeMessage st) of
+              Right (SomeMessage msg') -> return $ Every $ AnyMessage f msg' == a
+              Left _                   -> return $ Every False
+
+-- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@.
+--
+prop_codecs_compat
+  :: forall ps failure f m bytes.
+     ( Monad m
+     , Eq (AnyMessage ps f)
+     , Show (AnyMessage ps f)
+     , forall a. Monoid a => Monoid (m a)
+     , Show failure
+     )
+  => (forall a. m a -> a)
+  -> Codec ps failure f m bytes
+  -> Codec ps failure f m bytes
+  -> AnyMessage ps f
+  -> Property
+prop_codecs_compat run codecA codecB msg =
+    run $ prop_codecs_compatM codecA codecB msg
diff --git a/src/Network/TypedProtocol/Codec.hs b/src/Network/TypedProtocol/Codec.hs
--- a/src/Network/TypedProtocol/Codec.hs
+++ b/src/Network/TypedProtocol/Codec.hs
@@ -8,7 +8,12 @@
 module Network.TypedProtocol.Codec
   ( -- * Defining and using Codecs
     -- ** Codec type
-    Codec (..)
+    CodecF (..)
+  , Codec
+  , Annotator (..)
+  , AnnotatedCodec
+  , hoistAnnotation
+  , unAnnotateCodec
   , hoistCodec
   , isoCodec
   , mapFailureCodec
@@ -36,21 +41,14 @@
     -- * CodecFailure
   , CodecFailure (..)
     -- * Testing codec properties
+    -- ** Codec
   , AnyMessage (AnyMessage, AnyMessageAndAgency)
-  , prop_codecM
-  , prop_codec
-  , prop_codec_splitsM
-  , prop_codec_splits
-  , prop_codec_binary_compatM
-  , prop_codec_binary_compat
-  , prop_codecs_compatM
-  , prop_codecs_compat
+    -- ** SomeState
   , SomeState (..)
   ) where
 
 import Control.Exception (Exception)
 import Data.Kind (Type)
-import Data.Monoid (All (..))
 
 import Network.TypedProtocol.Core
 import Network.TypedProtocol.Driver (SomeMessage (..))
@@ -66,10 +64,21 @@
 -- * The protocol
 -- * the type of decoding failures
 -- * the monad in which the decoder runs
--- * the type of the encoded data (typically strings or bytes)
+-- * a functor which wraps the decoder result, e.g. `SomeMessage` or `Annotator`.
+-- * the type of the encoded data (typically strings or bytes, or
+--   `AnyMessage` for testing purposes with no codec overhead).
 --
 -- A codec consists of a message encoder and a decoder.
 --
+-- The `CodecF` type comes with two useful type aliases:
+-- * `Codec`          - which can decode protocol messages
+-- * `AnnotatedCodec` - which also has access to bytes which were fed to the
+--                      codec when decoding a message.
+--
+-- `AnnotatedCodec` is useful if one wants to decode data structures and retain
+-- their CBOR encoding (`decodeWithByteSpan` from `cborg` can be used for that
+-- purpose).
+--
 -- The encoder is supplied both with the message to encode and the current
 -- protocol state (matching the message). The protocol state can be either
 -- a client or server state, but for either peer role it is a protocol state
@@ -123,31 +132,77 @@
 -- This toy example format uses newlines @\n@ as a framing format. See
 -- 'DecodeStep' for suggestions on how to use it for more realistic formats.
 --
-data Codec ps failure m bytes = Codec {
+data CodecF ps failure m (f :: ps -> Type) bytes = Codec {
        encode :: forall (st :: ps) (st' :: ps).
                  StateTokenI st
               => ActiveState st
-              -- evidence that the state 'st' is active
               => Message ps st st'
-              -- message to encode
               -> bytes,
+       -- ^ encode a message into `bytes`
 
        decode :: forall (st :: ps).
                  ActiveState st
               => StateToken st
               -- evidence for an active state
-              -> m (DecodeStep bytes failure m (SomeMessage st))
+              -> m (DecodeStep bytes failure m (f st))
+       -- ^ decode a message knowing that the current state is `st`
      }
--- TODO: input-output-hk/typed-protocols#57
 
 -- | Change functor in which the codec is running.
 --
+-- | The type of a standard `Codec` for `typed-protocols`.
+--
+type Codec ps failure m bytes = CodecF ps failure m SomeMessage bytes
+
+-- | A continuation for a decoder which is fed with whole bytes that were used
+-- to parse the message.
+--
+newtype Annotator bytes st = Annotator { runAnnotator :: bytes -> SomeMessage st }
+
+-- | Codec which has access to bytes received from the network to annotate
+-- decoded structure.
+--
+-- AnnotatedCodec works in two stages.  First it is decoding the structure as
+-- bytes are received from the network, like a `Codec` does.  The codec returns
+-- a continuation `Annotator` which is fed with all bytes used to parse the
+-- message.  It is the driver which is responsible for passing bytes which were
+-- fed to the incremental codec.
+--
+type AnnotatedCodec ps failure m bytes = CodecF ps failure m (Annotator bytes) bytes
+
+
+-- | Transform annotation.
+--
+hoistAnnotation :: forall ps failure m f g bytes.
+                   Functor m
+                => (forall st. f st -> g st)
+                -> CodecF ps failure m f bytes
+                -> CodecF ps failure m g bytes
+hoistAnnotation nat codec@Codec { decode } = codec { decode = decode' }
+  where
+    decode' :: forall (st :: ps).
+               ActiveState st
+            => StateToken st
+            -> m (DecodeStep bytes failure m (g st))
+    decode' tok = fmap nat <$> decode tok
+
+
+-- | Remove annotation. It is only safe if the `Annotator` treats empty input
+-- in a safe way.
+--
+unAnnotateCodec :: forall ps failure m bytes.
+                   (Functor m, Monoid bytes)
+                => AnnotatedCodec ps failure m bytes
+                -> Codec ps failure m bytes
+unAnnotateCodec = hoistAnnotation (($ mempty) . runAnnotator)
+
+
 hoistCodec
   :: ( Functor n )
   => (forall x . m x -> n x)
   -- ^ a natural transformation
-  -> Codec ps failure m bytes
-  -> Codec ps failure n bytes
+  -> CodecF ps failure m f bytes
+  -> CodecF ps failure n f bytes
 hoistCodec nat codec = codec
   { decode = fmap (hoistDecodeStep nat) . nat . decode codec
   }
@@ -159,9 +214,9 @@
          -- ^ map from 'bytes' to `bytes'`
          -> (bytes' -> bytes)
          -- ^ its inverse
-         -> Codec ps failure m bytes
+         -> CodecF ps failure m f bytes
          -- ^ codec
-         -> Codec ps failure m bytes'
+         -> CodecF ps failure m f bytes'
 isoCodec f finv Codec {encode, decode} = Codec {
       encode = \msg -> f $ encode msg,
       decode = \tok -> isoDecodeStep f finv <$> decode tok
@@ -173,8 +228,8 @@
   :: Functor m
   => (failure -> failure')
   -- ^ a function to apply to failure
-  -> Codec ps failure  m bytes
-  -> Codec ps failure' m bytes
+  -> CodecF ps failure  m f bytes
+  -> CodecF ps failure' m f bytes
 mapFailureCodec f Codec {encode, decode} = Codec {
     encode = encode,
     decode = \tok -> mapFailureDecodeStep f <$> decode tok
@@ -207,9 +262,11 @@
     -- @'fail'@ or was not provided enough input.
   | DecodeFail failure
 
+deriving instance Functor m => Functor (DecodeStep bytes failure m)
 
 -- | Change bytes of 'DecodeStep'.
 --
+
 isoDecodeStep
   :: Functor m
   => (bytes -> bytes')
@@ -322,8 +379,10 @@
 -- requires @UndecidableInstances@ and @QuantifiedConstraints@.
 instance (forall (st :: ps) (st' :: ps). Show (Message ps st st'))
       => Show (AnyMessage ps) where
-  show (AnyMessage (msg :: Message ps st st')) =
-    "AnyMessage " ++ show msg
+  showsPrec d (AnyMessage (msg :: Message ps st st')) =
+      showParen (d > app_prec) (showString "AnyMessage " . showsPrec (app_prec + 1) msg)
+    where
+      app_prec = 10
 
 
 -- | A convenient pattern synonym which unwrap 'AnyMessage' giving both the
@@ -346,85 +405,6 @@
 getAgency msg = (msg, stateToken)
 
 
--- | The 'Codec' round-trip property: decode after encode gives the same
--- message. Every codec must satisfy this property.
---
-prop_codecM
-  :: forall ps failure m bytes.
-     ( Monad m
-     , Eq (AnyMessage ps)
-     )
-  => Codec ps failure m bytes
-  -- ^ codec
-  -> AnyMessage ps
-  -- ^ some message
-  -> m Bool
-  -- ^ returns 'True' iff round trip returns the exact same message
-prop_codecM Codec {encode, decode} (AnyMessage (msg :: Message ps st st')) = do
-    r <- decode stateToken >>= runDecoder [encode msg]
-    case r :: Either failure (SomeMessage st) of
-      Right (SomeMessage msg') -> return $ AnyMessage msg' == AnyMessage msg
-      Left _                   -> return False
-
--- | The 'Codec' round-trip property in a pure monad.
---
-prop_codec
-  :: forall ps failure m bytes.
-     (Monad m, Eq (AnyMessage ps))
-  => (forall a. m a -> a)
-  -> Codec ps failure m bytes
-  -> AnyMessage ps
-  -> Bool
-prop_codec runM codec msg =
-    runM (prop_codecM codec msg)
-
-
--- | A variant on the codec round-trip property: given the encoding of a
--- message, check that decode always gives the same result irrespective
--- of how the chunks of input are fed to the incremental decoder.
---
--- This property guards against boundary errors in incremental decoders.
--- It is not necessary to check this for every message type, just for each
--- generic codec construction. For example given some binary serialisation
--- library one would write a generic adaptor to the codec interface. This
--- adaptor has to deal with the incremental decoding and this is what needs
--- to be checked.
---
-prop_codec_splitsM
-  :: forall ps failure m bytes.
-     (Monad m, Eq (AnyMessage ps))
-  => (bytes -> [[bytes]])
-  -- ^ alternative re-chunkings of serialised form
-  -> Codec ps failure m bytes
-  -> AnyMessage ps
-  -> m Bool
-prop_codec_splitsM splits
-                   Codec {encode, decode} (AnyMessage (msg :: Message ps st st')) = do
-    and <$> sequence
-      [ do r <- decode stateToken >>= runDecoder bytes'
-           case r :: Either failure (SomeMessage st) of
-             Right (SomeMessage msg') -> return $! AnyMessage msg' == AnyMessage msg
-             Left _                   -> return False
-
-      | let bytes = encode msg
-      , bytes' <- splits bytes ]
-
-
--- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@.
---
-prop_codec_splits
-  :: forall ps failure m bytes.
-     (Monad m, Eq (AnyMessage ps))
-  => (bytes -> [[bytes]])
-  -- ^ alternative re-chunkings of serialised form
-  -> (forall a. m a -> a)
-  -> Codec ps failure m bytes
-  -> AnyMessage ps
-  -> Bool
-prop_codec_splits splits runM codec msg =
-    runM $ prop_codec_splitsM splits codec msg
-
-
 -- | Auxiliary definition for 'prop_codec_binary_compatM'.
 --
 -- Used for the existential @st :: ps@ parameter when expressing that for each
@@ -437,110 +417,3 @@
     => StateToken st
     -- ^ state token for some active state 'st'
     -> SomeState ps
-
--- | Binary compatibility of two protocols
---
--- We check the following property:
---
--- 1. Using codec A, we encode a message of protocol @psA@ to @bytes@.
---
--- 2. When we decode those @bytes@ using codec B, we get a message of protocol
--- @ps@B.
---
--- 3. When we encode that message again using codec B, we get @bytes@.
---
--- 4. When we decode those @bytes@ using codec A, we get the original message
--- again.
-prop_codec_binary_compatM
-  :: forall psA psB failure m bytes.
-     ( Monad m
-     , Eq (AnyMessage psA)
-     )
-  => Codec psA failure m bytes
-  -> Codec psB failure m bytes
-  -> (forall (stA :: psA). ActiveState stA => StateToken stA -> SomeState psB)
-     -- ^ the states of A map directly to states of B.
-  -> AnyMessage psA
-  -> m Bool
-prop_codec_binary_compatM
-    codecA codecB stokEq
-    (AnyMessage (msgA :: Message psA stA stA')) =
-  let stokA :: StateToken stA
-      stokA = stateToken
-  in case stokEq stokA of
-    SomeState (stokB :: StateToken stB) -> do
-      -- 1.
-      let bytesA = encode codecA msgA
-      -- 2.
-      r1 <- decode codecB stokB >>= runDecoder [bytesA]
-      case r1 :: Either failure (SomeMessage stB) of
-        Left _     -> return False
-        Right (SomeMessage msgB) -> do
-          -- 3.
-          let bytesB = encode codecB msgB
-          -- 4.
-          r2 <- decode codecA (stateToken :: StateToken stA) >>= runDecoder [bytesB]
-          case r2 :: Either failure (SomeMessage stA) of
-            Left _                    -> return False
-            Right (SomeMessage msgA') -> return $ AnyMessage msgA' == AnyMessage msgA
-
--- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@.
-prop_codec_binary_compat
-  :: forall psA psB failure m bytes.
-     ( Monad m
-     , Eq (AnyMessage psA)
-     )
-  => (forall a. m a -> a)
-  -> Codec psA failure m bytes
-  -> Codec psB failure m bytes
-  -> (forall (stA :: psA). StateToken stA -> SomeState psB)
-     -- ^ the states of A map directly to states of B.
-  -> AnyMessage psA
-  -> Bool
-prop_codec_binary_compat runM codecA codecB stokEq msgA =
-     runM $ prop_codec_binary_compatM codecA codecB stokEq msgA
-
-
--- | Compatibility between two codecs of the same protocol.  Encode a message
--- with one codec and decode it with the other one, then compare if the result
--- is the same as initial message.
---
-prop_codecs_compatM
-  :: forall ps failure m bytes.
-     ( Monad m
-     , Eq (AnyMessage ps)
-     , forall a. Monoid a => Monoid (m a)
-     )
-  => Codec ps failure m bytes
-  -- ^ first codec
-  -> Codec ps failure m bytes
-  -- ^ second codec
-  -> AnyMessage ps
-  -- ^ some message
-  -> m Bool
-prop_codecs_compatM codecA codecB
-                    (AnyMessage (msg :: Message ps st st')) =
-    getAll <$> do r <- decode codecB (stateToken :: StateToken st) >>= runDecoder [encode codecA msg]
-                  case r :: Either failure (SomeMessage st) of
-                    Right (SomeMessage msg') -> return $! All $ AnyMessage msg' == AnyMessage msg
-                    Left _                   -> return $! All False
-            <> do r <- decode codecA (stateToken :: StateToken st) >>= runDecoder [encode codecB msg]
-                  case r :: Either failure (SomeMessage st) of
-                    Right (SomeMessage msg') -> return $! All $ AnyMessage msg' == AnyMessage msg
-                    Left _                   -> return $! All False
-
--- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@.
---
-prop_codecs_compat
-  :: forall ps failure m bytes.
-     ( Monad m
-     , Eq (AnyMessage ps)
-     , forall a. Monoid a => Monoid (m a)
-     )
-  => (forall a. m a -> a)
-  -> Codec ps failure m bytes
-  -> Codec ps failure m bytes
-  -> AnyMessage ps
-  -> Bool
-prop_codecs_compat run codecA codecB msg =
-    run $ prop_codecs_compatM codecA codecB msg
diff --git a/stateful/Network/TypedProtocol/Stateful/Codec.hs b/stateful/Network/TypedProtocol/Stateful/Codec.hs
--- a/stateful/Network/TypedProtocol/Stateful/Codec.hs
+++ b/stateful/Network/TypedProtocol/Stateful/Codec.hs
@@ -35,16 +35,9 @@
     -- * Testing codec properties
   , AnyMessage (.., AnyMessageAndAgency)
   , showAnyMessage
-  , prop_codecM
-  , prop_codec
-  , prop_codec_splitsM
-  , prop_codec_splits
-  , prop_codecs_compatM
-  , prop_codecs_compat
   ) where
 
 import Data.Kind (Type)
-import Data.Monoid (All (..))
 
 import Network.TypedProtocol.Codec (CodecFailure (..), DecodeStep (..),
            SomeMessage (..), hoistDecodeStep, isoDecodeStep,
@@ -55,6 +48,8 @@
 
 -- | A stateful codec.
 --
+-- TODO: provide CodecF as in typed-protocols:typed-protocols library.
+--
 data Codec ps failure (f :: ps -> Type) m bytes = Codec {
        encode :: forall (st :: ps) (st' :: ps).
                  StateTokenI st
@@ -177,119 +172,3 @@
 --
 getAgency :: StateTokenI st => Message ps st st' -> (Message ps st st', StateToken st)
 getAgency msg = (msg, stateToken)
-
-
--- | The 'Codec' round-trip property: decode after encode gives the same
--- message. Every codec must satisfy this property.
---
-prop_codecM
-  :: forall ps failure f m bytes.
-     ( Monad m
-     , Eq (AnyMessage ps f)
-     )
-  => Codec ps failure f m bytes
-  -> AnyMessage ps f
-  -> m Bool
-prop_codecM Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do
-    r <- decode (stateToken :: StateToken st) f >>= runDecoder [encode f msg]
-    case r :: Either failure (SomeMessage st) of
-      Right (SomeMessage msg') -> return $ AnyMessage f msg' == a
-      Left _                   -> return False
-
--- | The 'Codec' round-trip property in a pure monad.
---
-prop_codec
-  :: forall ps failure f m bytes.
-     (Monad m, Eq (AnyMessage ps f))
-  => (forall a. m a -> a)
-  -> Codec ps failure f m bytes
-  -> AnyMessage ps f
-  -> Bool
-prop_codec runM codec msg =
-    runM (prop_codecM codec msg)
-
-
--- | A variant on the codec round-trip property: given the encoding of a
--- message, check that decode always gives the same result irrespective
--- of how the chunks of input are fed to the incremental decoder.
---
--- This property guards against boundary errors in incremental decoders.
--- It is not necessary to check this for every message type, just for each
--- generic codec construction. For example given some binary serialisation
--- library one would write a generic adaptor to the codec interface. This
--- adaptor has to deal with the incremental decoding and this is what needs
--- to be checked.
---
-prop_codec_splitsM
-  :: forall ps failure f m bytes.
-     (Monad m, Eq (AnyMessage ps f))
-  => (bytes -> [[bytes]])   -- ^ alternative re-chunkings of serialised form
-  -> Codec ps failure f m bytes
-  -> AnyMessage ps f
-  -> m Bool
-prop_codec_splitsM splits
-                   Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do
-    and <$> sequence
-      [ do r <- decode (stateToken :: StateToken st) f >>= runDecoder bytes'
-           case r :: Either failure (SomeMessage st) of
-             Right (SomeMessage msg') -> return $ AnyMessage f msg' == a
-             Left _                   -> return False
-
-      | let bytes = encode f msg
-      , bytes' <- splits bytes ]
-
-
--- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@.
---
-prop_codec_splits
-  :: forall ps failure f m bytes.
-     (Monad m, Eq (AnyMessage ps f))
-  => (bytes -> [[bytes]])
-  -> (forall a. m a -> a)
-  -> Codec ps failure f m bytes
-  -> AnyMessage ps f
-  -> Bool
-prop_codec_splits splits runM codec msg =
-    runM $ prop_codec_splitsM splits codec msg
-
-
--- | Compatibility between two codecs of the same protocol.  Encode a message
--- with one codec and decode it with the other one, then compare if the result
--- is the same as initial message.
---
-prop_codecs_compatM
-  :: forall ps failure f m bytes.
-     ( Monad m
-     , Eq (AnyMessage ps f)
-     , forall a. Monoid a => Monoid (m a)
-     )
-  => Codec ps failure f m bytes
-  -> Codec ps failure f m bytes
-  -> AnyMessage ps f
-  -> m Bool
-prop_codecs_compatM codecA codecB
-                    a@(AnyMessage f (msg :: Message ps st st')) =
-    getAll <$> do r <- decode codecB (stateToken :: StateToken st) f >>= runDecoder [encode codecA f msg]
-                  case r :: Either failure (SomeMessage st) of
-                    Right (SomeMessage msg') -> return $ All $ AnyMessage f msg' == a
-                    Left _                   -> return $ All False
-            <> do r <- decode codecA (stateToken :: StateToken st) f >>= runDecoder [encode codecB f msg]
-                  case r :: Either failure (SomeMessage st) of
-                    Right (SomeMessage msg') -> return $ All $ AnyMessage f msg' == a
-                    Left _                   -> return $ All False
-
--- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@.
---
-prop_codecs_compat
-  :: forall ps failure f m bytes.
-     ( Monad m
-     , Eq (AnyMessage ps f)
-     , forall a. Monoid a => Monoid (m a)
-     )
-  => (forall a. m a -> a)
-  -> Codec ps failure f m bytes
-  -> Codec ps failure f m bytes
-  -> AnyMessage ps f
-  -> Bool
-prop_codecs_compat run codecA codecB msg =
-    run $ prop_codecs_compatM codecA codecB msg
diff --git a/test/Network/TypedProtocol/PingPong/Tests.hs b/test/Network/TypedProtocol/PingPong/Tests.hs
--- a/test/Network/TypedProtocol/PingPong/Tests.hs
+++ b/test/Network/TypedProtocol/PingPong/Tests.hs
@@ -13,6 +13,7 @@
 
 import Network.TypedProtocol.Channel
 import Network.TypedProtocol.Codec
+import Network.TypedProtocol.Codec.Properties
 import Network.TypedProtocol.Driver.Simple
 import Network.TypedProtocol.Proofs
 
@@ -390,20 +391,20 @@
   AnyMessage MsgDone == AnyMessage MsgDone = True
   _                  ==                  _ = False
 
-prop_codec_PingPong :: AnyMessage PingPong -> Bool
+prop_codec_PingPong :: AnyMessage PingPong -> Property
 prop_codec_PingPong =
     prop_codec
       runIdentity
       codecPingPong
 
-prop_codec_splits2_PingPong :: AnyMessage PingPong -> Bool
+prop_codec_splits2_PingPong :: AnyMessage PingPong -> Property
 prop_codec_splits2_PingPong =
     prop_codec_splits
       splits2
       runIdentity
       codecPingPong
 
-prop_codec_splits3_PingPong :: AnyMessage PingPong -> Bool
+prop_codec_splits3_PingPong :: AnyMessage PingPong -> Property
 prop_codec_splits3_PingPong =
     prop_codec_splits
       splits3
@@ -416,13 +417,13 @@
 
 prop_codec_cbor_PingPong
   :: AnyMessage PingPong
-  -> Bool
+  -> Property
 prop_codec_cbor_PingPong msg =
   runST $ prop_codecM CBOR.codecPingPong msg
 
 prop_codec_cbor_splits2_PingPong
   :: AnyMessage PingPong
-  -> Bool
+  -> Property
 prop_codec_cbor_splits2_PingPong msg =
   runST $ prop_codec_splitsM
       splits2BS
@@ -431,7 +432,7 @@
 
 prop_codec_cbor_splits3_PingPong
   :: AnyMessage PingPong
-  -> Bool
+  -> Property
 prop_codec_cbor_splits3_PingPong msg =
   runST $ prop_codec_splitsM
       splits3BS
diff --git a/test/Network/TypedProtocol/ReqResp/Tests.hs b/test/Network/TypedProtocol/ReqResp/Tests.hs
--- a/test/Network/TypedProtocol/ReqResp/Tests.hs
+++ b/test/Network/TypedProtocol/ReqResp/Tests.hs
@@ -6,6 +6,7 @@
 
 import Network.TypedProtocol.Channel
 import Network.TypedProtocol.Codec
+import Network.TypedProtocol.Codec.Properties
 import Network.TypedProtocol.Driver.Simple
 import Network.TypedProtocol.Proofs
 
@@ -21,7 +22,6 @@
 import Control.Monad.Class.MonadST
 import Control.Monad.Class.MonadSTM
 import Control.Monad.Class.MonadThrow
-import Control.Monad.Class.MonadTimer.SI
 import Control.Monad.IOSim
 import Control.Monad.ST (runST)
 import Control.Tracer (nullTracer)
@@ -73,6 +73,9 @@
       , testProperty "codec 3-splits"  $ withMaxSuccess 30 prop_codec_cbor_splits3_ReqResp
       ]
     ]
+  , testGroup "AnnotatedCodec"
+    [ testProperty "codec"             prop_anncodec_ReqResp
+    ]
   ]
 
 
@@ -193,7 +196,7 @@
 
 
 prop_channelPipelined :: ( MonadLabelledSTM m, MonadAsync m, MonadCatch m
-                         , MonadDelay m, MonadST m)
+                         , MonadST m)
                       => (Int -> Int -> (Int, Int)) -> [Int]
                       -> m Bool
 prop_channelPipelined f xs = do
@@ -315,14 +318,14 @@
   (AnyMessage MsgDone)      == (AnyMessage MsgDone)      = True
   _                         == _                         = False
 
-prop_codec_ReqResp :: AnyMessage (ReqResp String String) -> Bool
+prop_codec_ReqResp :: AnyMessage (ReqResp String String) -> Property
 prop_codec_ReqResp =
     prop_codec
       runIdentity
       codecReqResp
 
 prop_codec_splits2_ReqResp :: AnyMessage (ReqResp String String)
-                           -> Bool
+                           -> Property
 prop_codec_splits2_ReqResp =
     prop_codec_splits
       splits2
@@ -330,7 +333,7 @@
       codecReqResp
 
 prop_codec_splits3_ReqResp :: AnyMessage (ReqResp String String)
-                           -> Bool
+                           -> Property
 prop_codec_splits3_ReqResp =
     prop_codec_splits
       splits3
@@ -339,13 +342,13 @@
 
 prop_codec_cbor_ReqResp
   :: AnyMessage (ReqResp String String)
-  -> Bool
+  -> Property
 prop_codec_cbor_ReqResp msg =
   runST $ prop_codecM CBOR.codecReqResp msg
 
 prop_codec_cbor_splits2_ReqResp
   :: AnyMessage (ReqResp String String)
-  -> Bool
+  -> Property
 prop_codec_cbor_splits2_ReqResp msg =
   runST $ prop_codec_splitsM
       splits2BS
@@ -354,9 +357,22 @@
 
 prop_codec_cbor_splits3_ReqResp
   :: AnyMessage (ReqResp String String)
-  -> Bool
+  -> Property
 prop_codec_cbor_splits3_ReqResp msg =
   runST $ prop_codec_splitsM
       splits3BS
       CBOR.codecReqResp
       msg
+
+
+instance (Show a, Arbitrary a) => Arbitrary (WithBytes a) where
+  arbitrary = mkWithBytes <$> arbitrary
+  shrink WithBytes { message } = mkWithBytes <$> shrink message
+
+prop_anncodec_ReqResp
+  :: AnyMessage (ReqResp (WithBytes Int) (WithBytes Int))
+  -> Property
+prop_anncodec_ReqResp =
+  prop_anncodec
+    runIdentity
+    anncodecReqResp
diff --git a/typed-protocols.cabal b/typed-protocols.cabal
--- a/typed-protocols.cabal
+++ b/typed-protocols.cabal
@@ -1,8 +1,9 @@
 cabal-version:       3.4
 name:                typed-protocols
-version:             1.0.0.0
+version:             1.1.0.0
 synopsis:            A framework for strongly typed protocols
 description:         A robust session type framework which supports protocol pipelining.
+                     Haddocks are published [here](https://input-output-hk.github.io/typed-protocols/)
 license:             Apache-2.0
 license-files:
   LICENSE
@@ -16,25 +17,12 @@
 extra-doc-files:     CHANGELOG.md
                      README.md
 
-library
-  exposed-modules:   Network.TypedProtocol
-                   , Network.TypedProtocol.Core
-                   , Network.TypedProtocol.Peer
-                   , Network.TypedProtocol.Peer.Client
-                   , Network.TypedProtocol.Peer.Server
-                   , Network.TypedProtocol.Codec
-                   , Network.TypedProtocol.Driver
-                   , Network.TypedProtocol.Proofs
-  other-modules:     Network.TypedProtocol.Lemmas
-  build-depends:     base >=4.12 && <4.22,
-                     io-classes:io-classes ^>= 1.8,
-                     singletons ^>= 3.0
-
-  hs-source-dirs:    src
-  default-language:  GHC2021
-  default-extensions: DataKinds
-                      GADTs
-                      LambdaCase
+-- Minimal GHC setup, additional extensions are enabled per package (e.g.
+-- pervasive type level extensions in the code base like `GADTs` or
+-- `DataKinds`, etc), or per module (e.g. `CPP` or other more exotic ones).
+common GHC
+  default-language:   GHC2021
+  default-extensions: LambdaCase
   ghc-options:       -Wall
                      -Wno-unticked-promoted-constructors
                      -Wcompat
@@ -43,33 +31,52 @@
                      -Wpartial-fields
                      -Widentities
                      -Wredundant-constraints
+                     -Wunused-packages
 
-library cborg
-  visibility:        public
-  exposed-modules:   Network.TypedProtocol.Codec.CBOR
+library
+  import:             GHC
+  exposed-modules:    Network.TypedProtocol
+                    , Network.TypedProtocol.Core
+                    , Network.TypedProtocol.Peer
+                    , Network.TypedProtocol.Peer.Client
+                    , Network.TypedProtocol.Peer.Server
+                    , Network.TypedProtocol.Codec
+                    , Network.TypedProtocol.Driver
+                    , Network.TypedProtocol.Proofs
+  other-modules:      Network.TypedProtocol.Lemmas
+  build-depends:      base >=4.12 && <4.22,
+                      io-classes:io-classes ^>= 1.8,
+                      singletons ^>= 3.0
+  hs-source-dirs:     src
+  default-extensions: DataKinds
+                      GADTs
 
-  build-depends:     base,
-                     bytestring      >=0.10  && <0.13,
-                     cborg           >=0.2.1 && <0.3,
-                     singletons,       
-                     primitive,
+library codec-properties
+  import:             GHC
+  visibility:         public
+  exposed-modules:    Network.TypedProtocol.Codec.Properties
+                      Network.TypedProtocol.Stateful.Codec.Properties
+  build-depends:      base >=4.12 && <4.22,
+                      typed-protocols:{stateful, typed-protocols},
+                      QuickCheck >= 2.16
+  hs-source-dirs:     properties
+  default-extensions: GADTs
+                      ImportQualifiedPost
 
-                     io-classes:io-classes,
-                     typed-protocols:typed-protocols
+library cborg
+  import:             GHC
+  visibility:         public
+  exposed-modules:    Network.TypedProtocol.Codec.CBOR
+  build-depends:      base,
+                      bytestring      >=0.10  && <0.13,
+                      cborg           >=0.2.1 && <0.3,
 
-  hs-source-dirs:    cborg
-  default-language:  GHC2021
-  default-extensions: LambdaCase
-  ghc-options:       -Wall
-                     -Wno-unticked-promoted-constructors
-                     -Wcompat
-                     -Wincomplete-uni-patterns
-                     -Wincomplete-record-updates
-                     -Wpartial-fields
-                     -Widentities
-                     -Wredundant-constraints
+                      io-classes:io-classes,
+                      typed-protocols:typed-protocols
+  hs-source-dirs:     cborg
 
 library stateful
+  import:             GHC
   visibility:         public
   exposed-modules:    Network.TypedProtocol.Stateful.Peer
                     , Network.TypedProtocol.Stateful.Peer.Client
@@ -81,124 +88,88 @@
                       singletons,
                       io-classes:io-classes,
                       typed-protocols:typed-protocols
-
   hs-source-dirs:     stateful
-  default-language:   GHC2021
   default-extensions: DataKinds
                       GADTs
                       ImportQualifiedPost
-  ghc-options:        -Wall
-                      -Wno-unticked-promoted-constructors
-                      -Wcompat
-                      -Wincomplete-uni-patterns
-                      -Wincomplete-record-updates
-                      -Wpartial-fields
-                      -Widentities
-                      -Wredundant-constraints
 
 library stateful-cborg
-  visibility:        public
-  exposed-modules:   Network.TypedProtocol.Stateful.Codec.CBOR
-
-  build-depends:     base,
-                     bytestring,
-                     cborg,
-                     singletons,       
+  import:             GHC
+  visibility:         public
+  exposed-modules:    Network.TypedProtocol.Stateful.Codec.CBOR
 
-                     io-classes:io-classes,
-                     typed-protocols:{typed-protocols,cborg,stateful}
+  build-depends:      base,
+                      bytestring,
+                      cborg,
 
-  hs-source-dirs:    stateful-cborg
-  default-language:  GHC2021
+                      io-classes:io-classes,
+                      typed-protocols:{typed-protocols,cborg,stateful}
+  hs-source-dirs:     stateful-cborg
   default-extensions: ImportQualifiedPost
-  ghc-options:       -Wall
-                     -Wno-unticked-promoted-constructors
-                     -Wcompat
-                     -Wincomplete-uni-patterns
-                     -Wincomplete-record-updates
-                     -Wpartial-fields
-                     -Widentities
-                     -Wredundant-constraints
 
 library examples
-  visibility:        public
-  exposed-modules:   Network.TypedProtocol.Channel
-                   , Network.TypedProtocol.Driver.Simple
-
-                   , Network.TypedProtocol.PingPong.Type
-                   , Network.TypedProtocol.PingPong.Client
-                   , Network.TypedProtocol.PingPong.Server
-                   , Network.TypedProtocol.PingPong.Codec
-                   , Network.TypedProtocol.PingPong.Codec.CBOR
-                   , Network.TypedProtocol.PingPong.Examples
+  import:             GHC
+  visibility:         public
+  exposed-modules:    Network.TypedProtocol.Channel
+                    , Network.TypedProtocol.Driver.Simple
 
-                   , Network.TypedProtocol.ReqResp.Type
-                   , Network.TypedProtocol.ReqResp.Client
-                   , Network.TypedProtocol.ReqResp.Server
-                   , Network.TypedProtocol.ReqResp.Codec
-                   , Network.TypedProtocol.ReqResp.Codec.CBOR
-                   , Network.TypedProtocol.ReqResp.Examples
+                    , Network.TypedProtocol.PingPong.Type
+                    , Network.TypedProtocol.PingPong.Client
+                    , Network.TypedProtocol.PingPong.Server
+                    , Network.TypedProtocol.PingPong.Codec
+                    , Network.TypedProtocol.PingPong.Codec.CBOR
+                    , Network.TypedProtocol.PingPong.Examples
 
-                   , Network.TypedProtocol.ReqResp2.Type
-                   , Network.TypedProtocol.ReqResp2.Client
+                    , Network.TypedProtocol.ReqResp.Type
+                    , Network.TypedProtocol.ReqResp.Client
+                    , Network.TypedProtocol.ReqResp.Server
+                    , Network.TypedProtocol.ReqResp.Codec
+                    , Network.TypedProtocol.ReqResp.Codec.CBOR
+                    , Network.TypedProtocol.ReqResp.Examples
 
-                   , Network.TypedProtocol.Stateful.ReqResp.Type
-                   , Network.TypedProtocol.Stateful.ReqResp.Client
-                   , Network.TypedProtocol.Stateful.ReqResp.Server
-                   , Network.TypedProtocol.Stateful.ReqResp.Codec
-                   , Network.TypedProtocol.Stateful.ReqResp.Examples
+                    , Network.TypedProtocol.ReqResp2.Type
+                    , Network.TypedProtocol.ReqResp2.Client
 
-                   , Network.TypedProtocol.Trans.Wedge
-  build-depends:     base,
-                     bytestring,
-                     cborg,
-                     serialise,
-                     singletons,
-                     contra-tracer,
-                     io-classes:{io-classes, si-timers},
-                     network,
-                     time,
-                     typed-protocols:{typed-protocols,cborg,stateful}
+                    , Network.TypedProtocol.Stateful.ReqResp.Type
+                    , Network.TypedProtocol.Stateful.ReqResp.Client
+                    , Network.TypedProtocol.Stateful.ReqResp.Server
+                    , Network.TypedProtocol.Stateful.ReqResp.Codec
+                    , Network.TypedProtocol.Stateful.ReqResp.Examples
 
-  hs-source-dirs:    examples
-  default-language:  GHC2021
+                    , Network.TypedProtocol.Trans.Wedge
+  build-depends:      base,
+                      bytestring,
+                      cborg,
+                      serialise,
+                      singletons,
+                      contra-tracer,
+                      io-classes:{io-classes, si-timers},
+                      typed-protocols:{typed-protocols,cborg,stateful}
+  if !os(windows)
+    build-depends:    network
+  hs-source-dirs:     examples
   default-extensions: DataKinds
                       GADTs
-                      LambdaCase
-  ghc-options:       -Wall
-                     -Wno-unticked-promoted-constructors
-                     -Wcompat
-                     -Wincomplete-uni-patterns
-                     -Wincomplete-record-updates
-                     -Wpartial-fields
-                     -Widentities
-                     -Wredundant-constraints
 
 test-suite test
-  type:              exitcode-stdio-1.0
-  main-is:           Main.hs
-  hs-source-dirs:    test
-  default-language:  GHC2021
+  import:             GHC
+  type:               exitcode-stdio-1.0
+  main-is:            Main.hs
+  hs-source-dirs:     test
   default-extensions: GADTs
-                      LambdaCase
-  other-modules:     Network.TypedProtocol.PingPong.Tests
-                   , Network.TypedProtocol.ReqResp.Tests
-  build-depends:     base
-                   , bytestring
-                   , contra-tracer
-                   , typed-protocols:{typed-protocols,cborg,examples}
-                   , io-classes:{io-classes,si-timers}
-                   , io-sim
-                   , QuickCheck
-                   , tasty
-                   , tasty-quickcheck
-
+  other-modules:      Network.TypedProtocol.PingPong.Tests
+                    , Network.TypedProtocol.ReqResp.Tests
+  build-depends:      base
+                    , bytestring
+                    , contra-tracer
+                    , typed-protocols:{typed-protocols,codec-properties,examples}
+                    , io-classes:io-classes
+                    , io-sim
+                    , QuickCheck
+                    , tasty
+                    , tasty-quickcheck
   if !os(windows)
       build-depends: directory
                    , network
                    , unix
-
-  ghc-options:       -rtsopts
-                     -Wall
-                     -Wno-unticked-promoted-constructors
-                     -Wno-orphans
+  ghc-options:      -rtsopts