The escrow smart contract establishes a decentralized purchase process between the seller and buyer. The principle is that the price amount is escrowed in the smart contract and released when the purchased item is received by buyer.

The critical point of the process is that it requires actions from the buyer and the seller to complete the process:

  • if the seller does not send the item, buyer's fund are locked in the escrow
  • if the buyer does not complete the process, even if the item is received, then the seller does not reveive payment

In order to motivate both the seller and the buyer to execute the process, the basic idea is that they fund the escrow with security deposits that are transferred back only if the process is complete. In the escrow presented here, security deposits are a proportion of the price of the item.



selleraddressSeller's address.
buyeraddressBuyer's address.
taxcollecteraddressTax collector's address.
pricetezAmount of transaction.
taxraterationalTax rate applied to price
securityraterationalSecurity rate applied to price for security deposit.
_statestatesEscrow state, one of Create, Aborted, Funded, Completed


abortbuyer and seller can abort escrow in Created state.
toFundedInternally called by escrow to go to Funded state.
fundCalled by buyer and seller to provide funds:
  • buyer must transfer price, security deposit and taxes
  • seller must transfer security deposit.
completeCalled by buyer when purchased item is received. This transfers:
  • item price and security deposit to seller
  • security deposit to buyer
  • tax to taxcollector


archetype escrow(
seller : address,
buyer : address,
taxcollector : address,
price : tez,
taxrate : rational,
securityrate : rational,
variable buyer_funded : bool = false
variable seller_funded : bool = false
(* states *)
states =
| Created initial
| Aborted
| Funded
| Completed
transition abort () {
called by buyer or seller
from Created to Aborted
transition toFunded () {
called by selfaddress
from Created to Funded
entry fund () {
called by buyer or seller
effect {
if caller = buyer then begin
dorequire(transferred >= (1 + taxrate + securityrate) * price, "NOT_ENOUGH_FUND");
buyer_funded := true
end else if caller = seller then begin
dorequire(transferred >= securityrate * price, "NOT_ENOUGH_FUND");
seller_funded := true
if buyer_funded and seller_funded then
transfer 0tz to entry self.toFunded()
transition complete () {
called by buyer
from Funded to Completed
with effect {
transfer ((1 + securityrate) * price) to seller;
transfer (securityrate * price) to buyer;
if taxrate > 0 then
transfer (taxrate * price) to taxcollector;