This post stems from a recent conversation with Heidi Howard where we talked about the changing role of TLA⁺ & finite-state model checking in both research and industry. For a long time, users of TLA⁺ (or other formal specification languages like Quint) had a classic 80/20 payoff/effort choice available to them: they could either put in a large amount of effort to formally prove their system properties correct with 100% confidence, or for 20% of that effort they could model-check their system and get perhaps 80% of that confidence. This economic calculation might no longer hold. The summer of 2026 has seen fairly astonishing improvements in the field of automated theorem proving. System correctness theorems are generally shallow but broad, eschewing deep math knowledge but requiring many tedious steps. Thus people formally specifying their system have a new option, where they can...