Property-based testing and model-based testing are closely related. Both ask the developer to state the expected behavior of a system (whether you call it a property, invariant, model, specification, or contract) and then validate that behavior over arbitrary inputs and arbitrary sequences of operations. Property-based testing frameworks also typically provide fuzzing and shrinking.

Where we felt there was a gap was in expressing rich stateful behavior: models involving non-determinism (e.g. a timeout where the write may or may not have committed), concurrency, and eventual asynchronous completion, and then checking that an observed execution trace conforms to that model. Accordant aims to make those kinds of specifications concise and readable.

Once you have such a model, it's possible to integrate it with the fuzzing and shrinking capabilities of existing property-based testing libraries. We'll have documentation on that integration soon.