> It's infamously hard to exhaustively unit-test concurrency.

a useful example from last week where TLA+ found a bug in pg_rewind:

https://multigres.com/blog/2026/05/04/tla-pg-rewind