Skip to content

Add Stateright.rs model checking tests #1598

@drmingdrmer

Description

@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

Metadata

Metadata

Assignees

No one assigned

    Labels

    C-testCategory: test infrastructure or coverage

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions