https://github.com/stateright/stateright Skip to content Sign up * Why GitHub? Features - + Mobile - + Actions - + Codespaces - + Packages - + Security - + Code review - + Project management - + Integrations - + GitHub Sponsors - + Customer stories- * Team * Enterprise * Explore + Explore GitHub - Learn and contribute + Topics - + Collections - + Trending - + Learning Lab - + Open source guides - Connect with others + The ReadME Project - + Events - + Community forum - + GitHub Education - + GitHub Stars program - * Marketplace * Pricing Plans - + Compare plans - + Contact Sales - + Education - [ ] [search-key] * # In this repository All GitHub | Jump to | * No suggested jump to results * # In this repository All GitHub | Jump to | * # In this organization All GitHub | Jump to | * # In this repository All GitHub | Jump to | Sign in Sign up {{ message }} stateright / stateright * Notifications * Star 657 * Fork 15 A model checker for implementing distributed systems. docs.rs/stateright MIT License 657 stars 15 forks Star Notifications * Code * Issues 4 * Pull requests 1 * Discussions * Actions * Projects 0 * Wiki * Security * Insights More * Code * Issues * Pull requests * Discussions * Actions * Projects * Wiki * Security * Insights master Switch branches/tags [ ] Branches Tags Could not load branches Nothing to show {{ refName }} default View all branches Could not load tags Nothing to show {{ refName }} default View all tags 2 branches 0 tags Code Clone HTTPS GitHub CLI [https://github.com/s] Use Git or checkout with SVN using the web URL. [gh repo clone stater] Work fast with our official CLI. Learn more. * Open with GitHub Desktop * Download ZIP Launching GitHub Desktop If nothing happens, download GitHub Desktop and try again. Go back Launching GitHub Desktop If nothing happens, download GitHub Desktop and try again. Go back Launching Xcode If nothing happens, download Xcode and try again. Go back Launching Visual Studio Code Your codespace will open once ready. There was a problem preparing your codespace, please try again. Latest commit @abhinav-upadhyay @jonnadal abhinav-upadhyay and jonnadal Add missing 'to' in the sentence ... 36c7dec Jun 6, 2021 Add missing 'to' in the sentence 36c7dec Git stats * 310 commits Files Permalink Failed to load latest commit information. Type Name Latest commit message Commit time .github/workflows introduce rust.yml for GH build action Jan 19, 2021 examples examples: remove unnecessary cast May 23, 2021 src rename generated_count to unique_state_count May 22, 2021 ui rename generated_count to unique_state_count May 22, 2021 .gitignore .gitignore dot files Mar 9, 2018 CHANGES.md version 0.28.0 May 22, 2021 Cargo.toml replace clap w/ pico-args May 22, 2021 LICENSE clarify that contributors maintain their copyright Dec 5, 2020 README.md Add missing 'to' in the sentence Jun 6, 2021 bench.sh remove unnecessary restriction in paxos example May 15, 2021 explorer.png revise screenshot May 11, 2021 View code Getting Started Examples Features Contribution License README.md chat crates.io docs.rs LICENSE Correctly implementing distributed algorithms such as the Paxos and Raft consensus protocols is notoriously difficult due to inherent nondetermism such as message reordering by network devices. Stateright is a Rust actor library that aims to solve this problem by providing an embedded model checker, a UI for exploring system behavior (demo), and a lightweight actor runtime. It also features a linearizability tester that can be run within the model checker for more exhaustive test coverage than similar solutions such as Jepsen. Stateright Explorer screenshot Getting Started 1. Please see the book, "Building Distributed Systems With Stateright." 2. A video introduction is also available. 3. Stateright also has detailed API docs. 4. Consider also joining the Stateright Discord server for Q&A or other feedback. Examples Stateright includes a variety of examples, such as a Single Decree Paxos cluster and an abstract two phase commit model. Passing a check CLI argument causes each example to validate itself using Stateright's model checker: # Two phase commit with 3 resource managers. cargo run --release --example 2pc check 3 # Paxos cluster with 3 clients. cargo run --release --example paxos check 3 # Single-copy (unreplicated) register with 3 clients. cargo run --release --example single-copy-register check 3 # Linearizable distributed register (ABD algorithm) with 2 clients. # (please be patient with this one, as it takes longer to check) cargo run --release --example linearizable-register check 2 Passing an explore CLI argument causes each example to spin up the Stateright Explorer web UI locally on port 3000, allowing you to browse system behaviors: cargo run --release --example 2pc explore cargo run --release --example paxos explore cargo run --release --example single-copy-register explore cargo run --release --example linearizable-register explore Passing a spawn CLI argument to the examples leveraging the actor functionality will cause each to spawn actors using the included runtime, transmitting JSON messages over UDP: cargo run --release --example paxos spawn cargo run --release --example single-copy-register spawn cargo run --release --example linearizable-register spawn Features Stateright contains a general purpose model checker offering: * Invariant checks via "always" properties. * Nontriviality checks via "sometimes" properties. * Liveness checks via "eventually" properties. * A web browser UI for interactively exploring state space. * Linearizability and sequential consistency testers. Stateright's actor system features include: * An actor runtime that can execute actors outside the model checker in the "real world." * A model for lossy/lossless duplicating/non-duplicating networks with the ability to capture actor message history to check an actor system against an expected consistency model. * An optional network adapter that provides a lossless non-duplicating ordered virtual channel for messages between a pair of actors. In contrast with other actor libraries, Stateright enables you to formally verify the correctness of your implementation, and in contrast with model checkers such as TLC for TLA+, systems implemented using Stateright can also be run on a real network without being reimplemented in a different language. Contribution Contributions are welcome! Please fork the library, push changes to your fork, and send a pull request. All contributions are shared under an MIT license unless explicitly stated otherwise in the pull request. License Stateright is copyright 2018 Jonathan Nadal and other contributors. It is made available under the MIT License. To avoid the need for a Javascript package manager, the Stateright repository includes code for the following Javascript dependency used by Stateright Explorer: * KnockoutJS is copyright 2010 Steven Sanderson, the Knockout.js team, and other contributors. It is made available under the MIT License. About A model checker for implementing distributed systems. docs.rs/stateright Topics distributed-systems actor-model paxos model-checker Resources Readme License MIT License Releases No releases published Packages 0 No packages published Contributors 3 * @jonnadal jonnadal Jon Nadal * @graydon graydon Graydon Hoare * @abhinav-upadhyay abhinav-upadhyay Abhinav Upadhyay Languages * Rust 93.6% * JavaScript 2.9% * HTML 2.0% * CSS 1.3% * Shell 0.2% * (c) 2021 GitHub, Inc. * Terms * Privacy * Security * Status * Docs * Contact GitHub * Pricing * API * Training * Blog * About You can't perform that action at this time. You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.