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…).
There is no reason to start implementing things, if your design is wrong.
Formal Specification proves your design, while Formal Verification proves your implementation.
As far as I understand this project - Stateright does both (i.e. 2-in-1). Kind of executable model?