Regarding the last point — correct, Stateright aims to verify both. It’s important to clarify that this doesn’t provide a proof of correctness, but it can dram

Regarding the last point — correct, Stateright aims to verify both. It’s important to clarify that this doesn’t provide a proof of correctness, but it can dramatically improve confidence in both the design and implementation compared with fuzz testing, for example. This is done by exhaustively enumerating possible nondeterministic outcomes (e.g. due to message reordering) within specified constraints (e.g. up to S servers and C clients performing X operations…). Examples: SD Paxos: https://github.com/stateright/stateright/blob/master/examples/paxos.rs https://github.com/stateright/stateright/blob/master/example... ABD (linearizable register algorithm): https://github.com/stateright/stateright/blob/master/examples/linearizable-register.rs https://github.com/stateright/stateright/blob/master/example...