Modelling the archetype of a message-passing bug with TLA+ (2022)

Then it will be too noisy or too slow to be useful due to too many intermediate states. The feature of TLA+ is that it forces you to greatly dumb down the code to be able to use it, so it's more of verifying an algorithm represented as visual graph blocks rather than verifying assembly instructions.

I understand the wish for a magic bullet to just verify already existing code, but I recon the answer to this is to verify code before it's even written.

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.