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.

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.

Mix of different types of tests helps.

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

https://jepsen.io/