bvrmn 1 day ago

Even 10x speedup would be amazing. Just imagine current 1min check would be performed in 6s.

1
ahelwer 11 hours ago

There is a strong Jevons Paradox effect at play here though, people generally have a set amount of wall-clock time (1 minute, 10 minutes, etc.) they budget to check their model and then find the largest model that fits within that wall-clock time. So really this just increases the size of the state space people will explore, which might be the difference between checking, say, 3 vs. 5 nodes in a distributed system.

bvrmn 10 hours ago

For TLA it's even worse. Increasing node counts makes the spec immediately more "correct", at least it feels like that xdd.