Yes
I was able to find and prevent a catastrophic bug by pointing Opus armed with TLA+ at the problem
lopatin on Hacker News
In the thread “The internet discovers TLA+. Now what?”
Helped: Using TLA+ invariants to verify state-machine logic.
… At my company, some experts were optimizing our clustering and failover logic by adding a bit more state (and hence complexity). Despite me not being an expert in that area, I was able to find and prevent a catastrophic bug by pointing Opus armed with TLA+ at the problem. It was a bug that was not possible in the prior implementation of the system and no one thought to write unit tests for the sequence of steps that triggers it, so initially went unnoticed. …