Building a Two-Phase Commit Protocol with Choreo

This tutorial will guide you step-by-step through implementing a distributed two-phase commit protocol using the Choreo framework. We’ll start from the provided template and build up to a complete specification.

Prerequisites

Quint installed
Choreo files downloaded (choreo.qnt and template.qnt , plus the Quint spells). Use the following commands to get them easily:


# Download the required Choreo files
curl -O https://raw.githubusercontent.com/informalsystems/choreo/main/choreo.qnt
curl -O https://raw.githubusercontent.com/informalsystems/choreo/main/template.qnt
 
# Download the spells folder and files
mkdir -p spells
curl -o spells/basicSpells.qnt https://raw.githubusercontent.com/informalsystems/choreo/main/spells/basicSpells.qnt
curl -o spells/rareSpells.qnt https://raw.githubusercontent.com/informalsystems/choreo/main/spells/rareSpells.qnt

Overview: What is Two-Phase Commit?

The two-phase commit protocol is a distributed transaction protocol that ensures either all participants commit or all abort. It involves:

Coordinator: Initiates the protocol and decides whether to commit or abort based on messages from participants
Participants: Vote to prepare or abort, then follow coordinator’s decision

If Alice wants to withdraw 50 bucks from an ATM, the ATM acts as a coordinator while redundant database nodes are participants. The ATM asks “prepare a transaction where Alice withdraws $50”, and each database node will check if she has enough balance and either send a “Commit” or an “Abort” message. Only when the ATM receives “Commit” from all nodes, it will tell them to execute the prepared transaction, while it can instead choose to abort at any point and tell all nodes to abort as well.

Starting with the Template

Let’s begin with the template file that provides the structure for any Choreo protocol. The template includes:

template.qnt


module my_protocol {
  import basicSpells.* from "spells/basicSpells"
  import choreo(processes = NODES) as choreo from "choreo"
 
  // TODO: Define your protocol-specific types here
 
  type Node = str
  type Message = ExampleMessage(Node)
  type StateFields = {
    // TODO: Add your state fields here
  }
  type CustomEffects = ()
  type Event = ()
  type Extensions = ()
 
  // ... rest of template
}

The template gives us the basic structure, but we need to define our protocol-specific types and logic.

Define Protocol-Specific Types

First, let’s define the types specific to two-phase commit. We need to distinguish between coordinators and participants, and track the stage of the protocol.

two_phase_commit.qnt


 module two_phase_commit {
   import basicSpells.* from "../../spells/basicSpells"
   import choreo(processes = NODES) as choreo from "../../choreo"
 
+  // Auxiliary types
+  type Role = Coordinator | Participant
+  type Stage = Working | Prepared | Committed | Aborted
 
   // Mandatory types for the Choreo
   type Node = str

Why these types?

Role: Each node is either the coordinator (makes decisions) or a participant (follows orders)
Stage: Tracks the current stage of a given node in the two-phase commit protocol

Define Message Types

Now let’s define the messages that nodes exchange during the protocol:

two_phase_commit.qnt


   type Node = str
-  type Message = ExampleMessage(Node)
+  type Message =
+    | CoordinatorAbort
+    | CoordinatorCommit
+    | ParticipantPrepared(Node)

Message purposes:

CoordinatorAbort: Coordinator tells participants to abort
CoordinatorCommit: Coordinator tells participants to commit
ParticipantPrepared(Node): A participant signals they’re prepared to commit

Define State Fields

Each node needs to track its role and current stage:

two_phase_commit.qnt


   type StateFields = {
-    // TODO: Add your state fields here
+    role: Role,
+    stage: Stage,
   }
 
   type CustomEffects = ()
   type Event = ()
   type Extensions = ()

State explanation:

role: Whether this node is coordinator or participant (set at initialization)
stage: Current stage in the protocol (changes as protocol progresses)

Add Helper Functions

We need a helper function to extract prepared messages from the message set:

two_phase_commit.qnt


pure def get_prepared_msgs(msgs: Set[Message]): Set[Node] = {
  msgs.filterMap(m => match m {
    | ParticipantPrepared(n) => Some(n)
    | _ => None
  })
}

This function filters the message set to find all ParticipantPrepared messages and returns the set of nodes that sent them. We hope to add an easier way of doing this to Quint soon, but currently, we need to filterMap by hand like this.

Implement Participant Transitions

Let’s implement the participant behavior. Participants can:

Spontaneously prepare
Spontaneously abort
Follow coordinator’s abort decision
Follow coordinator’s commit decision

We implement one operator for each of these options. Each of them return a Set with the transition if we can take that action in the current state, or an empty Set otherwise. We could also do it with an Option type, but we choose Set as it’s easier to combine the results later on (by simply calling flatten()).

Spontaneous Prepare

two_phase_commit.qnt


// --- Participant transitions ----------------------------------------------
pure def spontaneously_prepares(ctx: LocalContext): Set[Transition] = {
  if (ctx.state.role == Participant and ctx.state.stage == Working) {
    Set({
      effects: Set(choreo::Broadcast(ParticipantPrepared(ctx.state.process_id))),
      post_state: { ...ctx.state, stage: Prepared }
    })
  } else {
    Set()
  }
}

Logic:

Guard: Only participants in “Working” stage can prepare
Effects: Broadcast a prepared message to all nodes
State change: Move to “Prepared” stage

Spontaneous Abort

two_phase_commit.qnt


pure def spontaneously_aborts(ctx: LocalContext): Set[Transition] = {
  if (ctx.state.role == Participant and ctx.state.stage == Working) {
    Set({
      effects: Set(),
      post_state: { ...ctx.state, stage: Aborted }
    })
  } else {
    Set()
  }
}

Logic:

Guard: Only participants in “Working” stage can abort
Effects: None (no message needed)
State change: Move to “Aborted” stage

Follow Coordinator’s Instructions

two_phase_commit.qnt


pure def aborts_as_instructed(ctx: LocalContext): Set[Transition] = {
  if (ctx.state.role == Participant and ctx.messages.contains(CoordinatorAbort)) {
    Set({
      effects: Set(),
      post_state: { ...ctx.state, stage: Aborted }
    })
  } else {
    Set()
  }
}
 
pure def commits_as_instructed(ctx: LocalContext): Set[Transition] = {
  if (ctx.state.role == Participant and ctx.messages.contains(CoordinatorCommit)) {
    Set({
      effects: Set(),
      post_state: { ...ctx.state, stage: Committed }
    })
  } else {
    Set()
  }
}

Both transitions check for the appropriate coordinator message and change state accordingly.

Implement Coordinator Transitions

The coordinator has two main responsibilities:

Decide to commit when all participants are prepared
Decide to abort at any time

Decide on Commit

two_phase_commit.qnt


// --- Coordinator transitions ------------------------------
pure def decides_on_commit(ctx: LocalContext): Set[Transition] = {
  if (ctx.state.role == Coordinator
      and ctx.state.stage == Working
      and ctx.messages.get_prepared_msgs().size() == PARTICIPANTS.size()) {
    Set({
      effects: Set(choreo::Broadcast(CoordinatorCommit)),
      post_state: { ...ctx.state, stage: Committed }
    })
  } else {
    Set()
  }
}

Guard Condition:

Must be coordinator
Must be in “Working” stage
Must have received prepared messages from ALL participants

Decide on Abort

two_phase_commit.qnt


  pure def decides_on_abort(ctx: LocalContext): Set[Transition] = {
    if (ctx.state.role == Coordinator and ctx.state.stage == Working) {
      Set({
        effects: Set(choreo::Broadcast(CoordinatorAbort)),
        post_state: { ...ctx.state, stage: Aborted }
      })
    } else {
      Set()
    }
  }

The coordinator can decide to abort at any time while in the “Working” stage.

Wire Everything Together

Main Listener

two_phase_commit.qnt


   pure def main_listener(ctx: LocalContext): Set[Transition] = {
     Set(
-      // ...
+      spontaneously_prepares(ctx),
+      spontaneously_aborts(ctx),
+      aborts_as_instructed(ctx),
+      commits_as_instructed(ctx),
+      decides_on_commit(ctx),
+      decides_on_abort(ctx)
     ).flatten()
   }

This combines all possible transitions. Choreo will check which ones are enabled and allow non-deterministic choice.

Node Configuration

two_phase_commit.qnt


   // =============================================================================
   // PROTOCOL CONFIGURATION
   // =============================================================================
 
-  // TODO: Define your process set
-  pure val NODES = Set("n1", "n2", "n3")  // Replace with your node set
+  pure val COORDINATOR: Node = "c"
+  pure val PARTICIPANTS: Set[Node] = Set("p1", "p2", "p3")
+  pure val NODES = PARTICIPANTS.union(Set(COORDINATOR))

We define one coordinator and three participants.

Initialization

two_phase_commit.qnt


   // =============================================================================
   // INITIALIZATION
   // =============================================================================
 
-  // TODO: Define how to initialize each process's local state
   pure def initialize(n: Node): LocalState = {
     {
       process_id: n,
-      // TODO: Initialize your state fields
-      // phase: Init,
-      // value: None,
-      // round: 0,
+      role: if (n == COORDINATOR) Coordinator else Participant,
+      stage: Working,
     }
   }
 
- // TODO: Define initial global state
   action init = choreo::init({
     system: NODES.mapBy(n => initialize(n)),
-    messages: NODES.mapBy(n => Set()),  // Or add initial messages if needed
+    messages: NODES.mapBy(n => Set()),
-    events: NODES.mapBy(n => Set()),    // Or add initial events if needed
+    events: NODES.mapBy(n => Set()),
-    extensions: ()  // Or initialize your extensions
+    extensions: ()
   })

Each node starts in the “Working” stage with their role determined by whether they are the coordinator.

Step Function

two_phase_commit.qnt


   // =============================================================================
   // STEP FUNCTION
   // =============================================================================
 
-  // TODO: Define how the system makes progress
   action step = choreo::step(
     main_listener,
-    apply_custom_effect  // Use (c, _) => c if no custom effects
+    (c, _) => c
   )

Since we don’t have custom effects, we use the identity function.

Add Properties and Tests

Consistency Property

two_phase_commit.qnt


   // =============================================================================
   // PROPERTIES
   // =============================================================================
 
+  val consistency = PARTICIPANTS.forall(p1 => {
+    PARTICIPANTS.forall(p2 => {
+      not(choreo::s.system.get(p1).stage == Committed
+        and choreo::s.system.get(p2).stage == Aborted)
+    })
+  })

This ensures that no two participants can be in conflicting states (one committed, one aborted).

Test Scenario

two_phase_commit.qnt


   // =============================================================================
   // TESTING AND DEBUGGING
   // =============================================================================
 
+  run commitTest = init
+    .then(step_with("p1", spontaneously_prepares))
+    .then(step_with("p2", spontaneously_prepares))
+    .then(step_with("p3", spontaneously_prepares))
+    .then(step_with(COORDINATOR, decides_on_commit))
+    .then(step_with("p1", commits_as_instructed))
+    .then(step_with("p2", commits_as_instructed))
+    .then(step_with("p3", commits_as_instructed))
+    .expect({
+      // Check that all participants have committed
+      PARTICIPANTS.forall(p => {
+        choreo::s.system.get(p).stage == Committed
+      })
+    })

This test simulates a successful commit scenario.

Testing Your Implementation

Let’s simulate our specification:


quint run two_phase_commit.qnt --invariant consistency


[ok] No violation found (7045ms at 1419 traces/second).
Trace length statistics: max=8, min=5, average=6.49
You may increase --max-samples and --max-steps.
Use --verbosity to produce more (or less) output.
Use --seed=0x12954db3ea62c1 to reproduce.

Let’s run our commitTest:


quint test two_phase_commit.qnt --match commitTest


  two_phase_commit
    ok commitTest passed 1 test(s)
 
  1 passing (16ms)

Interactive Exploration

You can also explore the protocol interactively using the Quint REPL:


quint -r two_phase_commit.qnt::two_phase_commit


Quint REPL 0.27.0
Type ".exit" to exit, or ".help" for more information
>>> init
true
>>> choreo::s
{
  events: Map("c" -> Set(), "p1" -> Set(), "p2" -> Set(), "p3" -> Set()),
  extensions: (),
  messages: Map("c" -> Set(), "p1" -> Set(), "p2" -> Set(), "p3" -> Set()),
  system:
    Map(
      "c" -> { process_id: "c", role: Coordinator, stage: Working },
      "p1" -> { process_id: "p1", role: Participant, stage: Working },
      "p2" -> { process_id: "p2", role: Participant, stage: Working },
      "p3" -> { process_id: "p3", role: Participant, stage: Working }
    )
}
>>> step_with("p1", spontaneously_prepares)
true
>>> choreo::s.messages
Map(
  "c" -> Set(ParticipantPrepared("p1")),
  "p1" -> Set(ParticipantPrepared("p1")),
  "p2" -> Set(ParticipantPrepared("p1")),
  "p3" -> Set(ParticipantPrepared("p1"))
)

Check out the complete two phase commit spec using Choreo here .

Advanced Features

This tutorial covered the basics of Choreo with a simple two-phase commit protocol. For more complex protocols, you’ll need additional features:

Advanced Guides

Using the choreo::cue Pattern: Learn the listen-then-act pattern for clean protocol transitions
CustomEffect and Environment Extensions: Add global state and evidence collection for accountability
Using step_micro: Process messages one at a time for easier debugging and testing

Complete Examples

Tendermint - Uses all advanced features for consensus
Alpenglow - Byzantine agreement protocol
Monad BFT - Another consensus implementation