I'm getting the impression that LLMs are just not very good at "reasoning" about time. I have definitely had success getting a coding agent to produce decent concurrent code, but I had to basically lead it by the nose, and I strongly suspect that in most cases it would have taken less time to just do it the old fashioned way.

I've had good luck having it translate TLA+ specs to programming languages. The specs are written by me and my fingers, and I've done most of the interesting concurrency reasoning beforehand.

I'm pretty sure it still saves me time, and if nothing else it's an excuse to write TLA+, and that's fun.