What TLA+ can and can't check

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…

Quelle: Originalartikel öffnen