LLMs are bad at vibing specifications

You can go far without writing TLA+ syntax now, but you still need to understand temporal logic.

In the age of LLMs, syntax is no longer the bottleneck for writing, reading, or learning TLA+. People are even getting value by generating T...