I don't think I disagree with any of that.

TLA+ is a relatively simple language so I think it's a good candidate for this kind of stuff; most of the stuff in the generated LSP also just proxies straight to the official command line tools. It's certainly a simpler language than Rust, so I think it's easier for Claude to keep a higher percentage of stuff in context, and at least using the TLA+ bindings seems to work pretty well.

I haven't done it since my laptop has lots of RAM, but I suspect that I will likely edit the generated code to eat less at some point.