Marc Brooker on Nostr: TLA+ as a correctness oracle for deterministic (or even non-deterministic) simulation ...

TLA+ as a correctness oracle for deterministic (or even non-deterministic) simulation testing makes a ton of sense to me.

As you say, a big part of that is driving folks to think about what correctness means to them.

In DSQL testing, for example, we've used "do what Postgres does" as a correctness oracle for a lot of the non-distributed surface area, just because that's what many of our customers care about.