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.