Linearizability checker written in Rust

Tools for verifying linearizability of S2

LTest is a framework for verifying the linearizability of C++ data structures.

Concurrent priority queue in Harmony with atomic specification, lock-based implementation, and black-box differential testing.

This test harness is a verification system that checks implementations for conformance to the Durable Promise Specification.

Framework for distributed system's verification, with fault injection.

Jepsen tests for Restate

A collection of Rust crates for distributed computing.

Parallel property-based testing with a deterministic thread scheduler

linearizability checker for distributed systems

A linearizability checker for concurrent data structures

Jepsen tests for Tarantool

An implementation of ISIS total order multicast protocol

A tutorial about how to apply property-based testing to stateful systems.

A tutorial about how to apply property-based testing to stateful systems.

Reading the linearizability paper with TLA+

An experimental linearizability checker for lock-free data structures using safe memory reclamation.

Verification tool for lock-free data structures with safe memory reclamation.