diff --git a/marlowe-spec-test/marlowe-spec-test.cabal b/marlowe-spec-test/marlowe-spec-test.cabal
index bf314607..334481fb 100644
--- a/marlowe-spec-test/marlowe-spec-test.cabal
+++ b/marlowe-spec-test/marlowe-spec-test.cabal
@@ -47,6 +47,7 @@ library
         aeson,
         base >=4.9 && <5,
         bytestring,
+        containers,
         marlowe,
         tasty,
         tasty-hunit,
diff --git a/marlowe-spec-test/src/Marlowe/Spec/Core/Arbitrary.hs b/marlowe-spec-test/src/Marlowe/Spec/Core/Arbitrary.hs
index 2487f607..44398650 100644
--- a/marlowe-spec-test/src/Marlowe/Spec/Core/Arbitrary.hs
+++ b/marlowe-spec-test/src/Marlowe/Spec/Core/Arbitrary.hs
@@ -18,19 +18,18 @@ import Data.List (nub)
 import Marlowe.Spec.Interpret (InterpretJsonRequest, Request (..), parseValidResponse)
 import Marlowe.Spec.TypeId (TypeId (..))
 import Orderings (Ord (..), max)
-import QuickCheck.GenT (GenT, MonadGen (..), frequency, resize, scale, sized, suchThat, vectorOf)
+import QuickCheck.GenT (GenT, MonadGen (..), frequency, resize, sized, suchThat, vectorOf)
 import Semantics (Payment (..), TransactionError (..), TransactionOutput (..), TransactionOutputRecord_ext (..), TransactionWarning (..), Transaction_ext (..), computeTransaction, evalValue)
 import SemanticsGuarantees (valid_state)
 import SemanticsTypes (Action (..), Bound (..), Case (..), ChoiceId (ChoiceId), Contract (..), Environment_ext (..), Input (..), IntervalError (..), Observation (..), Party, Payee (..), State_ext (..), Token (..), Value (..), ValueId (..), minTime)
 import Test.QuickCheck (Gen, chooseInt, getSize)
 import Test.QuickCheck.Arbitrary (Arbitrary (..))
-import Test.QuickCheck.Gen (chooseInteger, elements)
+import qualified Test.QuickCheck.Gen as QC (chooseInteger, elements)
 
 data RandomResponse a
   = RandomValue a
   | UnknownType TypeId
 
-
 instance ToJSON a => ToJSON (RandomResponse a) where
   toJSON (RandomValue v) = object
     [ "value" .= v
@@ -49,17 +48,14 @@ instance FromJSON a => FromJSON (RandomResponse a) where
 data GenerateRandomValueException = GenerateRandomValueException String
   deriving (Show, Exception)
 
-
 -- | Part of the Fibonacci sequence.
 fibonaccis :: Num a => [a]
 fibonaccis = [2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987, 1597, 2584]
 
-
 -- | Inverse-Fibanoncci frequencies.
 fibonacciFrequencies :: Integral a => [a]
 fibonacciFrequencies = (1000000 `div`) <$> fibonaccis
 
-
 -- | Select an element of a list with propability proportional to inverse-Fibonacci weights.
 arbitraryFibonacci :: [a] -> Gen a
 arbitraryFibonacci = frequency . zip fibonacciFrequencies . fmap pure
@@ -80,9 +76,9 @@ arbitraryInteger = Arith.Int_of_integer <$>
     , (60, arbitraryFibonacci fibonaccis)
     ]
 
-chooseInteger' :: (Arith.Int, Arith.Int) -> Gen Arith.Int
-chooseInteger' (Arith.Int_of_integer i, Arith.Int_of_integer j) =
-  Arith.Int_of_integer <$> chooseInteger (i, j)
+chooseinteger :: (Arith.Int, Arith.Int) -> Gen Arith.Int
+chooseinteger (Arith.Int_of_integer i, Arith.Int_of_integer j) =
+  Arith.Int_of_integer <$> QC.chooseInteger (i, j)
 
 -- | An arbitrary non-negative integer, mostly small.
 arbitraryNonnegativeInteger :: Gen Arith.Int
@@ -102,10 +98,8 @@ arbitraryPositiveInteger = Arith.Int_of_integer <$>
     , (30, arbitraryFibonacci fibonaccis)
     ]
 
-type TimeInterval = (Arith.Int, Arith.Int)
-
 -- | Geneate a semi-random time interval.
-arbitraryTimeInterval :: Gen TimeInterval
+arbitraryTimeInterval :: Gen (Arith.Int, Arith.Int)
 arbitraryTimeInterval =
   do
     start <- arbitraryInteger
@@ -113,31 +107,31 @@ arbitraryTimeInterval =
     pure (start, start + duration)
 
 -- | Generate a semi-random time interrval straddling a given time.
-arbitraryTimeIntervalAround :: Arith.Int -> Gen TimeInterval
+arbitraryTimeIntervalAround :: Arith.Int -> Gen (Arith.Int, Arith.Int)
 arbitraryTimeIntervalAround limit =
   do
-    start <- arbitraryInteger `suchThat` (less_eq limit)
+    start <- arbitraryInteger `suchThat` (flip less_eq limit)
     duration <- ((limit - start) +) <$> arbitraryNonnegativeInteger
     pure (start, start + duration)
 
 -- | Generate a semi-random time interval before a given time.
-arbitraryTimeIntervalBefore :: Arith.Int -> Arith.Int -> Gen TimeInterval
+arbitraryTimeIntervalBefore :: Arith.Int -> Arith.Int -> Gen (Arith.Int, Arith.Int)
 arbitraryTimeIntervalBefore lower upper =
   do
-    start <- arbitraryInteger `suchThat` (less_eq lower)
-    duration <- chooseInteger' (0, upper - start - 1)
+    start <- arbitraryInteger `suchThat` (flip less_eq lower)
+    duration <- chooseinteger (0, upper - start - 1)
     pure (start, start + duration)
 
 -- | Generate a semi-random time interval after a given time.
-arbitraryTimeIntervalAfter :: Arith.Int -> Gen TimeInterval
+arbitraryTimeIntervalAfter :: Arith.Int -> Gen (Arith.Int, Arith.Int)
 arbitraryTimeIntervalAfter lower =
   do
-    start <- arbitraryInteger `suchThat` (\t -> less t lower)
+    start <- arbitraryInteger `suchThat` (less_eq lower)
     duration <- arbitraryNonnegativeInteger
     pure (start, start + duration)
 
 -- | Shrink a generated time interval.
-shrinkTimeInterval :: TimeInterval -> [TimeInterval]
+shrinkTimeInterval :: (Arith.Int, Arith.Int) -> [(Arith.Int, Arith.Int)]
 shrinkTimeInterval (start, end) =
   let
     mid = (start + end) `Arith.divide_int` 2
@@ -152,7 +146,6 @@ shrinkTimeInterval (start, end) =
       , (end  , end  )
       ]
 
-
 arbitrarySeed :: Gen Int
 arbitrarySeed = resize 10000 $ choose (1, 10000000)
 
@@ -178,6 +171,17 @@ genParty interpret = do
       Right (UnknownType _) -> throwIO $ GenerateRandomValueException "Client process doesn't know how to generate Core.Party"
       Right (RandomValue t) -> pure t
 
+genContract :: InterpretJsonRequest -> GenT IO Contract
+genContract interpret = do
+  size <- liftGen $ getSize
+  seed <- liftGen $ arbitrarySeed
+  liftIO do
+    res <- interpret (GenerateRandomValue (TypeId "Core.Contract" (Proxy :: Proxy Contract)) size seed)
+    case parseValidResponse res of
+      Left err -> throwIO $ GenerateRandomValueException err
+      Right (UnknownType _) -> throwIO $ GenerateRandomValueException "Client process doesn't know how to generate Core.Contract"
+      Right (RandomValue t) -> pure t
+
 genPayee ::  InterpretJsonRequest -> GenT IO Payee
 genPayee i = do
   isParty <- liftGen arbitrary
@@ -338,8 +342,8 @@ genObservation i = sized (
 
 genAction :: InterpretJsonRequest -> GenT IO Action
 genAction i = frequency
-      [ (4, Deposit <$> genParty i <*> genParty i <*> genToken i <*> genValue i)
-      , (5, do
+      [ (7, Deposit <$> genParty i <*> genParty i <*> genToken i <*> genValue i)
+      , (2, do
           lSize <- liftGen $ chooseInt (1, 4)
           Choice <$> genChoiceId i <*> vectorOf lSize (liftGen genBound)
         )
@@ -349,32 +353,6 @@ genAction i = frequency
 genCase :: InterpretJsonRequest -> GenT IO Case
 genCase i = Case <$> genAction i <*> genContract i
 
-genContract :: InterpretJsonRequest -> GenT IO Contract
-genContract i = sized (
-  \case n | n <= 1 -> genClose
-          | otherwise -> frequency
-            [ ( 30, genClose)
-            , ( 20, genPay n)
-            , ( 15, genIf n)
-            , ( 20, genWhen n)
-            , ( 10, genLet n)
-            , ( 5, genAssert n)
-            ]
-  )
-  where
-  genClose = pure Close
-  genPay n = Pay <$> genParty i <*> genPayee i <*> genToken i <*> limit (genValue i) <*> resize (n - 1) (genContract i)
-  genIf n = If <$> limit  (genObservation i) <*> resize (n - 1) (genContract i) <*> resize (n - 1) (genContract i)
-  genWhen n = do
-    lSize <- liftGen $ chooseInt (0, 3)
-    cases <- vectorOf lSize (resize (n - lSize) (genCase i))
-    timeout <- liftGen $ arbitraryInteger
-    cont <- resize (n - 1) (genContract i)
-    pure $ When cases timeout cont
-  genLet n = Let <$> liftGen genValueId <*> limit (genValue i) <*> resize (n - 1) (genContract i)
-  genAssert n = Assert <$> limit (genObservation i) <*> resize (n - 1) (genContract i)
-  limit = scale (min 3)
-
 genInput :: InterpretJsonRequest -> GenT IO Input
 genInput i = frequency
   [ (50, IDeposit <$> genParty i <*> genParty i <*> genToken i <*> liftGen arbitraryInteger)
@@ -469,27 +447,22 @@ arbitraryValidStep state (When cases timeout _) =
     isTimeout <- frequency [(9, pure False), (1, pure True)]
     if isTimeout || less_eq timeout minTime' || all (isEmptyChoice . getAction) cases
       then Transaction_ext <$> arbitraryTimeIntervalAfter timeout <*> pure [] <*> pure ()
-      else do
-             times <- arbitraryTimeIntervalBefore minTime' timeout
-             case' <- elements $ filter (not . isEmptyChoice . getAction) cases
-             i <- case getAction case' of
-                    Deposit a p t v -> pure . IDeposit a p t $ evalValue (Environment_ext times ()) state v
-                    Choice n bs     -> do
-                                         Bound lower upper <- elements bs
-                                         IChoice n <$> chooseInteger' (lower, upper)
-                    Notify _        -> pure INotify
-             pure $ Transaction_ext times [i] ()
+      else
+        do
+          times <- arbitraryTimeIntervalBefore minTime' timeout
+          case' <- QC.elements $ filter (not . isEmptyChoice . getAction) cases
+          i <- case getAction case' of
+                 Deposit a p t v -> pure . IDeposit a p t $ evalValue (Environment_ext times ()) state v
+                 Choice n bs     -> do
+                                      Bound lower upper <- QC.elements bs
+                                      IChoice n <$> chooseinteger (lower, upper)
+                 Notify _        -> pure INotify
+          pure $ Transaction_ext times [i] ()
   where
     getAction :: Case -> Action
     getAction (Case a _) = a
 
 arbitraryValidStep state contract =
-{-
-  NOTE: Alternatively, if semantics should allow applying `[]` to a non-quiescent contract
-  without ever throwing a timeout-related error, then replace the above with the following:
-
-  TransactionInput <$> arbitraryTimeIntervalAround minTime <*> pure []
--}
   let
     nextTimeout Close                                    = minTime state
     nextTimeout (Pay _ _ _ _ continuation)               = nextTimeout continuation
@@ -502,26 +475,6 @@ arbitraryValidStep state contract =
  where
   maximum' = foldl1 Orderings.max
 
--- | Generate random transaction input.
-arbitraryValidInput :: State_ext ()             -- ^ The state of the contract.
-                    -> Contract                 -- ^ The contract.
-                    -> Gen (Transaction_ext ()) -- ^ Generator for a transaction input.
-arbitraryValidInput = arbitraryValidInput' Nothing
-
-arbitraryValidInput' :: Maybe (Transaction_ext ()) -> State_ext () -> Contract -> Gen (Transaction_ext ())
-arbitraryValidInput' Nothing state contract = arbitraryValidStep state contract
-arbitraryValidInput' (Just tr@(Transaction_ext timeInterval input _)) state contract =
-  case computeTransaction tr state contract of
-    TransactionError _              -> pure tr
-    TransactionOutput (TransactionOutputRecord_ext _ _ txOutState txOutContract _) -> do
-                               Transaction_ext a nextInput b <- arbitraryValidStep state contract
-                               let
-                                 combinedInput = input ++ nextInput -- {txInputs = txInputs input ++ txInputs nextInput}
-                                 newTr = Transaction_ext a combinedInput b
-                               case computeTransaction newTr txOutState txOutContract of
-                                 TransactionError _                                        -> pure tr
-                                 TransactionOutput (TransactionOutputRecord_ext _ _ _ _ _) -> pure newTr
-
 -- | Generate a random path through a contract.
 arbitraryValidInputs :: State_ext ()             -- ^ The state of the contract.
                      -> Contract                 -- ^ The contract.
@@ -529,7 +482,7 @@ arbitraryValidInputs :: State_ext ()             -- ^ The state of the contract.
 arbitraryValidInputs _ Close = pure []
 arbitraryValidInputs state contract =
   do
-    input <- arbitraryValidInput state contract
-    case computeTransaction input state contract of  -- FIXME: It is tautological to use `computeTransaction` to filter test cases.
+    txIn <- arbitraryValidStep state contract
+    case computeTransaction txIn state contract of  -- FIXME: It is tautological to use `computeTransaction` to filter test cases.
       TransactionError _ -> pure []
-      TransactionOutput (TransactionOutputRecord_ext _ _ txOutState txOutContract _) -> (input :) <$> arbitraryValidInputs txOutState txOutContract
+      TransactionOutput (TransactionOutputRecord_ext _ _ txOutState txOutContract _) -> (txIn :) <$> arbitraryValidInputs txOutState txOutContract
diff --git a/marlowe-spec-test/src/Marlowe/Spec/Core/Semantics.hs b/marlowe-spec-test/src/Marlowe/Spec/Core/Semantics.hs
index 1608c506..9f58d9e3 100644
--- a/marlowe-spec-test/src/Marlowe/Spec/Core/Semantics.hs
+++ b/marlowe-spec-test/src/Marlowe/Spec/Core/Semantics.hs
@@ -1,13 +1,16 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE BlockArguments #-}
 
-module Marlowe.Spec.Core.Semantics where
+module Marlowe.Spec.Core.Semantics
+  ( tests
+  )
+  where
 
 import qualified Arith as Arith
 import Control.Monad.IO.Class (MonadIO(..))
 import Data.Aeson (ToJSON(..))
 import qualified Data.Aeson as JSON
-import Marlowe.Spec.Core.Arbitrary (genValue, genState, genEnvironment, genContract, genTransaction, arbitraryNonnegativeInteger, arbitraryValidStep)
+import Marlowe.Spec.Core.Arbitrary (genValue, genState, genEnvironment, genContract, genTransaction, arbitraryNonnegativeInteger, arbitraryValidInputs)
 import Marlowe.Spec.Interpret (InterpretJsonRequest, Request (..), Response (..))
 import Marlowe.Spec.Reproducible (reproducibleProperty, reproducibleProperty', generate, generateT, assertResponse)
 import Test.Tasty (TestTree, testGroup)
@@ -31,10 +34,10 @@ tests i = testGroup "Semantics"
     [ evalValueTest i
     , divisionRoundsTowardsZeroTest i
     -- TransactionBound.thy
-    -- , playTrace_only_accepts_maxTransactionsInitialStateTest i -- FIXME: does not make sense!
+    -- , playTrace_only_accepts_maxTransactionsInitialStateTest i -- FIXME: does not make sense
     -- SingleInputTransactions.thy
     , traceToSingleInputIsEquivalentTest i
-    , reduceContractUntilQuiescentIdempotentTest i -- FIXME: new request
+    , reduceContractUntilQuiescentIdempotentTest i
     -- QuiescentResults.thy
     , computeTransactionIsQuiescentTest i
     , playTraceIsQuiescentTest i
@@ -94,7 +97,7 @@ playTrace_only_accepts_maxTransactionsInitialStateTest interpret = reproducibleP
     RequestResponse res <- run $ liftIO $ interpret req
 
     case JSON.fromJSON res of
-      JSON.Success (TransactionOutput (TransactionOutputRecord_ext _ _ _ txOutContract _)) -> do
+      JSON.Success (TransactionOutput (TransactionOutputRecord_ext _ _ _ _ _)) -> do
         monitor
           ( counterexample $
               "Request: " ++ showAsJson req ++ "\n"
@@ -144,7 +147,7 @@ reduceContractUntilQuiescentIdempotentTest interpret = reproducibleProperty "red
     RequestResponse res <- run $ liftIO $ interpret req
 
     case JSON.fromJSON res of
-      JSON.Success (ContractQuiescent reduced warnings payments nsta ncont) -> do
+      JSON.Success (ContractQuiescent _ _ _ nsta ncont) -> do
         monitor
           ( counterexample $
               "Request: " ++ showAsJson req ++ "\n"
@@ -210,9 +213,9 @@ computeTransactionIsQuiescentTest interpret = reproducibleProperty "Compute tran
 --      isQuiescent (txOutContract traOut) (txOutState traOut)"
 playTraceIsQuiescentTest :: InterpretJsonRequest -> TestTree
 playTraceIsQuiescentTest interpret = reproducibleProperty "playTrace is quiescent" do
-    contract <- run $ generateT $ genContract interpret
+    contract <- run $ generateT $ genContract interpret `suchThat` (/=Close)
     startTime <- run $ generate $ arbitraryNonnegativeInteger
-    transactions <- run $ generate $ listOf1 $ arbitraryValidStep (State_ext [] [] [] startTime ()) contract
+    transactions <- run $ generate $ arbitraryValidInputs (State_ext [] [] [] startTime ()) contract `suchThat` ((>0) . length)
     let
         req :: Request JSON.Value
         req = PlayTrace (integer_of_int startTime) contract transactions
diff --git a/marlowe-spec-test/src/Marlowe/Spec/LocalInterpret.hs b/marlowe-spec-test/src/Marlowe/Spec/LocalInterpret.hs
index 926ef0b2..950f23de 100644
--- a/marlowe-spec-test/src/Marlowe/Spec/LocalInterpret.hs
+++ b/marlowe-spec-test/src/Marlowe/Spec/LocalInterpret.hs
@@ -1,9 +1,18 @@
+{-# LANGUAGE BlockArguments    #-}
 {-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeApplications  #-}
+{-# LANGUAGE LambdaCase        #-}
+{-# LANGUAGE RecordWildCards   #-}
+{-# LANGUAGE FlexibleInstances #-}
 
-module Marlowe.Spec.LocalInterpret where
+{-# OPTIONS_GHC -fno-warn-orphans #-}
 
-import Arith (Int(..))
+module Marlowe.Spec.LocalInterpret
+ ( interpretLocal
+ )
+ where
+
+import qualified Arith (Int(..))
 import qualified Data.Aeson as JSON
 import Marlowe.Spec.Interpret (Response(..), Request(..))
 import Semantics (playTrace, computeTransaction, evalValue, reduceContractUntilQuiescent)
@@ -11,13 +20,22 @@ import Marlowe.Spec.TypeId (TypeId (..), fromTypeName)
 import Marlowe.Spec.Core.Serialization.Json
 import Data.Data (Proxy)
 import Data.Aeson (Result (..),FromJSON,ToJSON)
-import SemanticsTypes (Token(Token), Party (..))
-import Test.QuickCheck (Gen, frequency, Arbitrary (arbitrary))
+import Data.Map (Map, fromList, keys)
+import SemanticsTypes (Token(Token), Party (..), Contract (..), ChoiceId (..), ValueId (..), State_ext (..), Case(..), Action (..), Value (..), Payee (..), Observation (..), Bound (..))
+import Test.QuickCheck (Gen, frequency, Arbitrary (..), suchThat, resize)
 import qualified Marlowe.Spec.Core.Arbitrary as RandomResponse
-import Marlowe.Spec.Core.Arbitrary (arbitraryFibonacci)
+import Marlowe.Spec.Core.Arbitrary (arbitraryFibonacci, arbitraryPositiveInteger, arbitraryChoiceName, arbitraryInteger, shrinkChoiceName, shrinkString, arbitraryNonnegativeInteger)
 import Test.QuickCheck.Gen (Gen(..))
 import Test.QuickCheck.Random (mkQCGen)
-
+import Test.QuickCheck (sized)
+import Test.QuickCheck (elements)
+import Test.QuickCheck (listOf)
+import Test.QuickCheck.Arbitrary (shrinkList)
+import qualified Examples.Escrow as Escrow
+import qualified Examples.Swap as Swap
+import Data.List (nubBy, nub)
+import Data.Function (on)
+import Arith (divide_int)
 
 interpretLocal :: Request JSON.Value -> IO (Response JSON.Value)
 interpretLocal (TestRoundtripSerialization t v) =
@@ -29,7 +47,7 @@ interpretLocal (PlayTrace t c is) =
   pure
     $ RequestResponse
     $ JSON.toJSON
-    $ playTrace (Int_of_integer t) c is
+    $ playTrace (Arith.Int_of_integer t) c is
 interpretLocal (EvalValue env state val) =
   pure
     $ RequestResponse
@@ -50,20 +68,135 @@ interpretLocal (GenerateRandomValue t@(TypeId name _) size seed) =
     $ RequestResponse
     $ JSON.toJSON
     $ case name of
-      "Core.Token" -> RandomResponse.RandomValue $ JSON.toJSON $ generate' arbitraryToken
-      "Core.Party" -> RandomResponse.RandomValue $ JSON.toJSON $ generate' arbitraryParty
+      "Core.Token" -> RandomResponse.RandomValue $ JSON.toJSON $ (generate' arbitrary :: Token)
+      "Core.Party" -> RandomResponse.RandomValue $ JSON.toJSON $ (generate' arbitrary :: Party)
+      "Core.Contract" -> RandomResponse.RandomValue $ JSON.toJSON $ (generate' arbitrary :: Contract)
       _ -> RandomResponse.UnknownType t
   where
   generate' (MkGen g) = g (mkQCGen seed) size
 
+-- | Class for arbitrary values with respect to a context.
+class Arbitrary a => SemiArbitrary a where
+  -- | Generate an arbitrary value within a context.
+  semiArbitrary :: Context -> Gen a
+  semiArbitrary context =
+     case fromContext context of
+       [] -> arbitrary
+       xs -> perturb arbitrary xs
+  -- | Report values present in a context.
+  fromContext :: Context -> [a]
+  fromContext _ = []
 
-arbitraryToken :: Gen Token
-arbitraryToken =
-  frequency
-    [(50, pure $ Token "" "")
-    ,(50, Token <$> arbitrary <*> arbitrary)
-    ]
+-- | Select an element of a list with high probability, or create a non-element at random with low probability.
+perturb :: Gen a   -- ^ The generator for a random item.
+        -> [a]     -- ^ The list of pre-defined items.
+        -> Gen a   -- ^ Generator for an item
+perturb gen [] = gen
+perturb gen xs = frequency [(20, gen), (80, elements xs)]
+
+-- | Context for generating correlated Marlowe terms and state.
+data Context =
+  Context
+  {
+    parties      :: [Party]                      -- ^ Universe of parties.
+  , tokens       :: [Token]                      -- ^ Universe of tokens.
+  , amounts      :: [Arith.Int]                  -- ^ Universe of token amounts.
+  , choiceNames  :: [String]                     -- ^ Universe of choice names.
+  , chosenNums   :: [Arith.Int]                  -- ^ Universe of chosen numbers.
+  , choiceIds    :: [ChoiceId]                   -- ^ Universe of token identifiers.
+  , valueIds     :: [ValueId]                    -- ^ Universe of value identifiers.
+  , values       :: [Arith.Int]                  -- ^ Universe of values.
+  , times        :: [Arith.Int]                  -- ^ Universe of times.
+  , caccounts    :: Map (Party, Token) Arith.Int -- ^ Accounts for state.
+  , cchoices     :: Map ChoiceId Arith.Int       -- ^ Choices for state.
+  , cboundValues :: Map ValueId Arith.Int        -- ^ Bound values for state.
+  }
+
+instance Ord Party where
+  compare (Address a) (Address b) = compare a b
+  compare (Address _) (Role _) = LT
+  compare (Role _) (Address _) = GT
+  compare (Role a) (Role b) = compare a b
+
+instance Ord Token where
+  compare (Token a1 b1) (Token a2 b2) =
+    let res = compare a1 a2
+     in case res of
+      EQ -> compare b1 b2
+      _ -> res
+
+instance Ord ChoiceId where
+  compare (ChoiceId a1 b1) (ChoiceId a2 b2) =
+    let res = compare a1 a2
+     in case res of
+      EQ -> compare b1 b2
+      _ -> res
+
+instance Ord ValueId where
+  compare (ValueId a) (ValueId b) = compare a b
+
+instance Arbitrary Context where
+  arbitrary =
+    do
+      parties <- arbitrary
+      tokens <- arbitrary
+      amounts <- listOf arbitraryPositiveInteger
+      choiceNames <- listOf arbitraryChoiceName
+      chosenNums <- listOf arbitraryInteger
+      valueIds <- arbitrary
+      values <- listOf arbitraryInteger
+      times <- listOf arbitraryPositiveInteger
+      choiceIds <- listOf $ ChoiceId <$> perturb arbitraryChoiceName choiceNames <*> perturb arbitrary parties
+      caccounts <- fromList . nubBy ((==) `on` fst) <$> listOf ((,) <$> ((,) <$> perturb arbitrary parties <*> perturb arbitrary tokens) <*> perturb arbitraryPositiveInteger amounts)
+      cchoices <- fromList . nubBy ((==) `on` fst) <$> listOf ((,) <$> perturb arbitrary choiceIds <*> perturb arbitraryInteger chosenNums)
+      cboundValues <- fromList . nubBy ((==) `on` fst) <$> listOf ((,) <$> perturb arbitrary valueIds <*> perturb arbitraryInteger values)
+      pure Context{..}
+  shrink context@Context{..} =
+    [context {parties = parties'} | parties' <- shrink parties]
+      ++ [context {tokens = tokens'} | tokens' <- shrink tokens]
+      ++ [context {amounts = amounts'} | amounts' <- shrink amounts]
+      ++ [context {choiceNames = choiceNames'} | choiceNames' <- shrinkList shrinkChoiceName choiceNames]
+      ++ [context {chosenNums = chosenNums'} | chosenNums' <- shrink chosenNums]
+      ++ [context {valueIds = valueIds'} | valueIds' <- shrink valueIds]
+      ++ [context {values = values'} | values' <- shrink values]
+      ++ [context {times = times'} | times' <- shrink times]
+      ++ [context {choiceIds = choiceIds'} | choiceIds' <- shrink choiceIds]
+      ++ [context {caccounts = caccounts'} | caccounts' <- shrink caccounts]
+      ++ [context {cchoices = cchoices'} | cchoices' <- shrink cchoices]
+      ++ [context {cboundValues = cboundValues'} | cboundValues' <- shrink cboundValues]
+
+instance Arbitrary Arith.Int where
+  arbitrary = arbitraryInteger
+
+instance SemiArbitrary Arith.Int where
+  fromContext = times
 
+instance Arbitrary Token where
+  arbitrary =
+     do
+       isAda <- arbitrary
+       if isAda
+         then pure $ Token "" ""
+         else Token <$> arbitrary <*> arbitrary
+  shrink (Token c n)
+    | c == "" && n == "" = []
+    | otherwise                       = Token "" "" : [Token c' n' | c' <- shrink c, n' <- shrink n]
+
+instance SemiArbitrary Token where
+  fromContext = tokens
+
+instance Arbitrary Party where
+  arbitrary =
+    do
+       isPubKeyHash <- frequency [(2, pure True), (8, pure False)]
+       if isPubKeyHash
+         then Address <$> arbitrary
+         else Role <$> arbitraryFibonacci randomRoleNames
+  shrink (Address _) = Role <$> randomRoleNames
+  shrink (Role _)      = Role <$> randomRoleNames
+
+instance SemiArbitrary Party where
+  fromContext = parties
 
 -- | Some role names.
 randomRoleNames :: [String]
@@ -87,13 +220,287 @@ randomRoleNames =
   , "Alcippe Alende Blanka Roland Dafne"  -- NB: Too long for Cardano ledger.
   ]
 
+instance Arbitrary Contract where
+  arbitrary = frequency [(95, semiArbitrary =<< arbitrary), (5, fst <$> goldenContract)]
+  shrink (Pay a p t x c) = [Pay a' p t x c | a' <- shrink a] ++ [Pay a p' t x c | p' <- shrink p] ++ [Pay a p t' x c | t' <- shrink t] ++ [Pay a p t x' c | x' <- shrink x] ++ [Pay a p t x c' | c' <- shrink c]
+  shrink (If o x y) = [If o' x y | o' <- shrink o] ++ [If o x' y | x' <- shrink x] ++ [If o x y' | y' <- shrink y]
+  shrink (When a t c) = [When a' t c | a' <- shrink a] ++ [When a t' c | t' <- shrink t] ++ [When a t c' | c' <- shrink c]
+  shrink (Let v x c) = [Let v' x c | v' <- shrink v] ++ [Let v x' c | x' <- shrink x] ++ [Let v x c' | c' <- shrink c]
+  shrink (Assert o c) = [Assert o' c | o' <- shrink o] ++ [Assert o c' | c' <- shrink c]
+  shrink _ = []
+
+-- | Generate one of the golden contracts and its initial state.
+goldenContract :: Gen (Contract, State_ext ())
+goldenContract = (,) <$> elements goldenContracts <*> pure (State_ext [] [] [] 0 ())
+
+goldenContracts :: [Contract]
+goldenContracts = [ Swap.swapExample, Escrow.escrowExample ]
+
+instance SemiArbitrary Contract where
+  semiArbitrary context = sized \size -> arbitraryContractSized (min size 100 `div` 20) context -- Keep tests from growing too large to execute by capping the maximum contract depth at 5
+
+-- | Generate a random case, weighted towards different contract constructs.
+arbitraryCaseWeighted :: [(Int, Int, Int, Int, Int, Int)]  -- ^ The weights for contract terms.
+                      -> Context                           -- ^ The Marlowe context.
+                      -> Gen Case                          -- ^ Generator for a case.
+arbitraryCaseWeighted w context =
+  Case <$> semiArbitrary context <*> arbitraryContractWeighted w context
+
+-- | Generate an arbitrary contract, weighted towards different contract constructs.
+arbitraryContractWeighted :: [(Int, Int, Int, Int, Int, Int)]  -- ^ The weights of contract terms, which must eventually include `Close` as a posibility.
+                          -> Context                           -- ^ The Marlowe context.
+                          -> Gen Contract                      -- ^ Generator for a contract.
+arbitraryContractWeighted ((wClose, wPay, wIf, wWhen, wLet, wAssert) : w) context =
+  frequency
+    [
+      (wClose , pure Close)
+    , (wPay   , Pay <$> semiArbitrary context <*> semiArbitrary context <*> semiArbitrary context <*> semiArbitrary context <*> arbitraryContractWeighted w context)
+    , (wIf    , If <$> semiArbitrary context <*> arbitraryContractWeighted w context <*> arbitraryContractWeighted w context)
+    , (wWhen  , When <$> listOf (arbitraryCaseWeighted w context) `suchThat` ((<= length w) . length) <*> semiArbitrary context <*> arbitraryContractWeighted w context)
+    , (wLet   , Let <$> semiArbitrary context <*> semiArbitrary context <*> arbitraryContractWeighted w context)
+    , (wAssert, Assert <$> semiArbitrary context <*> arbitraryContractWeighted w context)
+    ]
+arbitraryContractWeighted [] _ = pure Close
+
+-- | Default weights for contract terms.
+defaultContractWeights :: (Int, Int, Int, Int, Int, Int)
+defaultContractWeights = (35, 20, 10, 15, 20, 5)
 
-arbitraryParty :: Gen Party
-arbitraryParty = do
-  isAddress <- frequency [(2, pure True), (8, pure False)]
-  if isAddress
-    then Address <$> arbitrary
-    else Role <$> arbitraryFibonacci randomRoleNames
+-- | Generate a semi-random contract of a given depth.
+arbitraryContractSized :: Int           -- ^ The maximum depth.
+                       -> Context       -- ^ The Marlowe context.
+                       -> Gen Contract  -- ^ Generator for a contract.
+arbitraryContractSized = arbitraryContractWeighted . (`replicate` defaultContractWeights)
+
+instance Arbitrary Value where
+  arbitrary =  sized
+    \case n | n <= 1 ->
+              frequency
+                [ (80, genConstant)
+                , (10, genTimeIntervalStart)
+                , (10, genTimeIntervalEnd)
+                ]
+            | n == 2 ->
+              frequency
+                [ (45, genConstant)
+                , (8, genTimeIntervalStart)
+                , (8, genTimeIntervalEnd)
+                , (13, genNegValue)
+                , (13, genUseValue)
+                , (13, genChoiceValue)
+                ]
+            | otherwise ->
+              frequency
+                [ ( 8, genAvailableMoney)
+                , (14, genConstant)
+                , ( 8, resize (n - 1) $ genNegValue)
+                , ( 8, resize (n - 2) $ genAddValue)
+                , ( 8, resize (n - 2) $ genSubValue)
+                , ( 8, resize (n - 2) $ genMulValue)
+                , ( 8, resize (n - 2) $ genDivValue)
+                , (10, genChoiceValue)
+                , ( 6, genTimeIntervalStart)
+                , ( 6, genTimeIntervalEnd)
+                , ( 8, genUseValue)
+                , ( 8, resize (n - 3) $ genCond)
+                ]
+    where
+      genAvailableMoney = AvailableMoney <$> arbitrary <*> arbitrary
+      genConstant = Constant <$> arbitraryPositiveInteger
+      genNegValue = NegValue <$> arbitrary
+      genAddValue = AddValue <$> arbitrary <*> arbitrary
+      genSubValue = SubValue <$> arbitrary <*> arbitrary
+      genMulValue = MulValue <$> arbitrary <*> arbitrary
+      genDivValue = DivValue <$> arbitrary <*> arbitrary
+      genChoiceValue = ChoiceValue <$> arbitrary
+      genTimeIntervalStart = pure TimeIntervalStart
+      genTimeIntervalEnd = pure TimeIntervalEnd
+      genUseValue = UseValue <$> arbitrary
+      genCond = Cond <$> arbitrary <*> arbitrary <*> arbitrary
+
+instance SemiArbitrary Value where
+  semiArbitrary context =
+    frequency
+      [
+        ( 8, uncurry AvailableMoney <$> perturb arbitrary (keys $ caccounts context))
+      , (14, Constant <$> semiArbitrary context)
+      , ( 8, NegValue <$> semiArbitrary context)
+      , ( 8, AddValue <$> semiArbitrary context <*> semiArbitrary context)
+      , ( 8, SubValue <$> semiArbitrary context <*> semiArbitrary context)
+      , ( 8, MulValue <$> semiArbitrary context <*> semiArbitrary context)
+      , ( 8, DivValue <$> semiArbitrary context <*> semiArbitrary context)
+      , (10, ChoiceValue <$> semiArbitrary context)
+      , ( 6, pure TimeIntervalStart)
+      , ( 6, pure TimeIntervalEnd)
+      , ( 8, UseValue <$> semiArbitrary context)
+      , ( 8, Cond <$> semiArbitrary context <*> semiArbitrary context <*> semiArbitrary context)
+      ]
+
+instance Arbitrary Observation where
+  arbitrary =
+    frequency
+      [
+        ( 8, AndObs <$> arbitrary <*> arbitrary)
+      , ( 8, OrObs <$> arbitrary <*> arbitrary)
+      , ( 8, NotObs <$> arbitrary)
+      , (16, ChoseSomething <$> arbitrary)
+      , ( 8, ValueGE <$> arbitrary <*> arbitrary)
+      , ( 8, ValueGT <$> arbitrary <*> arbitrary)
+      , ( 8, ValueLT <$> arbitrary <*> arbitrary)
+      , ( 8, ValueLE <$> arbitrary <*> arbitrary)
+      , ( 8, ValueEQ <$> arbitrary <*> arbitrary)
+      , (10, pure TrueObs)
+      , (10, pure FalseObs)
+      ]
+  shrink (AndObs x y)       = [AndObs x' y | x' <- shrink x] ++ [AndObs x y' | y' <- shrink y]
+  shrink (OrObs x y)        = [OrObs x' y | x' <- shrink x] ++ [OrObs x y' | y' <- shrink y]
+  shrink (NotObs x)         = NotObs <$> shrink x
+  shrink (ChoseSomething c) = ChoseSomething <$> shrink c
+  shrink (ValueGE x y)      = [ValueGE x' y | x' <- shrink x] ++ [ValueGE x y' | y' <- shrink y]
+  shrink (ValueGT x y)      = [ValueGT x' y | x' <- shrink x] ++ [ValueGT x y' | y' <- shrink y]
+  shrink (ValueLT x y)      = [ValueLT x' y | x' <- shrink x] ++ [ValueLT x y' | y' <- shrink y]
+  shrink (ValueLE x y)      = [ValueLE x' y | x' <- shrink x] ++ [ValueLE x y' | y' <- shrink y]
+  shrink (ValueEQ x y)      = [ValueEQ x' y | x' <- shrink x] ++ [ValueEQ x y' | y' <- shrink y]
+  shrink _                  = []
+
+instance SemiArbitrary Observation where
+  semiArbitrary context =
+    frequency
+      [
+        ( 8, AndObs <$> semiArbitrary context <*> semiArbitrary context)
+      , ( 8, OrObs <$> semiArbitrary context <*> semiArbitrary context)
+      , ( 8, NotObs <$> semiArbitrary context)
+      , (16, ChoseSomething <$> semiArbitrary context)
+      , ( 8, ValueGE <$> semiArbitrary context <*> semiArbitrary context)
+      , ( 8, ValueGT <$> semiArbitrary context <*> semiArbitrary context)
+      , ( 8, ValueLT <$> semiArbitrary context <*> semiArbitrary context)
+      , ( 8, ValueLE <$> semiArbitrary context <*> semiArbitrary context)
+      , ( 8, ValueEQ <$> semiArbitrary context <*> semiArbitrary context)
+      , (10, pure TrueObs)
+      , (10, pure FalseObs)
+      ]
+
+instance Arbitrary ChoiceId where
+  arbitrary = ChoiceId <$> arbitraryChoiceName <*> arbitrary
+  shrink (ChoiceId n p) = [ChoiceId n' p' | n' <- shrinkChoiceName n, p' <- shrink p]
+
+instance SemiArbitrary ChoiceId where
+  fromContext = choiceIds
+
+instance Arbitrary Case where
+  arbitrary = semiArbitrary =<< arbitrary
+  shrink (Case a c)           = [Case a' c | a' <- shrink a] ++ [Case a c' | c' <- shrink c]
+
+instance SemiArbitrary Case where
+  semiArbitrary context = Case <$> semiArbitrary context <*> semiArbitrary context
+
+-- | Some value identifiers.
+randomValueIds :: [ValueId]
+randomValueIds =
+  [
+    ValueId "x"
+  , ValueId "id"
+  , ValueId "lab"
+  , ValueId "idea"
+  , ValueId "story"
+  , ValueId "memory"
+  , ValueId "fishing"
+  , ValueId ""
+  , ValueId "drawing"
+  , ValueId "reaction"
+  , ValueId "difference"
+  , ValueId "replacement"
+  , ValueId "paper apartment"
+  , ValueId "leadership information"
+  , ValueId "entertainment region assumptions"
+  , ValueId "candidate apartment reaction replacement"  -- NB: Too long for ledger.
+  ]
+
+instance Arbitrary ValueId where
+  arbitrary = arbitraryFibonacci randomValueIds
+  shrink = shrinkString (\(ValueId x) -> x) randomValueIds
+
+instance SemiArbitrary ValueId where
+  fromContext = valueIds
+
+instance Arbitrary Payee where
+  arbitrary =
+    do
+      isParty <- arbitrary
+      if isParty
+        then Party <$> arbitrary
+        else Account <$> arbitrary
+  shrink (Party x)   = Party <$> shrink x
+  shrink (Account x) = Account <$> shrink x
+
+instance SemiArbitrary Payee where
+  semiArbitrary context =
+      do
+        party <- semiArbitrary context
+        isParty <- arbitrary
+        pure
+          $ if isParty
+              then Party party
+              else Account party
+
+instance Arbitrary Action where
+  arbitrary =
+    frequency
+      [
+        (3, Deposit <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary)
+      , (6, Choice <$> arbitrary <*> arbitrary `suchThat` ((< 5) . length))
+      , (1, Notify <$> arbitrary)
+      ]
+  shrink (Deposit a p t x) = [Deposit a' p t x | a' <- shrink a] ++ [Deposit a p' t x | p' <- shrink p] ++ [Deposit a p t' x | t' <- shrink t] ++ [Deposit a p t x' | x' <- shrink x]
+  shrink (Choice c b) = [Choice c' b | c' <- shrink c] ++ [Choice c b' | b' <- shrink b]
+  shrink (Notify o) = Notify <$> shrink o
+
+instance SemiArbitrary Action where
+  semiArbitrary context@Context{..} =
+    let
+      arbitraryDeposit =
+        do
+          (account, token) <- perturb arbitrary $ keys caccounts
+          party <- semiArbitrary context
+          Deposit account party token <$> semiArbitrary context
+      arbitraryChoice = Choice <$> semiArbitrary context <*> semiArbitrary context
+    in
+      frequency
+        [
+          (3, arbitraryDeposit)
+        , (6, arbitraryChoice)
+        , (1, Notify <$> semiArbitrary context)
+        ]
+
+instance Arbitrary Bound where
+  arbitrary =
+    do
+      lower <- arbitraryInteger
+      extent <- arbitraryNonnegativeInteger
+      pure $ Bound lower (lower + extent)
+  shrink (Bound lower upper) =
+    let
+      mid = (lower + upper) `divide_int` 2
+    in
+      filter (/= Bound lower upper)
+        $ nub
+        [
+          Bound lower lower
+        , Bound lower mid
+        , Bound mid   mid
+        , Bound mid   upper
+        , Bound upper upper
+        ]
+
+instance SemiArbitrary Bound where
+  semiArbitrary context =
+      do
+        lower <- semiArbitrary context
+        extent <- arbitraryNonnegativeInteger
+        pure $ Bound lower (lower + extent)
+
+instance SemiArbitrary [Bound] where
+  semiArbitrary context = listOf $ semiArbitrary context
 
 localJsonRoundtripSerialization :: TypeId -> JSON.Value -> SerializationResponse JSON.Value
 localJsonRoundtripSerialization t@(TypeId name proxy) v = case fromTypeName name of
@@ -104,4 +511,3 @@ localJsonRoundtripSerialization t@(TypeId name proxy) v = case fromTypeName name
     roundtrip _  = case JSON.fromJSON v :: Result a of
             Error str -> SerializationError str
             Success c ->  SerializationSuccess $ JSON.toJSON c
-