# Eventual Consistency Pattern

> Eventual consistency with asynchronous primary-replica replication: a runnable model checking that replicas never get ahead of the primary and eventually converge.

Canonical: https://fizzbee.io/design/patterns/eventual-consistency/
Source: https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/13-05-01-eventual-consistency


Primary-replica replication with eventual convergence

**Demonstrates:** async replication, replica roles, eventual consistency

```fizz
# Example 0068: Eventual Consistency Pattern
# Primary-replica replication with eventual convergence
# Demonstrates: async replication, replica roles, eventual consistency

---
deadlock_detection: false
---

role Primary:
    action Init:
        self.value = 0
        self.update_count = 0

    atomic action Write:
        require self.update_count < MAX_UPDATES

        # Write to primary
        self.value = self.value + 1
        self.update_count = self.update_count + 1

    fair action Replicate:
        # Push updates to replicas asynchronously
        for replica in replicas:
            replica.ApplyUpdate(self.value)

role Replica:
    action Init:
        self.value = 0

    atomic func ApplyUpdate(new_value):
        # Apply update from primary (only if newer)
        if new_value > self.value:
            self.value = new_value

NUM_REPLICAS = 2
MAX_UPDATES = 2

action Init:
    primary = Primary()
    replicas = []
    for i in range(NUM_REPLICAS):
        replicas.append(Replica())

# Safety: replicas never ahead of primary
always assertion ReplicasNeverAhead:
    for replica in replicas:
        if replica.value > primary.value:
            return False
    return True

# Safety: replica values are monotonic (only increase)
always assertion MonotonicReplicas:
    for replica in replicas:
        if replica.value < 0:
            return False
    return True

# Liveness: eventually all replicas converge to primary value
eventually always assertion EventuallyConsistent:
    for replica in replicas:
        if replica.value != primary.value:
            return False
    return True
```
Run it in the FizzBee playground: https://fizzbee.io/play


**Expected result** (from `fizz`):

```
StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2} deadlock_detection:false
Nodes: 30, queued: 0
Valid Nodes: 30 Unique states: 26
Checking eventually always EventuallyConsistent
IsLive: true
PASSED: Model checker completed successfully
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/13-05-01-eventual-consistency)

## Language features used

[Roles](/reference/language/roles/), [Fairness](/reference/language/fairness/), [Assertions](/reference/language/assertions/), [Flow Modifiers](/reference/language/flow-modifiers/), [Functions](/reference/language/functions/)