diff --git a/isabelle/CodeExports/CodeExports.thy b/isabelle/CodeExports/CodeExports.thy
index 9ff0cfc5..202a23f2 100644
--- a/isabelle/CodeExports/CodeExports.thy
+++ b/isabelle/CodeExports/CodeExports.thy
@@ -11,6 +11,7 @@ theory CodeExports
 
 imports
   Core.Semantics
+  Examples.Escrow
   Examples.Swap
   "HOL-Library.Code_Target_Numeral"
   HOL.String
@@ -45,6 +46,8 @@ text \<open>With a \<^bold>\<open>code\_identifier\<close> we hint what the name
 code_identifier
   code_module Swap \<rightharpoonup> (Haskell) Examples.Swap
 
+code_identifier
+  code_module Escrow \<rightharpoonup> (Haskell) Examples.Escrow
 
 text \<open>We export all the constants in one statement, because they don't add up, if you export two times,
 the second export will overwrite the first one.\<close>
@@ -69,6 +72,16 @@ export_code
   validAndPositive_state
 
   \<comment> \<open> Export examples to be used as oracle specificaiton tests\<close>
+  escrowExample
+  everythingIsAlrightTransactions
+  everythingIsAlrightPayments
+  confirmProblemTransactions
+  confirmProblemPayments
+  dismissClaimTransactions
+  dismissClaimPayments
+  confirmClaimTransactions
+  confirmClaimPayments
+
   swapExample
   happyPathTransactions
   happyPathPayments
diff --git a/isabelle/Doc/Specification/Examples.thy b/isabelle/Doc/Specification/Examples.thy
index 2c8ef0a2..87ebc8f2 100644
--- a/isabelle/Doc/Specification/Examples.thy
+++ b/isabelle/Doc/Specification/Examples.thy
@@ -1,6 +1,6 @@
 (*<*)
 theory Examples
-imports Examples.Swap
+imports Examples.Escrow Examples.Swap
 begin
 (*>*)
 
@@ -11,4 +11,4 @@ with their corresponding guarantees:"
 
 (*<*)
 end
-(*>*)
\ No newline at end of file
+(*>*)
diff --git a/isabelle/Doc/Specification/Specification.thy b/isabelle/Doc/Specification/Specification.thy
index 67df29ef..6d9566c7 100644
--- a/isabelle/Doc/Specification/Specification.thy
+++ b/isabelle/Doc/Specification/Specification.thy
@@ -33,7 +33,7 @@ for both the intended and not intended behaviour (in the form of bugs or exploit
 text \<open>To reduce the probability of not intended behaviour, the Marlowe DSL is designed with simplicity
 in mind. Without loops, recursion, or other features that general purposes smart-contract languages
 (E.g: Plutus, Solidity) have, it is easier to make certain claims. Each Marlowe contract can be
-reasoned with a static analizer to avoid common pitfalls such as trying to Pay more money than the
+reasoned with a static analyzer to avoid common pitfalls such as trying to Pay more money than the
 available. And the \<^emph>\<open>executable semantics\<close> that dictates the logic of \<^bold>\<open>all\<close> Marlowe contracts is
 formalized with the proof-assistant Isabelle.
 \<close>
diff --git a/isabelle/Doc/Specification/document/root.tex b/isabelle/Doc/Specification/document/root.tex
index 13d31227..76427f8b 100644
--- a/isabelle/Doc/Specification/document/root.tex
+++ b/isabelle/Doc/Specification/document/root.tex
@@ -84,6 +84,7 @@
 \appendix
 \input{Examples.tex}
 \input{Swap.tex}
+\input{Escrow.tex}
 \input{ByteString.tex}
 \input{OptBoundTimeInterval.tex}
 \input{CodeExports.tex}
diff --git a/isabelle/Examples/Escrow.thy b/isabelle/Examples/Escrow.thy
new file mode 100644
index 00000000..64fdbc8d
--- /dev/null
+++ b/isabelle/Examples/Escrow.thy
@@ -0,0 +1,285 @@
+(*<*)
+theory Escrow
+  imports Core.Semantics Core.TransactionBound Core.Timeout
+begin
+
+(*>*)
+section \<open>Escrow contract\<close>
+
+text \<open>An escrow contract allows a \<^bold>\<open>Buyer\<close> to purchase an item for a price.
+The money is deposited in an escrow, waiting for some feedback from the  \<^bold>\<open>Buyer\<close>. If the  \<^bold>\<open>Buyer\<close> and  \<^bold>\<open>Seller\<close> don't agree, a  \<^bold>\<open>Mediator\<close> will resolve the conflict.
+\<close>
+
+subsection \<open>Contract definition\<close>
+
+text \<open>The participants of the contract are:\<close>
+definition "seller = Role (BS ''Seller'')"
+definition "buyer = Role (BS ''Buyer'')"
+definition "mediator = Role (BS ''Mediator'')"
+text \<open>An escrow contract takes as arguments the price, token
+and the deadlines that apply for the payment, the complaint, the dispute and
+the mediation.
+\<close>
+
+record EscrowArgs =
+  price             :: Value
+  token             :: Token
+  paymentDeadline   :: Timeout
+  complaintDeadline :: Timeout
+  disputeDeadline   :: Timeout
+  mediationDeadline :: Timeout
+
+text \<open>The contract is built in multiple steps. The innermost step is the
+mediation step, where the mediator either confirms or dismisses a claim about
+a problem with the transaction. In case the mediator dismisses the claim the
+seller is paid, in case the mediator confirms the claim, the contract is closed
+and the buyer refunded implicitly:
+\<close>
+
+fun mediation :: "EscrowArgs \<Rightarrow> Contract" where
+  "mediation args =
+    When
+      [ Case (Choice (ChoiceId (BS ''Dismiss claim'') mediator) [Bound 0 0])
+          (Pay buyer (Account seller) (token args) (price args) Close)
+      , Case (Choice (ChoiceId (BS ''Confirm claim'') mediator) [Bound 1 1]) Close
+      ] (mediationDeadline args) Close"
+
+text \<open>In case a problem is reported by the buyer, the seller has to either confirm or dispute the
+problem. In case the seller confirms the problem, the buyer is refunded implicitly.
+Disputing the problem leads to the mediation step defined above.\<close>
+
+fun dispute :: "EscrowArgs \<Rightarrow> Contract" where
+  "dispute args =
+    When
+      [ Case (Choice (ChoiceId (BS ''Confirm problem'') seller) [Bound 1 1]) Close
+      , Case (Choice (ChoiceId (BS ''Dispute problem'') seller) [Bound 0 0]) (mediation args)
+      ] (disputeDeadline args) Close"
+
+text \<open>The buyer can either report that everything is alright with transaction or a problem. When
+a problem is reported the funds are placed in the buyer's account and the contract continues with the
+dispute step defined above.\<close>
+
+fun report :: "EscrowArgs \<Rightarrow> Contract" where
+  "report args =
+    When
+      [ Case (Choice (ChoiceId (BS ''Everything is alright'') buyer) [Bound 0 0]) Close
+      , Case (Choice (ChoiceId (BS ''Report problem'') buyer) [Bound 1 1])
+          (Pay (seller) (Account buyer) (token args) (price args) (dispute args))
+      ] (complaintDeadline args) Close"
+
+text \<open>The escrow contract waits for the buyer to deposit and then continues with the report step
+defined above.\<close>
+
+fun escrow :: "EscrowArgs \<Rightarrow> Contract" where
+  "escrow args =
+    When
+      [ Case (Deposit seller buyer (token args) (price args)) (report args) ]
+      (paymentDeadline args) Close"
+
+(*<*)
+definition "exampleArgs =
+  \<lparr> price = Constant 10
+  , token = Token (BS '''') (BS '''')
+  , paymentDeadline = 1664812800000
+  , complaintDeadline = 1664816400000
+  , disputeDeadline = 1664820420000
+  , mediationDeadline = 1664824440000
+  \<rparr>"
+
+definition "escrowExample = escrow exampleArgs"
+
+(*>*)
+subsection \<open>Possible Outcomes\<close>
+
+text \<open>There are four possible outcomes for the escrow contract.\<close>
+
+subsubsection \<open>Everything is alright\<close>
+
+text \<open>
+Steps:
+\begin{enumerate}
+\item Buyer deposits funds into seller's account.
+\item Buyer reports that everything is alright.
+\end{enumerate}
+Outcome: Seller receives purchase price.
+\<close>
+
+(*<*)
+definition
+  "everythingIsAlrightTransactions =
+    [
+      \<comment> \<open>First party deposit\<close>
+      \<lparr> interval = (1664812600000, 1664812700000)
+      , inputs = [ IDeposit seller buyer (token exampleArgs) 10 ]
+      \<rparr>
+   ,  \<lparr> interval = (1664812900000, 1664813100000)
+      , inputs = [ IChoice (ChoiceId (BS ''Everything is alright'') buyer) 0 ]
+      \<rparr>
+    ]
+  "
+
+definition
+  "everythingIsAlrightPayments =
+    [ Payment seller (Party seller) (token exampleArgs) 10 ]
+  "
+
+proposition
+ "playTrace 0 escrowExample everythingIsAlrightTransactions = TransactionOutput txOut
+  \<Longrightarrow>
+     txOutContract txOut = Close
+     \<and> txOutPayments txOut = everythingIsAlrightPayments
+     \<and> txOutWarnings txOut = []"
+     apply (code_simp)
+     apply (auto simp add: everythingIsAlrightPayments_def
+              seller_def buyer_def exampleArgs_def)
+     done
+
+(*>*)
+subsubsection \<open>Confirm problem\<close>
+text \<open>
+Steps:
+\begin{enumerate}
+\item Buyer deposits funds into seller's account.
+\item Buyer reports that there is a problem.
+\item Seller confirms that there is a problem.
+\end{enumerate}
+Outcome: Buyer receives refund.
+\<close>
+
+(*<*)
+definition
+  "confirmProblemTransactions =
+    [
+      \<comment> \<open>First party deposit\<close>
+      \<lparr> interval = (1664812600000, 1664812700000)
+      , inputs = [ IDeposit seller buyer (token exampleArgs) 10 ]
+      \<rparr>
+   ,  \<lparr> interval = (1664812900000, 1664813100000)
+      , inputs = [ IChoice (ChoiceId (BS ''Report problem'') buyer) 1 ]
+      \<rparr>
+   ,  \<lparr> interval = (1664817400000, 1664817400000)
+      , inputs = [ IChoice (ChoiceId (BS ''Confirm problem'') seller) 1 ]
+      \<rparr>
+    ]
+  "
+
+definition
+  "confirmProblemPayments =
+    [ Payment seller (Account buyer) (token exampleArgs) 10
+    , Payment buyer (Party buyer) (token exampleArgs) 10
+    ]
+  "
+
+proposition
+ "playTrace 0 escrowExample confirmProblemTransactions = TransactionOutput txOut
+  \<Longrightarrow>
+     txOutContract txOut = Close
+     \<and> txOutPayments txOut = confirmProblemPayments
+     \<and> txOutWarnings txOut = []"
+     apply (code_simp)
+     apply (auto simp add: confirmProblemPayments_def
+              seller_def buyer_def mediator_def exampleArgs_def)
+     done
+
+(*>*)
+subsubsection \<open>Dismiss claim\<close>
+text \<open>
+\begin{enumerate}
+\item Buyer deposits funds into seller's account.
+\item Buyer reports that there is a problem.
+\item Seller disputes that there is a problem.
+\item Mediator dismisses the buyer's claim.
+\end{enumerate}
+Outcome: Seller receives purchase price.
+\<close>
+
+(*<*)
+definition
+  "dismissClaimTransactions =
+    [
+      \<comment> \<open>First party deposit\<close>
+      \<lparr> interval = (1664812600000, 1664812700000)
+      , inputs = [ IDeposit seller buyer (token exampleArgs) 10 ]
+      \<rparr>
+   ,  \<lparr> interval = (1664812900000, 1664813100000)
+      , inputs = [ IChoice (ChoiceId (BS ''Report problem'') buyer) 1 ]
+      \<rparr>
+   ,  \<lparr> interval = (1664817400000, 1664817400000)
+      , inputs = [ IChoice (ChoiceId (BS ''Dispute problem'') seller) 0 ]
+      \<rparr>
+   ,  \<lparr> interval = (1664821400000, 1664822400000)
+      , inputs = [ IChoice (ChoiceId (BS ''Dismiss claim'') mediator) 0 ]
+      \<rparr>
+    ]
+  "
+
+definition
+  "dismissClaimPayments =
+    [ Payment seller (Account buyer) (token exampleArgs) 10
+    , Payment buyer (Account seller) (token exampleArgs) 10
+    , Payment seller (Party seller) (token exampleArgs) 10
+    ]
+  "
+
+proposition
+ "playTrace 0 escrowExample dismissClaimTransactions = TransactionOutput txOut
+  \<Longrightarrow>
+     txOutContract txOut = Close
+     \<and> txOutPayments txOut = dismissClaimPayments
+     \<and> txOutWarnings txOut = []"
+     apply (code_simp)
+     apply (auto simp add: dismissClaimPayments_def
+              seller_def buyer_def mediator_def exampleArgs_def)
+     done
+
+(*>*)
+subsubsection \<open>Confirm claim\<close>
+text \<open>
+\begin{enumerate}
+\item Buyer deposits funds into seller's account.
+\item Buyer reports that there is a problem.
+\item Seller disputes that there is a problem.
+\item Mediator confirms the buyer's claim.
+\end{enumerate}
+Outcome: Buyer receives refund.
+\<close>
+
+(*<*)
+definition
+  "confirmClaimTransactions =
+    [
+      \<comment> \<open>First party deposit\<close>
+      \<lparr> interval = (1664812600000, 1664812700000)
+      , inputs = [ IDeposit seller buyer (token exampleArgs) 10 ]
+      \<rparr>
+   ,  \<lparr> interval = (1664812900000, 1664813100000)
+      , inputs = [ IChoice (ChoiceId (BS ''Report problem'') buyer) 1 ]
+      \<rparr>
+   ,  \<lparr> interval = (1664817400000, 1664817400000)
+      , inputs = [ IChoice (ChoiceId (BS ''Dispute problem'') seller) 0 ]
+      \<rparr>
+   ,  \<lparr> interval = (1664821400000, 1664822400000)
+      , inputs = [ IChoice (ChoiceId (BS ''Confirm claim'') mediator) 1 ]
+      \<rparr>
+    ]
+  "
+
+definition
+  "confirmClaimPayments =
+    [ Payment seller (Account buyer) (token exampleArgs) 10
+    , Payment buyer (Party buyer) (token exampleArgs) 10
+    ]
+  "
+
+proposition
+ "playTrace 0 escrowExample confirmClaimTransactions = TransactionOutput txOut
+  \<Longrightarrow>
+     txOutContract txOut = Close
+     \<and> txOutPayments txOut = confirmClaimPayments
+     \<and> txOutWarnings txOut = []"
+     apply (code_simp)
+     apply (auto simp add: confirmClaimPayments_def
+              seller_def buyer_def mediator_def exampleArgs_def)
+     done
+end
+(*>*)
\ No newline at end of file
diff --git a/isabelle/ROOT b/isabelle/ROOT
index d6692d83..fe885e9c 100644
--- a/isabelle/ROOT
+++ b/isabelle/ROOT
@@ -53,6 +53,7 @@ session Examples in "Examples" = HOL +
     "HOL-Library"
     "Core"
   theories
+    Escrow
     Swap
 
 session CodeExports in "CodeExports" = HOL +
@@ -100,6 +101,7 @@ session Specification in "Doc/Specification" = HOL +
     "Core.OptBoundTimeInterval"
     "CodeExports.CodeExports"
     "Util.ByteString"
+    "Examples.Escrow"
     "Examples.Swap"
   document_files
     "root.tex"
diff --git a/isabelle/generated/Examples/Escrow.hs b/isabelle/generated/Examples/Escrow.hs
new file mode 100644
index 00000000..6e1065e8
--- /dev/null
+++ b/isabelle/generated/Examples/Escrow.hs
@@ -0,0 +1,545 @@
+{-# LANGUAGE EmptyDataDecls, RankNTypes, ScopedTypeVariables #-}
+
+module
+  Examples.Escrow(EscrowArgs_ext, escrowExample, confirmClaimPayments,
+                   dismissClaimPayments, confirmProblemPayments,
+                   confirmClaimTransactions, dismissClaimTransactions,
+                   confirmProblemTransactions, everythingIsAlrightPayments,
+                   everythingIsAlrightTransactions)
+  where {
+
+import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**),
+  (>>=), (>>), (=<<), (&&), (||), (^), (^^), (.), ($), ($!), (++), (!!), Eq,
+  error, id, return, not, fst, snd, map, filter, concat, concatMap, reverse,
+  zip, null, takeWhile, dropWhile, all, any, Integer, negate, abs, divMod,
+  String, Bool(True, False), Maybe(Nothing, Just));
+import qualified Prelude;
+import qualified Semantics;
+import qualified Stringa;
+import qualified SemanticsTypes;
+import qualified Arith;
+
+data EscrowArgs_ext a =
+  EscrowArgs_ext SemanticsTypes.Value SemanticsTypes.Token Arith.Int Arith.Int
+    Arith.Int Arith.Int a
+  deriving (Prelude.Read, Prelude.Show);
+
+buyer :: SemanticsTypes.Party;
+buyer =
+  SemanticsTypes.Role
+    (Stringa.implode
+      [Stringa.Char False True False False False False True False,
+        Stringa.Char True False True False True True True False,
+        Stringa.Char True False False True True True True False,
+        Stringa.Char True False True False False True True False,
+        Stringa.Char False True False False True True True False]);
+
+paymentDeadline :: forall a. EscrowArgs_ext a -> Arith.Int;
+paymentDeadline
+  (EscrowArgs_ext price token paymentDeadline complaintDeadline disputeDeadline
+    mediationDeadline more)
+  = paymentDeadline;
+
+token :: forall a. EscrowArgs_ext a -> SemanticsTypes.Token;
+token (EscrowArgs_ext price token paymentDeadline complaintDeadline
+        disputeDeadline mediationDeadline more)
+  = token;
+
+price :: forall a. EscrowArgs_ext a -> SemanticsTypes.Value;
+price (EscrowArgs_ext price token paymentDeadline complaintDeadline
+        disputeDeadline mediationDeadline more)
+  = price;
+
+seller :: SemanticsTypes.Party;
+seller =
+  SemanticsTypes.Role
+    (Stringa.implode
+      [Stringa.Char True True False False True False True False,
+        Stringa.Char True False True False False True True False,
+        Stringa.Char False False True True False True True False,
+        Stringa.Char False False True True False True True False,
+        Stringa.Char True False True False False True True False,
+        Stringa.Char False True False False True True True False]);
+
+complaintDeadline :: forall a. EscrowArgs_ext a -> Arith.Int;
+complaintDeadline
+  (EscrowArgs_ext price token paymentDeadline complaintDeadline disputeDeadline
+    mediationDeadline more)
+  = complaintDeadline;
+
+disputeDeadline :: forall a. EscrowArgs_ext a -> Arith.Int;
+disputeDeadline
+  (EscrowArgs_ext price token paymentDeadline complaintDeadline disputeDeadline
+    mediationDeadline more)
+  = disputeDeadline;
+
+mediationDeadline :: forall a. EscrowArgs_ext a -> Arith.Int;
+mediationDeadline
+  (EscrowArgs_ext price token paymentDeadline complaintDeadline disputeDeadline
+    mediationDeadline more)
+  = mediationDeadline;
+
+mediator :: SemanticsTypes.Party;
+mediator =
+  SemanticsTypes.Role
+    (Stringa.implode
+      [Stringa.Char True False True True False False True False,
+        Stringa.Char True False True False False True True False,
+        Stringa.Char False False True False False True True False,
+        Stringa.Char True False False True False True True False,
+        Stringa.Char True False False False False True True False,
+        Stringa.Char False False True False True True True False,
+        Stringa.Char True True True True False True True False,
+        Stringa.Char False True False False True True True False]);
+
+mediation :: EscrowArgs_ext () -> SemanticsTypes.Contract;
+mediation args =
+  SemanticsTypes.When
+    [SemanticsTypes.Case
+       (SemanticsTypes.Choice
+         (SemanticsTypes.ChoiceId
+           (Stringa.implode
+             [Stringa.Char False False True False False False True False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char True True False False True True True False,
+               Stringa.Char True False True True False True True False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char True True False False True True True False,
+               Stringa.Char True True False False True True True False,
+               Stringa.Char False False False False False True False False,
+               Stringa.Char True True False False False True True False,
+               Stringa.Char False False True True False True True False,
+               Stringa.Char True False False False False True True False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char True False True True False True True False])
+           mediator)
+         [SemanticsTypes.Bound Arith.zero_int Arith.zero_int])
+       (SemanticsTypes.Pay buyer (SemanticsTypes.Account seller) (token args)
+         (price args) SemanticsTypes.Close),
+      SemanticsTypes.Case
+        (SemanticsTypes.Choice
+          (SemanticsTypes.ChoiceId
+            (Stringa.implode
+              [Stringa.Char True True False False False False True False,
+                Stringa.Char True True True True False True True False,
+                Stringa.Char False True True True False True True False,
+                Stringa.Char False True True False False True True False,
+                Stringa.Char True False False True False True True False,
+                Stringa.Char False True False False True True True False,
+                Stringa.Char True False True True False True True False,
+                Stringa.Char False False False False False True False False,
+                Stringa.Char True True False False False True True False,
+                Stringa.Char False False True True False True True False,
+                Stringa.Char True False False False False True True False,
+                Stringa.Char True False False True False True True False,
+                Stringa.Char True False True True False True True False])
+            mediator)
+          [SemanticsTypes.Bound Arith.one_int Arith.one_int])
+        SemanticsTypes.Close]
+    (mediationDeadline args) SemanticsTypes.Close;
+
+dispute :: EscrowArgs_ext () -> SemanticsTypes.Contract;
+dispute args =
+  SemanticsTypes.When
+    [SemanticsTypes.Case
+       (SemanticsTypes.Choice
+         (SemanticsTypes.ChoiceId
+           (Stringa.implode
+             [Stringa.Char True True False False False False True False,
+               Stringa.Char True True True True False True True False,
+               Stringa.Char False True True True False True True False,
+               Stringa.Char False True True False False True True False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char False True False False True True True False,
+               Stringa.Char True False True True False True True False,
+               Stringa.Char False False False False False True False False,
+               Stringa.Char False False False False True True True False,
+               Stringa.Char False True False False True True True False,
+               Stringa.Char True True True True False True True False,
+               Stringa.Char False True False False False True True False,
+               Stringa.Char False False True True False True True False,
+               Stringa.Char True False True False False True True False,
+               Stringa.Char True False True True False True True False])
+           seller)
+         [SemanticsTypes.Bound Arith.one_int Arith.one_int])
+       SemanticsTypes.Close,
+      SemanticsTypes.Case
+        (SemanticsTypes.Choice
+          (SemanticsTypes.ChoiceId
+            (Stringa.implode
+              [Stringa.Char False False True False False False True False,
+                Stringa.Char True False False True False True True False,
+                Stringa.Char True True False False True True True False,
+                Stringa.Char False False False False True True True False,
+                Stringa.Char True False True False True True True False,
+                Stringa.Char False False True False True True True False,
+                Stringa.Char True False True False False True True False,
+                Stringa.Char False False False False False True False False,
+                Stringa.Char False False False False True True True False,
+                Stringa.Char False True False False True True True False,
+                Stringa.Char True True True True False True True False,
+                Stringa.Char False True False False False True True False,
+                Stringa.Char False False True True False True True False,
+                Stringa.Char True False True False False True True False,
+                Stringa.Char True False True True False True True False])
+            seller)
+          [SemanticsTypes.Bound Arith.zero_int Arith.zero_int])
+        (mediation args)]
+    (disputeDeadline args) SemanticsTypes.Close;
+
+report :: EscrowArgs_ext () -> SemanticsTypes.Contract;
+report args =
+  SemanticsTypes.When
+    [SemanticsTypes.Case
+       (SemanticsTypes.Choice
+         (SemanticsTypes.ChoiceId
+           (Stringa.implode
+             [Stringa.Char True False True False False False True False,
+               Stringa.Char False True True False True True True False,
+               Stringa.Char True False True False False True True False,
+               Stringa.Char False True False False True True True False,
+               Stringa.Char True False False True True True True False,
+               Stringa.Char False False True False True True True False,
+               Stringa.Char False False False True False True True False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char False True True True False True True False,
+               Stringa.Char True True True False False True True False,
+               Stringa.Char False False False False False True False False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char True True False False True True True False,
+               Stringa.Char False False False False False True False False,
+               Stringa.Char True False False False False True True False,
+               Stringa.Char False False True True False True True False,
+               Stringa.Char False True False False True True True False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char True True True False False True True False,
+               Stringa.Char False False False True False True True False,
+               Stringa.Char False False True False True True True False])
+           buyer)
+         [SemanticsTypes.Bound Arith.zero_int Arith.zero_int])
+       SemanticsTypes.Close,
+      SemanticsTypes.Case
+        (SemanticsTypes.Choice
+          (SemanticsTypes.ChoiceId
+            (Stringa.implode
+              [Stringa.Char False True False False True False True False,
+                Stringa.Char True False True False False True True False,
+                Stringa.Char False False False False True True True False,
+                Stringa.Char True True True True False True True False,
+                Stringa.Char False True False False True True True False,
+                Stringa.Char False False True False True True True False,
+                Stringa.Char False False False False False True False False,
+                Stringa.Char False False False False True True True False,
+                Stringa.Char False True False False True True True False,
+                Stringa.Char True True True True False True True False,
+                Stringa.Char False True False False False True True False,
+                Stringa.Char False False True True False True True False,
+                Stringa.Char True False True False False True True False,
+                Stringa.Char True False True True False True True False])
+            buyer)
+          [SemanticsTypes.Bound Arith.one_int Arith.one_int])
+        (SemanticsTypes.Pay seller (SemanticsTypes.Account buyer) (token args)
+          (price args) (dispute args))]
+    (complaintDeadline args) SemanticsTypes.Close;
+
+escrow :: EscrowArgs_ext () -> SemanticsTypes.Contract;
+escrow args =
+  SemanticsTypes.When
+    [SemanticsTypes.Case
+       (SemanticsTypes.Deposit seller buyer (token args) (price args))
+       (report args)]
+    (paymentDeadline args) SemanticsTypes.Close;
+
+exampleArgs :: EscrowArgs_ext ();
+exampleArgs =
+  EscrowArgs_ext
+    (SemanticsTypes.Constant (Arith.Int_of_integer (10 :: Integer)))
+    (SemanticsTypes.Token (Stringa.implode []) (Stringa.implode []))
+    (Arith.Int_of_integer (1664812800000 :: Integer))
+    (Arith.Int_of_integer (1664816400000 :: Integer))
+    (Arith.Int_of_integer (1664820420000 :: Integer))
+    (Arith.Int_of_integer (1664824440000 :: Integer)) ();
+
+escrowExample :: SemanticsTypes.Contract;
+escrowExample = escrow exampleArgs;
+
+confirmClaimPayments :: [Semantics.Payment];
+confirmClaimPayments =
+  [Semantics.Payment seller (SemanticsTypes.Account buyer) (token exampleArgs)
+     (Arith.Int_of_integer (10 :: Integer)),
+    Semantics.Payment buyer (SemanticsTypes.Party buyer) (token exampleArgs)
+      (Arith.Int_of_integer (10 :: Integer))];
+
+dismissClaimPayments :: [Semantics.Payment];
+dismissClaimPayments =
+  [Semantics.Payment seller (SemanticsTypes.Account buyer) (token exampleArgs)
+     (Arith.Int_of_integer (10 :: Integer)),
+    Semantics.Payment buyer (SemanticsTypes.Account seller) (token exampleArgs)
+      (Arith.Int_of_integer (10 :: Integer)),
+    Semantics.Payment seller (SemanticsTypes.Party seller) (token exampleArgs)
+      (Arith.Int_of_integer (10 :: Integer))];
+
+confirmProblemPayments :: [Semantics.Payment];
+confirmProblemPayments =
+  [Semantics.Payment seller (SemanticsTypes.Account buyer) (token exampleArgs)
+     (Arith.Int_of_integer (10 :: Integer)),
+    Semantics.Payment buyer (SemanticsTypes.Party buyer) (token exampleArgs)
+      (Arith.Int_of_integer (10 :: Integer))];
+
+confirmClaimTransactions :: [Semantics.Transaction_ext ()];
+confirmClaimTransactions =
+  [Semantics.Transaction_ext
+     (Arith.Int_of_integer (1664812600000 :: Integer),
+       Arith.Int_of_integer (1664812700000 :: Integer))
+     [SemanticsTypes.IDeposit seller buyer (token exampleArgs)
+        (Arith.Int_of_integer (10 :: Integer))]
+     (),
+    Semantics.Transaction_ext
+      (Arith.Int_of_integer (1664812900000 :: Integer),
+        Arith.Int_of_integer (1664813100000 :: Integer))
+      [SemanticsTypes.IChoice
+         (SemanticsTypes.ChoiceId
+           (Stringa.implode
+             [Stringa.Char False True False False True False True False,
+               Stringa.Char True False True False False True True False,
+               Stringa.Char False False False False True True True False,
+               Stringa.Char True True True True False True True False,
+               Stringa.Char False True False False True True True False,
+               Stringa.Char False False True False True True True False,
+               Stringa.Char False False False False False True False False,
+               Stringa.Char False False False False True True True False,
+               Stringa.Char False True False False True True True False,
+               Stringa.Char True True True True False True True False,
+               Stringa.Char False True False False False True True False,
+               Stringa.Char False False True True False True True False,
+               Stringa.Char True False True False False True True False,
+               Stringa.Char True False True True False True True False])
+           buyer)
+         Arith.one_int]
+      (),
+    Semantics.Transaction_ext
+      (Arith.Int_of_integer (1664817400000 :: Integer),
+        Arith.Int_of_integer (1664817400000 :: Integer))
+      [SemanticsTypes.IChoice
+         (SemanticsTypes.ChoiceId
+           (Stringa.implode
+             [Stringa.Char False False True False False False True False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char True True False False True True True False,
+               Stringa.Char False False False False True True True False,
+               Stringa.Char True False True False True True True False,
+               Stringa.Char False False True False True True True False,
+               Stringa.Char True False True False False True True False,
+               Stringa.Char False False False False False True False False,
+               Stringa.Char False False False False True True True False,
+               Stringa.Char False True False False True True True False,
+               Stringa.Char True True True True False True True False,
+               Stringa.Char False True False False False True True False,
+               Stringa.Char False False True True False True True False,
+               Stringa.Char True False True False False True True False,
+               Stringa.Char True False True True False True True False])
+           seller)
+         Arith.zero_int]
+      (),
+    Semantics.Transaction_ext
+      (Arith.Int_of_integer (1664821400000 :: Integer),
+        Arith.Int_of_integer (1664822400000 :: Integer))
+      [SemanticsTypes.IChoice
+         (SemanticsTypes.ChoiceId
+           (Stringa.implode
+             [Stringa.Char True True False False False False True False,
+               Stringa.Char True True True True False True True False,
+               Stringa.Char False True True True False True True False,
+               Stringa.Char False True True False False True True False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char False True False False True True True False,
+               Stringa.Char True False True True False True True False,
+               Stringa.Char False False False False False True False False,
+               Stringa.Char True True False False False True True False,
+               Stringa.Char False False True True False True True False,
+               Stringa.Char True False False False False True True False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char True False True True False True True False])
+           mediator)
+         Arith.one_int]
+      ()];
+
+dismissClaimTransactions :: [Semantics.Transaction_ext ()];
+dismissClaimTransactions =
+  [Semantics.Transaction_ext
+     (Arith.Int_of_integer (1664812600000 :: Integer),
+       Arith.Int_of_integer (1664812700000 :: Integer))
+     [SemanticsTypes.IDeposit seller buyer (token exampleArgs)
+        (Arith.Int_of_integer (10 :: Integer))]
+     (),
+    Semantics.Transaction_ext
+      (Arith.Int_of_integer (1664812900000 :: Integer),
+        Arith.Int_of_integer (1664813100000 :: Integer))
+      [SemanticsTypes.IChoice
+         (SemanticsTypes.ChoiceId
+           (Stringa.implode
+             [Stringa.Char False True False False True False True False,
+               Stringa.Char True False True False False True True False,
+               Stringa.Char False False False False True True True False,
+               Stringa.Char True True True True False True True False,
+               Stringa.Char False True False False True True True False,
+               Stringa.Char False False True False True True True False,
+               Stringa.Char False False False False False True False False,
+               Stringa.Char False False False False True True True False,
+               Stringa.Char False True False False True True True False,
+               Stringa.Char True True True True False True True False,
+               Stringa.Char False True False False False True True False,
+               Stringa.Char False False True True False True True False,
+               Stringa.Char True False True False False True True False,
+               Stringa.Char True False True True False True True False])
+           buyer)
+         Arith.one_int]
+      (),
+    Semantics.Transaction_ext
+      (Arith.Int_of_integer (1664817400000 :: Integer),
+        Arith.Int_of_integer (1664817400000 :: Integer))
+      [SemanticsTypes.IChoice
+         (SemanticsTypes.ChoiceId
+           (Stringa.implode
+             [Stringa.Char False False True False False False True False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char True True False False True True True False,
+               Stringa.Char False False False False True True True False,
+               Stringa.Char True False True False True True True False,
+               Stringa.Char False False True False True True True False,
+               Stringa.Char True False True False False True True False,
+               Stringa.Char False False False False False True False False,
+               Stringa.Char False False False False True True True False,
+               Stringa.Char False True False False True True True False,
+               Stringa.Char True True True True False True True False,
+               Stringa.Char False True False False False True True False,
+               Stringa.Char False False True True False True True False,
+               Stringa.Char True False True False False True True False,
+               Stringa.Char True False True True False True True False])
+           seller)
+         Arith.zero_int]
+      (),
+    Semantics.Transaction_ext
+      (Arith.Int_of_integer (1664821400000 :: Integer),
+        Arith.Int_of_integer (1664822400000 :: Integer))
+      [SemanticsTypes.IChoice
+         (SemanticsTypes.ChoiceId
+           (Stringa.implode
+             [Stringa.Char False False True False False False True False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char True True False False True True True False,
+               Stringa.Char True False True True False True True False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char True True False False True True True False,
+               Stringa.Char True True False False True True True False,
+               Stringa.Char False False False False False True False False,
+               Stringa.Char True True False False False True True False,
+               Stringa.Char False False True True False True True False,
+               Stringa.Char True False False False False True True False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char True False True True False True True False])
+           mediator)
+         Arith.zero_int]
+      ()];
+
+confirmProblemTransactions :: [Semantics.Transaction_ext ()];
+confirmProblemTransactions =
+  [Semantics.Transaction_ext
+     (Arith.Int_of_integer (1664812600000 :: Integer),
+       Arith.Int_of_integer (1664812700000 :: Integer))
+     [SemanticsTypes.IDeposit seller buyer (token exampleArgs)
+        (Arith.Int_of_integer (10 :: Integer))]
+     (),
+    Semantics.Transaction_ext
+      (Arith.Int_of_integer (1664812900000 :: Integer),
+        Arith.Int_of_integer (1664813100000 :: Integer))
+      [SemanticsTypes.IChoice
+         (SemanticsTypes.ChoiceId
+           (Stringa.implode
+             [Stringa.Char False True False False True False True False,
+               Stringa.Char True False True False False True True False,
+               Stringa.Char False False False False True True True False,
+               Stringa.Char True True True True False True True False,
+               Stringa.Char False True False False True True True False,
+               Stringa.Char False False True False True True True False,
+               Stringa.Char False False False False False True False False,
+               Stringa.Char False False False False True True True False,
+               Stringa.Char False True False False True True True False,
+               Stringa.Char True True True True False True True False,
+               Stringa.Char False True False False False True True False,
+               Stringa.Char False False True True False True True False,
+               Stringa.Char True False True False False True True False,
+               Stringa.Char True False True True False True True False])
+           buyer)
+         Arith.one_int]
+      (),
+    Semantics.Transaction_ext
+      (Arith.Int_of_integer (1664817400000 :: Integer),
+        Arith.Int_of_integer (1664817400000 :: Integer))
+      [SemanticsTypes.IChoice
+         (SemanticsTypes.ChoiceId
+           (Stringa.implode
+             [Stringa.Char True True False False False False True False,
+               Stringa.Char True True True True False True True False,
+               Stringa.Char False True True True False True True False,
+               Stringa.Char False True True False False True True False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char False True False False True True True False,
+               Stringa.Char True False True True False True True False,
+               Stringa.Char False False False False False True False False,
+               Stringa.Char False False False False True True True False,
+               Stringa.Char False True False False True True True False,
+               Stringa.Char True True True True False True True False,
+               Stringa.Char False True False False False True True False,
+               Stringa.Char False False True True False True True False,
+               Stringa.Char True False True False False True True False,
+               Stringa.Char True False True True False True True False])
+           seller)
+         Arith.one_int]
+      ()];
+
+everythingIsAlrightPayments :: [Semantics.Payment];
+everythingIsAlrightPayments =
+  [Semantics.Payment seller (SemanticsTypes.Party seller) (token exampleArgs)
+     (Arith.Int_of_integer (10 :: Integer))];
+
+everythingIsAlrightTransactions :: [Semantics.Transaction_ext ()];
+everythingIsAlrightTransactions =
+  [Semantics.Transaction_ext
+     (Arith.Int_of_integer (1664812600000 :: Integer),
+       Arith.Int_of_integer (1664812700000 :: Integer))
+     [SemanticsTypes.IDeposit seller buyer (token exampleArgs)
+        (Arith.Int_of_integer (10 :: Integer))]
+     (),
+    Semantics.Transaction_ext
+      (Arith.Int_of_integer (1664812900000 :: Integer),
+        Arith.Int_of_integer (1664813100000 :: Integer))
+      [SemanticsTypes.IChoice
+         (SemanticsTypes.ChoiceId
+           (Stringa.implode
+             [Stringa.Char True False True False False False True False,
+               Stringa.Char False True True False True True True False,
+               Stringa.Char True False True False False True True False,
+               Stringa.Char False True False False True True True False,
+               Stringa.Char True False False True True True True False,
+               Stringa.Char False False True False True True True False,
+               Stringa.Char False False False True False True True False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char False True True True False True True False,
+               Stringa.Char True True True False False True True False,
+               Stringa.Char False False False False False True False False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char True True False False True True True False,
+               Stringa.Char False False False False False True False False,
+               Stringa.Char True False False False False True True False,
+               Stringa.Char False False True True False True True False,
+               Stringa.Char False True False False True True True False,
+               Stringa.Char True False False True False True True False,
+               Stringa.Char True True True False False True True False,
+               Stringa.Char False False False True False True True False,
+               Stringa.Char False False True False True True True False])
+           buyer)
+         Arith.zero_int]
+      ()];
+
+}
diff --git a/isabelle/marlowe.cabal b/isabelle/marlowe.cabal
index 3d6a9604..de08526e 100644
--- a/isabelle/marlowe.cabal
+++ b/isabelle/marlowe.cabal
@@ -41,6 +41,7 @@ library
         Arith
         ArithNumInstance
         CoreOrphanEq
+        Examples.Escrow
         Examples.Swap
         MarloweCoreJson
         Semantics
diff --git a/marlowe-spec-test/marlowe-spec-test.cabal b/marlowe-spec-test/marlowe-spec-test.cabal
index 40d3a168..bf314607 100644
--- a/marlowe-spec-test/marlowe-spec-test.cabal
+++ b/marlowe-spec-test/marlowe-spec-test.cabal
@@ -34,6 +34,7 @@ library
         Marlowe.Spec.Core
         Marlowe.Spec.Core.Arbitrary
         Marlowe.Spec.Core.Examples
+        Marlowe.Spec.Core.Examples.Escrow
         Marlowe.Spec.Core.Examples.Swap
         Marlowe.Spec.Core.Semantics
         Marlowe.Spec.Core.Serialization.Json
diff --git a/marlowe-spec-test/src/Marlowe/Spec/Core/Examples.hs b/marlowe-spec-test/src/Marlowe/Spec/Core/Examples.hs
index cd96b394..fd8e06ae 100644
--- a/marlowe-spec-test/src/Marlowe/Spec/Core/Examples.hs
+++ b/marlowe-spec-test/src/Marlowe/Spec/Core/Examples.hs
@@ -2,10 +2,12 @@
 
 module Marlowe.Spec.Core.Examples (tests) where
 import Test.Tasty (TestTree, testGroup)
+import qualified Marlowe.Spec.Core.Examples.Escrow
 import qualified Marlowe.Spec.Core.Examples.Swap
 import Marlowe.Spec.Interpret (InterpretJsonRequest)
 
 tests :: InterpretJsonRequest -> TestTree
 tests i = testGroup "Contract examples"
   [ Marlowe.Spec.Core.Examples.Swap.tests i
-  ]
\ No newline at end of file
+  , Marlowe.Spec.Core.Examples.Escrow.tests i
+  ]
diff --git a/marlowe-spec-test/src/Marlowe/Spec/Core/Examples/Escrow.hs b/marlowe-spec-test/src/Marlowe/Spec/Core/Examples/Escrow.hs
new file mode 100644
index 00000000..f4570e2d
--- /dev/null
+++ b/marlowe-spec-test/src/Marlowe/Spec/Core/Examples/Escrow.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Marlowe.Spec.Core.Examples.Escrow (tests) where
+
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (assertFailure, testCase, (@?=))
+import Marlowe.Spec.Interpret (InterpretJsonRequest, Request (..), parseValidResponse)
+import Semantics (TransactionOutput(..), txOutContract, txOutWarnings, txOutPayments, Transaction_ext (..), Payment (..))
+import SemanticsTypes (Contract(..))
+import Examples.Escrow (confirmProblemPayments, dismissClaimPayments, confirmClaimPayments, escrowExample, confirmClaimTransactions, dismissClaimTransactions, confirmProblemTransactions, everythingIsAlrightPayments, everythingIsAlrightTransactions)
+
+tests :: InterpretJsonRequest -> TestTree
+tests i = testGroup "Escrow"
+    [ everythingIsAlright i
+    , confirmProblem i
+    , dismissClaim i
+    , confirmClaim i
+    ]
+
+everythingIsAlright :: InterpretJsonRequest -> TestTree
+everythingIsAlright = runScenario "Everything is alright" everythingIsAlrightTransactions everythingIsAlrightPayments
+
+confirmProblem :: InterpretJsonRequest -> TestTree
+confirmProblem = runScenario "Confirm Problem" confirmProblemTransactions confirmProblemPayments
+
+dismissClaim :: InterpretJsonRequest -> TestTree
+dismissClaim = runScenario "Dismiss Claim" dismissClaimTransactions dismissClaimPayments
+
+confirmClaim :: InterpretJsonRequest -> TestTree
+confirmClaim = runScenario "Confirm Claim" confirmClaimTransactions confirmClaimPayments
+
+runScenario :: String -> [Transaction_ext ()] -> [Payment] -> InterpretJsonRequest -> TestTree
+runScenario name transactions payments interpret = testCase name
+    ( do
+        res <- interpret $ PlayTrace 0 escrowExample transactions
+        case parseValidResponse res of
+            Left err -> assertFailure err
+            Right (TransactionError err) -> assertFailure $ "Transaction error: " ++ show err
+            Right (TransactionOutput o) -> do
+              txOutContract o @?= Close
+              txOutWarnings o @?= []
+              txOutPayments o @?= payments
+    )