diff --git a/.hlint.yaml b/.hlint.yaml
index 217d5ff..054580b 100644
--- a/.hlint.yaml
+++ b/.hlint.yaml
@@ -2,11 +2,17 @@
 - group: {name: generalise, enabled: true}
 - functions:
   - {name: undefined, within: []}
+# Do not prohibit using more monomorphic functions
 - ignore: {name: Use pure}
+- ignore: {name: Use fmap}
+- ignore: {name: Use traverse_}
+- ignore: {name: "Use <>"}
+# Do not enforce less explicit expressions
+# and util functions consisting of single line of code
+- ignore: {name: Use isNothing}
 - ignore: {name: Use print}
 - ignore: {name: Use null}
 - ignore: {name: Use notElem}
 - ignore: {name: Use unless}
-- ignore: {name: Use fmap}
-- ignore: {name: Use traverse_}
 - ignore: {name: "Use asks"}
+- ignore: {name: "Eta reduce"}
diff --git a/cem-script.cabal b/cem-script.cabal
index f4205b3..74a5668 100644
--- a/cem-script.cabal
+++ b/cem-script.cabal
@@ -170,6 +170,7 @@ library
     Cardano.CEM.OffChain
     Cardano.CEM.OnChain
     Cardano.CEM.Stages
+    Cardano.CEM.Testing.StateMachine
 
   other-modules:   Cardano.CEM.Monads.L1Commons
   build-depends:
@@ -178,6 +179,8 @@ library
     , clb
     , dependent-map
     , ouroboros-consensus
+    , QuickCheck
+    , quickcheck-dynamic
     , singletons-th
 
 test-suite cem-sdk-test
@@ -201,6 +204,7 @@ test-suite cem-sdk-test
   hs-source-dirs: test/
   other-modules:
     Auction
+    Dynamic
     OffChain
     TestNFT
     Utils
diff --git a/src-lib/data-spine/Data/Spine.hs b/src-lib/data-spine/Data/Spine.hs
index 974167c..82ebcfa 100644
--- a/src-lib/data-spine/Data/Spine.hs
+++ b/src-lib/data-spine/Data/Spine.hs
@@ -25,13 +25,13 @@ class
   type Spine sop
   getSpine :: sop -> Spine sop
 
--- instance (SingI sop1, SingI sop2) => SingI (sop1, sop2) where
-
 instance (HasSpine sop1, HasSpine sop2) => HasSpine (sop1, sop2) where
   type Spine (sop1, sop2) = (Spine sop1, Spine sop2)
   getSpine (d1, d2) = (getSpine d1, getSpine d2)
 
--- TODO: mkOfSpine, using Sing
+instance (HasSpine sop) => HasSpine (Maybe sop) where
+  type Spine (Maybe sop) = Maybe (Spine sop)
+  getSpine = fmap getSpine
 
 -- | Newtype encoding sop value of fixed known spine
 newtype OfSpine (x :: Spine datatype) = UnsafeMkOfSpine {getValue :: datatype}
diff --git a/src/Cardano/CEM.hs b/src/Cardano/CEM.hs
index f1b5f36..eeaa045 100644
--- a/src/Cardano/CEM.hs
+++ b/src/Cardano/CEM.hs
@@ -125,6 +125,15 @@ data TransitionSpec script = MkTransitionSpec
   }
   deriving stock (Show)
 
+-- | List of all signing keys required for transition spec
+getAllSpecSigners :: TransitionSpec script -> [PubKeyHash]
+getAllSpecSigners spec = signers spec ++ txInPKHs
+  where
+    txInPKHs = mapMaybe getPubKey $ filter ((Prelude.== In) . txFanCKind) $ constraints spec
+    getPubKey c = case address (txFanCFilter c) of
+      ByPubKey key -> Just key
+      _ -> Nothing
+
 {- | Static part of CEMScript datum.
 Datatype is actually used only by off-chain code due to Plutus limitations.
 -}
diff --git a/src/Cardano/CEM/Examples/Auction.hs b/src/Cardano/CEM/Examples/Auction.hs
index 5ba725b..53eb001 100644
--- a/src/Cardano/CEM/Examples/Auction.hs
+++ b/src/Cardano/CEM/Examples/Auction.hs
@@ -105,7 +105,7 @@ instance CEMScript SimpleAuction where
                   (SumValueEq $ lot params)
               , nextState NotStarted
               ]
-          , signers = [seller params]
+          , signers = []
           }
     (Just NotStarted, Start) ->
       Right
diff --git a/src/Cardano/CEM/Monads/CLB.hs b/src/Cardano/CEM/Monads/CLB.hs
index 93467d1..8b74b29 100644
--- a/src/Cardano/CEM/Monads/CLB.hs
+++ b/src/Cardano/CEM/Monads/CLB.hs
@@ -77,16 +77,21 @@ instance (MonadFail m) => MonadSubmitTx (ClbT m) where
         result <- sendTx tx'
         case result of
           Success _ _ -> return $ Right $ getTxId body
-          _ -> fail "TODO"
+          Fail _ validationError ->
+            return $ Left $ UnhandledNodeSubmissionError validationError
       Right (_, _) -> fail "Unsupported tx format"
       Left e -> return $ Left $ UnhandledAutobalanceError e
 
 instance (MonadFail m) => MonadTest (ClbT m) where
   getTestWalletSks = return $ map intToCardanoSk [1 .. 10]
 
+genesisClbState :: Value -> ClbState
+genesisClbState genesisValue =
+  initClb defaultBabbage genesisValue genesisValue
+
 execOnIsolatedClb :: Value -> ClbT IO a -> IO a
 execOnIsolatedClb genesisValue action =
   fst
     <$> runStateT
       (unwrapClbT action)
-      (initClb defaultBabbage genesisValue genesisValue)
+      (genesisClbState genesisValue)
diff --git a/src/Cardano/CEM/Testing/StateMachine.hs b/src/Cardano/CEM/Testing/StateMachine.hs
new file mode 100644
index 0000000..fd9dbdd
--- /dev/null
+++ b/src/Cardano/CEM/Testing/StateMachine.hs
@@ -0,0 +1,268 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+-- | Generic utils for using `quickcheck-dynamic`
+module Cardano.CEM.Testing.StateMachine where
+
+import Prelude
+
+import Control.Monad (void)
+import Control.Monad.Trans (MonadIO (..))
+import Data.Bifunctor (Bifunctor (..))
+import Data.Data (Typeable)
+import Data.Maybe (mapMaybe)
+import Data.Set qualified as Set
+
+import PlutusLedgerApi.V1 (PubKeyHash)
+import PlutusTx.IsData (FromData (..))
+
+import Cardano.Api (PaymentKey, SigningKey, Value)
+
+import Clb (ClbT)
+import Test.QuickCheck
+import Test.QuickCheck.DynamicLogic (DynLogicModel)
+import Test.QuickCheck.Gen qualified as Gen
+import Test.QuickCheck.Monadic (monadic)
+import Test.QuickCheck.StateModel (
+  Actions,
+  Any (..),
+  Generic,
+  HasVariables (..),
+  Realized,
+  RunModel (..),
+  StateModel (..),
+  runActions,
+ )
+import Text.Show.Pretty (ppShow)
+
+import Cardano.CEM (CEMParams (..))
+import Cardano.CEM hiding (scriptParams)
+import Cardano.CEM.Monads (MonadSubmitTx)
+import Cardano.CEM.Monads.CLB
+import Cardano.CEM.OffChain
+import Cardano.CEM.OnChain (CEMScriptCompiled)
+import Cardano.Extras
+import Data.Spine (HasSpine (..))
+
+data ScriptStateParams a = MkScriptStateParams
+  { actors :: [SigningKey PaymentKey]
+  , cemParams :: CEMParams a
+  }
+  deriving stock (Generic)
+
+params :: ScriptStateParams script -> Params script
+params = scriptParams . cemParams
+
+deriving stock instance (Eq (CEMParams a)) => Eq (ScriptStateParams a)
+deriving stock instance (Show (CEMParams a)) => Show (ScriptStateParams a)
+
+data ScriptState a
+  = Void
+  | ActorsKnown [SigningKey PaymentKey]
+  | ScriptState
+      { dappParams :: ScriptStateParams a
+      , state :: Maybe (State a)
+      , involvedActors :: Set.Set PubKeyHash
+      , finished :: Bool
+      }
+  deriving stock (Generic)
+
+deriving stock instance
+  (Eq (State a), Eq (CEMParams a)) => Eq (ScriptState a)
+deriving stock instance
+  (Show (State a), Show (CEMParams a)) => Show (ScriptState a)
+
+instance HasVariables (ScriptState a) where
+  getAllVariables _ = Set.empty
+
+instance {-# OVERLAPS #-} HasVariables (Action (ScriptState script) a) where
+  getAllVariables _ = Set.empty
+
+class
+  ( CEMScriptCompiled script
+  , Show (Transition script)
+  , Show (State script)
+  , Show (CEMParams script)
+  , Eq (State script)
+  , Eq (CEMParams script)
+  , Eq (Transition script)
+  ) =>
+  CEMScriptArbitrary script
+  where
+  arbitraryCEMParams :: [SigningKey PaymentKey] -> Gen (CEMParams script)
+  arbitraryTransition ::
+    ScriptStateParams script -> Maybe (State script) -> Gen (Transition script)
+
+instance (CEMScriptArbitrary script) => StateModel (ScriptState script) where
+  data Action (ScriptState script) output where
+    SetupActors :: [SigningKey PaymentKey] -> Action (ScriptState script) ()
+    SetupCEMParams :: CEMParams script -> Action (ScriptState script) ()
+    ScriptTransition ::
+      Transition script -> Action (ScriptState script) ()
+    deriving stock (Typeable)
+
+  type Error (ScriptState script) = String
+
+  initialState = Void
+
+  actionName (ScriptTransition transition) = head . words . show $ transition
+  actionName SetupActors {} = "SetupActors"
+  actionName SetupCEMParams {} = "SetupCEMParams"
+
+  arbitraryAction _varCtx modelState = case modelState of
+    Void {} -> Gen.oneof [] -- SetupActors should be done manually
+    ActorsKnown actors ->
+      Some . SetupCEMParams <$> arbitraryCEMParams actors
+    ScriptState {dappParams, state} ->
+      Some . ScriptTransition <$> arbitraryTransition dappParams state
+
+  precondition Void (SetupActors {}) = True
+  precondition (ActorsKnown {}) (SetupCEMParams {}) = True
+  precondition
+    (ScriptState {dappParams, state, finished})
+    (ScriptTransition transition) =
+      case transitionSpec @script (params dappParams) state transition of
+        Right _ -> not finished
+        Left _ -> False
+  -- Unreachable
+  precondition _ _ = False
+
+  nextState Void (SetupActors actors) _var = ActorsKnown actors
+  nextState (ActorsKnown actors) (SetupCEMParams cemParams) _var =
+    ScriptState
+      { dappParams = MkScriptStateParams {actors, cemParams}
+      , state = Nothing
+      , involvedActors = Set.empty
+      , finished = False
+      }
+  nextState
+    as@ScriptState {dappParams, state}
+    (ScriptTransition transition)
+    _var =
+      case transitionSpec (params dappParams) state transition of
+        Right spec ->
+          as
+            { state = nextCEMState spec
+            , involvedActors =
+                involvedActors as
+                  <> Set.fromList (getAllSpecSigners spec)
+            , finished = nextCEMState spec == Nothing
+            }
+        Left _ -> error "Unreachable"
+      where
+        nextCEMState spec = case outStates spec of
+          [] -> Nothing
+          [state'] -> Just state'
+          _ ->
+            error
+              "This StateModel instance support only with single-output scripts"
+        outStates spec = mapMaybe decodeOutState $ constraints spec
+        decodeOutState c = case rest (txFanCFilter c) of
+          UnsafeBySameCEM stateBS ->
+            fromBuiltinData @(State script) stateBS
+          _ -> Nothing
+  nextState _ _ _ = error "Unreachable"
+
+instance (CEMScriptArbitrary script) => Show (Action (ScriptState script) a) where
+  show (ScriptTransition t) = "ScriptTransition " <> show t
+  show (SetupActors {}) = "SetupActors"
+  show (SetupCEMParams {}) = "SetupCEMParams"
+
+deriving stock instance
+  (CEMScriptArbitrary script) => Eq (Action (ScriptState script) a)
+
+instance (CEMScriptArbitrary script) => DynLogicModel (ScriptState script)
+
+-- RunModel
+
+type instance Realized (ClbT m) () = ()
+
+findSkForPKH :: [SigningKey PaymentKey] -> PubKeyHash -> SigningKey PaymentKey
+findSkForPKH sks phk = head $ filter (\x -> signingKeyToPKH x == phk) sks
+
+class (CEMScriptArbitrary script) => CEMScriptRunModel script where
+  performHook ::
+    (MonadIO m, MonadSubmitTx m) =>
+    ScriptState script ->
+    Action (ScriptState script) () ->
+    m ()
+
+instance
+  ( Realized m () ~ ()
+  , MonadIO m
+  , MonadSubmitTx m
+  , CEMScriptArbitrary script
+  , CEMScriptRunModel script
+  ) =>
+  RunModel (ScriptState script) m
+  where
+  perform modelState action _lookup = do
+    case (modelState, action) of
+      (Void, SetupActors {}) -> do
+        _ <- performHook modelState action
+        return $ Right ()
+      (ActorsKnown {}, SetupCEMParams {}) -> do
+        _ <- performHook modelState action
+        return $ Right ()
+      (ScriptState {dappParams, state}, ScriptTransition transition) -> do
+        _ <- performHook modelState action
+        case transitionSpec (params dappParams) state transition of
+          Right spec -> do
+            r <-
+              resolveTxAndSubmit $
+                MkTxSpec
+                  { actions =
+                      [ MkSomeCEMAction $ MkCEMAction (cemParams dappParams) transition
+                      ]
+                  , specSigner = findSkForPKH (actors dappParams) $ signerPKH spec
+                  }
+            return $ bimap show (const ()) r
+          Left err -> return $ Left $ show err
+        where
+          signerPKH spec = case getAllSpecSigners spec of
+            [singleSigner] -> singleSigner
+            _ -> error "Transition should have exactly one signer"
+      (_, _) -> error "Unreachable"
+
+  monitoring (stateFrom, stateTo) _ _ _ prop = do
+    tabStateFrom $ labelIfFinished prop
+    where
+      isFinished (ScriptState {finished}) = finished
+      isFinished _ = False
+      labelIfFinished prop' =
+        if isFinished stateTo
+          then
+            tabulate
+              "Actors involved (in finished tests)"
+              [show $ length $ involvedActors stateTo]
+              $ label "Reached final state" prop'
+          else prop'
+      tabStateFrom prop' =
+        case stateFrom of
+          ScriptState {state} ->
+            tabulate "States (from)" [show $ getSpine state] prop'
+          _ -> prop'
+
+  monitoringFailure state _ _ err prop =
+    counterexample
+      ( "In model state "
+          <> ppShow state
+          <> "\nGot error from emulator: "
+          <> err
+      )
+      prop
+
+runActionsInClb ::
+  forall state.
+  (StateModel (ScriptState state), RunModel (ScriptState state) (ClbT IO)) =>
+  Value ->
+  Actions (ScriptState state) ->
+  Property
+runActionsInClb genesisValue actions =
+  monadic (ioProperty . execOnIsolatedClb genesisValue) $
+    void $
+      runActions @(ScriptState state) @(ClbT IO) actions
+
+-- Orphans
+
+instance HasVariables (SigningKey PaymentKey) where
+  getAllVariables _ = Set.empty
diff --git a/test/Auction.hs b/test/Auction.hs
index 00a5d19..194bf2c 100644
--- a/test/Auction.hs
+++ b/test/Auction.hs
@@ -201,6 +201,18 @@ auctionSpec = describe "Auction" $ do
     Just (CurrentBid currentBid) <- queryScriptState auctionParams
     liftIO $ currentBid `shouldBe` bid1
 
+    submitAndCheck $
+      MkTxSpec
+        { actions =
+            [ MkSomeCEMAction $
+                MkCEMAction
+                  auctionParams
+                  ( MakeBid $ MkBet (signingKeyToPKH bidder1) 4_000_000
+                  )
+            ]
+        , specSigner = bidder1
+        }
+
     submitAndCheck $
       MkTxSpec
         { actions =
diff --git a/test/Dynamic.hs b/test/Dynamic.hs
new file mode 100644
index 0000000..91876cc
--- /dev/null
+++ b/test/Dynamic.hs
@@ -0,0 +1,80 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Dynamic where
+
+import Prelude
+
+import PlutusLedgerApi.V1.Value (assetClassValue)
+
+import Cardano.Api (lovelaceToValue)
+
+import Test.Hspec (describe, it, shouldBe)
+import Test.QuickCheck
+import Test.QuickCheck.DynamicLogic
+
+import Cardano.CEM (CEMParams (..))
+import Cardano.CEM.Examples.Auction
+import Cardano.CEM.Examples.Compilation ()
+import Cardano.CEM.Monads (MonadTest (..))
+import Cardano.CEM.Testing.StateMachine
+import Cardano.Extras (signingKeyToPKH)
+
+import TestNFT (testNftAssetClass)
+import Utils (execClb, mintTestTokens)
+
+-- Defining generic instances
+
+instance CEMScriptArbitrary SimpleAuction where
+  arbitraryCEMParams actors = do
+    seller <- elements actors
+    return $
+      MkCEMParams
+        ( MkAuctionParams
+            { seller = signingKeyToPKH seller
+            , lot = assetClassValue testNftAssetClass 1
+            }
+        )
+        NoControl
+
+  arbitraryTransition dappParams state = case state of
+    Nothing -> return Create
+    Just NotStarted -> return Start
+    Just (CurrentBid bid) ->
+      frequency
+        [
+          ( 100
+          , MakeBid <$> (MkBet <$> genBidder <*> genBid bid)
+          )
+        , (1, return Close)
+        ]
+    Just (Winner {}) -> return Buyout
+    where
+      genBidder = elements (map signingKeyToPKH $ actors dappParams)
+      genBid bid = (betAmount bid +) <$> chooseInteger (0, 100_500)
+
+instance CEMScriptRunModel SimpleAuction where
+  performHook (ActorsKnown actors) (SetupCEMParams cemParams) = do
+    let s = seller $ scriptParams cemParams
+    mintTestTokens (findSkForPKH actors s) 1
+    return ()
+  performHook _ _ = return ()
+
+-- Run tests
+
+dynamicSpec = describe "Quickcheck Dynamic" $ do
+  it "Auction random trace works on CLB" $ do
+    quickCheckDLScript $ do
+      anyActions_
+  where
+    genesisValue = lovelaceToValue 300_000_000_000
+    runDLScript dl =
+      forAllDL
+        dl
+        (runActionsInClb @SimpleAuction genesisValue)
+    quickCheckDLScript dl = do
+      -- FIXME: CLB bug
+      actors <- execClb $ take 9 <$> getTestWalletSks
+      result <- quickCheckResult $ runDLScript $ do
+        _ <- action $ SetupActors actors
+        dl
+      isSuccess result `shouldBe` True
diff --git a/test/Main.hs b/test/Main.hs
index 4038def..ddbae9a 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -5,11 +5,13 @@ import Prelude
 import Test.Hspec (hspec)
 
 import Auction (auctionSpec)
+import Dynamic (dynamicSpec)
 import OffChain (offChainSpec)
 import Voting (votingSpec)
 
 main :: IO ()
 main = hspec $ do
+  dynamicSpec
   offChainSpec
   auctionSpec
   votingSpec