## What TLA+ can and can't check ## Let's chill just a little bit on the "TLA+ will save AI from itself" narrative Last week Boris Cherny, the inventor of Claude Code, mentioned that Opus was able to use TLA+1 to find race conditions in code. And now everybody on the internet is talking about formal verification. As a long-time educator (1 2) and advocate of TLA+, this is really exciting! TLA+ is great at designing complex concurrent systems and making sure they're bug-free.2 As a long-time advocate of level-headedness, this new euphoria worries me. I read a lot of people saying that formal…