Add Stateright.rs model checking tests

[drmingdrmer]

Parent issue: #475

Overview

Add Stateright.rs model checking tests to validate openraft's correctness. Stateright is a Rust-native distributed systems testing framework that can be embedded directly into the test suite.

Goals

• Model check core Raft properties
• Verify safety properties (no split-brain, log consistency)
• Verify liveness properties (leader election, log replication)
• Complement Jepsen with faster, deterministic testing

Advantages over Jepsen

• Written in Rust, integrates directly with openraft
• Faster iteration during development
• Deterministic execution for reproducible bugs
• No external infrastructure required

Implementation Steps

• Add stateright as dev-dependency
• Create model of openraft cluster
• Define safety properties to check
• Define liveness properties to check
• Add to CI pipeline

References

• Stateright documentation
• Stateright GitHub
• Stateright Raft example

[github-actions]

👋 Thanks for opening this issue!

Get help or engage by:

• /help : to print help messages.
• /assignme : to assign this issue to you.

[Phoenix500526]

/assignme

[Phoenix500526]

After investigating Stateright and OpenRaft’s execution model, I do not think this issue is feasible with its current goals.

Stateright explores an explicit state machine. Given a state and an action, the transition must produce a deterministic next state, and the complete state must be cloneable and hashable.

The official Stateright Raft example meets these requirements by implementing a separate synchronous Raft model inside the actor callbacks. It does not model-check an existing asynchronous Raft implementation.

OpenRaft’s safety and liveness also depend on behavior outside Engine. Engine updates its in-memory state and emits commands, while RaftCore executes those commands asynchronously. The production behavior includes:

• accepted, submitted, and flushed I/O stages;
• storage callbacks and crash windows;
• spawned replication workers;
• futures, wakers, channels, and timers;
• response conditions that wait for persistence or apply completion;
• task cancellation and scheduling.

A thin Stateright adapter would collapse these stages into atomic transitions. That would exclude storage ordering, crash timing, task scheduling, and other paths needed to check the safety and liveness properties listed in this issue.

A detailed adapter would need to model the executor, future polling, channels, timers, storage completion, replication workers, and crash semantics. Stateright would then check Engine + AdapterRuntime, rather than the production composition of Engine + RaftCore + AsyncRuntime + Storage/Network. Transferring the result to production would require proving that the adapter runtime preserves the production runtime’s behavior.

Model-checking Engine alone could still find bugs in local protocol transitions, but it would not satisfy this issue’s goal of validating OpenRaft’s full safety and liveness behavior.

A standalone Stateright Raft model could be useful as an executable specification or reference oracle. It should not be presented as validation of OpenRaft’s production implementation.

I suggest closing this issue as not planned and continuing to use deterministic simulation, fault injection, and targeted Engine tests for the actual asynchronous code paths.