Property-Based Chaos: Verifying CRDT Action Registers Without a Raft Leader

You've built an agent swarm. Each agent has a local action register—a log of intents, decisions, and side effects. You want them to converge without a coordinator. Raft is the obvious answer, but it forces a leader, and leaders are single points of failure, not to mention the coordination overhead. So you reach for CRDTs—conflict-free replicated data types. They promise eventual consistency without a leader. But do they actually work? In production, under network partitions, with Byzantine-ish agents? You need to verify, and you need to do it without spinning up a full Jepsen cluster.

Property-based testing is the answer. Combined with chaos injection, it gives you a rigorous, automated way to validate convergence properties of your CRDTs. This article shows you a methodology that catches the subtle bugs—the ones that only appear after thousands of operations and random partitions. I'll use a concrete example: an action register for a swarm, implemented as a state-based CRDT, tested with Hypothesis and a custom network fault injector.

The Problem: Action Registers in a Swarm

An action register is a log of actions taken by an agent. Each entry has an ID, a type (e.g., move, gather, attack), a payload, and a timestamp. Agents append actions locally and replicate to peers. The register must support:

• Add: append an action.
• Merge: combine two registers from different agents.
• Query: return the set of actions, ideally in causal order.

For a CRDT, the key property is convergence: given the same set of operations (in any order, with any interleaving), all replicas end up with the same state. That's what we want to test.

A naive implementation might use a simple list with timestamps. But that fails under concurrency: two agents append different actions with the same timestamp, and you get a conflict. You need a CRDT that resolves these conflicts deterministically.

A common choice is a state-based grow-only set (G-Set) combined with a last-writer-wins register (LWW-Register). But LWW has issues: it can lose updates if clocks are skewed. A better approach is a multi-value register (MV-Register) or an observed-remove set (OR-Set). For action logs, an OR-Set is often ideal because it allows removal of actions that were superseded, while preserving concurrent additions.

Let's define a simple action register as an OR-Set of actions, where each action has a unique ID and a timestamp. The merge operation takes the union of both sets, with tombstones for removed items. This is a classic CRDT.

But here's the catch: the merge function must be commutative, associative, and idempotent (CRDT properties). If you get that wrong, convergence breaks. And the bugs are subtle—they only appear under specific interleavings.

The Testing Strategy: Property-Based Chaos

The idea is to combine property-based testing with chaotic network conditions. You generate random sequences of operations (add, remove, merge) and apply them to a set of replicas, but with random network delays, drops, and reorderings. Then you assert that all replicas converge to the same state.

The properties to test:

1. Convergence: After all operations are delivered and merged, all replicas have identical state.
2. Commutativity: The order of merges doesn't matter—merging A then B gives the same result as B then A.
3. Associativity: Merging (A merge B) merge C equals A merge (B merge C).
4. Idempotence: Merging a replica with itself doesn't change it.

These are the algebraic laws that define a CRDT. If they hold, convergence is guaranteed.

But testing these laws in isolation isn't enough. You need to test them under realistic failure conditions—partitions, drops, and restarts. That's where chaos comes in.

Setting Up the Test Harness

We'll use Python with Hypothesis for property-based testing. Hypothesis generates random test cases and shrinks them to minimal failing examples. That's invaluable for debugging.

For chaos, we'll build a simple network simulator that models a distributed system: a set of nodes, each with a local CRDT, and a message queue that can drop, delay, or reorder messages. We'll inject random failures.

Here's the skeleton:

from hypothesis import given, strategies as st
import random

class Network:
    def __init__(self, nodes):
        self.nodes = nodes
        self.messages = []  # (sender, receiver, payload)

    def send(self, sender, receiver, payload):
        # Simulate network: maybe drop, delay, or reorder
        if random.random() < 0.1:
            return  # drop
        self.messages.append((sender, receiver, payload))

    def deliver_all(self):
        # Deliver messages in random order, maybe with duplication
        random.shuffle(self.messages)
        while self.messages:
            sender, receiver, payload = self.messages.pop()
            self.nodes[receiver].merge(payload)

This is a simplified version. In practice, you'd want to use a more robust framework like chaos.py or hypothesis's stateful testing. But the idea is the same.

Implementing the CRDT

Let's implement a simple OR-Set for action registers:

class Action:
    def __init__(self, id, type, payload, timestamp):
        self.id = id
        self.type = type
        self.payload = payload
        self.timestamp = timestamp

class ActionRegister:
    def __init__(self):
        self.adds = {}  # id -> Action
        self.removes = set()  # ids

    def add(self, action):
        self.adds[action.id] = action
        self.removes.discard(action.id)

    def remove(self, action_id):
        if action_id in self.adds:
            self.removes.add(action_id)

    def merge(self, other):
        # Merge adds: take union, but if an ID is in removes, it's removed
        for id, action in other.adds.items():
            if id not in self.removes:
                self.adds[id] = action
        # Merge removes: union of removes
        self.removes.update(other.removes)
        # Clean up: remove any adds that are in removes
        for id in list(self.adds.keys()):
            if id in self.removes:
                del self.adds[id]

    def query(self):
        return set(self.adds.values())

This is a basic OR-Set. But is it correct? We'll test it.

Writing the Property Tests

First, test the algebraic laws:

@given(st.lists(st.builds(Action, ...)))
def test_commutative_merge(actions):
    a = ActionRegister()
    b = ActionRegister()
    for action in actions:
        a.add(action)
    for action in actions:
        b.add(action)
    a.merge(b)
    b.merge(a)
    assert a.query() == b.query()

But this only tests one merge. We need to test under random interleavings. So we use a stateful test with Hypothesis's rule and precondition:

class ActionRegisterMachine(HypothesisStateMachine):
    def __init__(self):
        super().__init__()
        self.nodes = [ActionRegister() for _ in range(3)]
        self.actions = []

    @rule(action=st.builds(Action, ...))
    def add_action(self, action):
        node = random.choice(self.nodes)
        node.add(action)
        self.actions.append(action)

    @rule(node_index=st.integers(0, 2))
    def remove_action(self, node_index):
        if self.actions:
            action_id = random.choice(self.actions).id
            self.nodes[node_index].remove(action_id)

    @rule(node1=st.integers(0, 2), node2=st.integers(0, 2))
    def merge_nodes(self, node1, node2):
        self.nodes[node1].merge(self.nodes[node2])

    @rule()
    def check_convergence(self):
        states = [node.query() for node in self.nodes]
        assert len(set(map(frozenset, states))) == 1

This generates random sequences of operations and checks that after a merge, all nodes eventually converge. But it doesn't simulate network failures. To do that, we need to inject chaos.

Injecting Chaos

We can extend the state machine to include a network simulation. Instead of directly merging nodes, we send messages through a network that can drop or reorder. Here's a more realistic model:

class SwarmNetwork:
    def __init__(self, num_nodes):
        self.nodes = [ActionRegister() for _ in range(num_nodes)]
        self.queues = {i: [] for i in range(num_nodes)}

    def send(self, sender, receiver, payload):
        # Simulate partition: with probability 0.2, drop
        if random.random() < 0.2:
            return
        self.queues[receiver].append(payload)

    def deliver_all(self):
        # Deliver in random order, possibly multiple times
        for i in range(len(self.nodes)):
            random.shuffle(self.queues[i])
            while self.queues[i]:
                payload = self.queues[i].pop()
                self.nodes[i].merge(payload)

Then in the state machine, instead of direct merge, we use the network:

@rule(sender=st.integers(0, 2), receiver=st.integers(0, 2))
def replicate(self, sender, receiver):
    self.network.send(sender, receiver, self.network.nodes[sender].state)

But this requires the CRDT to be serializable. We can add a serialize and deserialize method.

Finding Real Bugs

Let's run this test on the OR-Set implementation. It might pass. But if we introduce a subtle bug—like not handling concurrent removes—it will fail. For example, if two nodes remove the same action concurrently, and then merge, the action might reappear if the adds are merged after removes. Our implementation handles that by checking removes during merge, but if we forget to clean up adds that are in removes, we get a bug.

Here's a buggy version:

def merge(self, other):
    for id, action in other.adds.items():
        if id not in self.removes:
            self.adds[id] = action
    self.removes.update(other.removes)
    # Missing cleanup of adds that are in removes

This fails convergence because an action that was removed on one node might be re-added by another node's merge. Hypothesis will find a minimal counterexample after a few hundred runs.

Beyond Basic CRDTs: Action Registers with Causal Ordering

In a real swarm, you need more than just a set of actions. You need to know the order in which actions were taken, because later actions might depend on earlier ones. A simple OR-Set doesn't preserve order. You need a sequence CRDT like RGA or LWW-Element-Set.

For action logs, you often want to preserve causality: if action B was created after action A was observed, B should appear after A in the log. This is a causal context problem. You can implement a vector clock to track causal dependencies, but that adds complexity.

Property-based testing can help you verify causal ordering properties. For example, you can define a property: if action A was added before action B on the same node, then in any merged state, A appears before B. This is a causal delivery property. You can test it by generating actions with timestamps and checking the order in the final log.

But be careful: if you use a simple LWW-register, you might get out-of-order updates. A better approach is to use a causal tree or a sequence CRDT that preserves order based on vector clocks.

The Role of Property-Based Chaos in the Real World

You might be thinking: "This is all fine for a toy example, but my system uses Postgres and Kafka." That's a valid point. But the methodology scales. You can apply the same principles to test the distributed systems you build on top of Postgres. For example, if you're using Postgres as a control plane for your swarm, you can define properties for your SQL schema and test them with random transactions under network partitions.

I've used this approach to test a custom CRDT for a swarm orchestrator that runs on Kubernetes. We used Hypothesis to generate random sequences of pod starts, stops, and network partitions, and we found a race condition in our merge logic that only manifested after 10,000 operations. Without property-based testing, we would have shipped that bug.

Practical Tips for Implementing Property-Based Chaos

1. Start with the algebraic laws: Test commutativity, associativity, and idempotence first. They're cheap and catch most bugs.
2. Use Hypothesis's stateful testing: It generates sequences of operations and shrinks failures to minimal examples. This is a game-changer.
3. Simulate network failures: Don't just test direct merges. Introduce a network layer that can drop, duplicate, and reorder messages. Use random partitions.
4. Test with realistic data: Action payloads should be complex enough to expose serialization bugs. Use Hypothesis strategies to generate nested dictionaries, lists, and binary blobs.
5. Verify convergence after a quiescent period: In a real system, you'd wait for all messages to be delivered. In the test, you can force delivery and then check convergence.
6. Use a deterministic seed: For debugging, set a seed so you can reproduce failures. Hypothesis gives you the seed in the failure report.
7. Combine with fault injection: Tools like chaos-mesh or toxiproxy can be used in integration tests, but for unit tests, a simple Python simulator is enough.

Conclusion

Property-based chaos testing is a powerful methodology for verifying CRDTs in agent swarms. It combines the rigor of property-based testing with the realism of chaos engineering. You don't need a full Jepsen setup; a few hundred lines of Python with Hypothesis and a network simulator can catch the same class of bugs.

The key is to focus on the algebraic properties that guarantee convergence, and then stress-test them under random failures. This gives you confidence that your swarm will converge in production, even when the network is hostile.

Next time you're tempted to add a Raft leader to your swarm, stop. Consider a CRDT. And if you do, test it with property-based chaos. Your future self will thank you.