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.