I've been using TLA with claude code at work and it roughly takes twice as long, but it's already _fast_ to get claude to produce code and this prevents a lot of rework.

Been having LLMs make TLA+ models since the winter and it does work wonders for complex stuff, I guess for the same reason it works for humans: the process of building the model helps when designing the code even if the model is thrown away later (I keep mine though)