Hacker News Reader

As I found out recently, there's a lighter option: model checkers like Spin. You describe your synchronization logic in a small modeling language (Promela), and Spin tries every possible interleaving of that model.

Mix of different types of tests helps.

Best examples are SQLite and Jepsen test suites for dbms engines.

https://jepsen.io/

My experience has been the opposite. If lean had linear types (or separation types), it would be, but as it is, Lean's just a little bit too focused on talking about results to tidily talk about how those results are computed.

I don't know. For many operations, you can encode "how" by saying "under any permutation of this sequence of applications". At least, for EREW machines.