Unfortunately the benefit of TLA+ is the act of modeling your system painstakingly. The actual checker helps confirm your hypothesis, etc. But skipping the modeling and outsourcing it is not ideal. I’ve always struggled reasoning about models my team mates wrote, and will often have to mentally go through the process of arriving at the same abstractions/invariants etc before I can understand it.
Agreed. To quote Leslie Lamport, "the hardest part of TLA+ is learning to think abstractly."
There's always a moment, usually annoyingly late in the process, where I realize I've been massively overthinking everything or solving the wrong problem. Time is an essential an ingredient. Clear thinking is extremely hard.
LLMs are definitely useful along the way, but the thinking is the spiritually fulfilling part.
Exactly. I view a complete TLA+ specification as a kind of metalanguage that can be used with LLMs to generate code from.