Comment by amw-zero

There’s a few different perspectives on this. One is, there isn’t much of a need to verify the implementation once you’ve verified an abstract specification. The costliest errors are _design_ mistakes, i.e. high-level errors that could never lead to a satisfactory implementation. Once you figure those issues out, it’s simple to write an implementation that conforms to the spec.

I think there’s actually merit to that perspective if you think about it for a while. However, I have also seen relatively simple behavior be implemented in complex ways, usually due to performance optimizations. In those cases, it’s nontrivial to know if it’s implementing the spec. But the spec can be used to generate test cases in many ways, e.g. http://www.vldb.org/pvldb/vol13/p1346-davis.pdf.

Frankly, I’ve had the most success by not using TLA+ and by instead writing executable models. And then using the model to show the expected values for interesting test cases, and then manually write test cases using those expected values.